Logiciels

Formal developments and proofs in Coq of numerical analysis problems. This archive includes several Coq developments: - Lebesgue directory is about the Lebesgue Integration of Nonnegative Functions (see paper, paper, and report); - Lebesgue/bochner_integral directory is about the Bochner integral (see report); - LM directory is about the Lax–Milgram theorem (see paper, paper, and report); - Opam package coq-num-analysis: version 1.0 provides Lebesgue, and LM. - Lebesgue and LM are compiling in Coq 8.12 to 8.16.

Mariotel est un logiciel libre (GNU GPL) de gestion de salles de TP virtuelles pour l'enseignement à distance, conçu et réalisé à partir de mars 2020 suite à la crise sanitaire du Covid-19. Avec ce système, n'importe quel enseignant d'une université hébergeant un serveur Mariotel peut, à tout moment, réserver une salle de TP composée de plusieurs ordinateurs virtuels. Chaque ordinateur virtuel, appelé "station de travail", sera affecté à un étudiant de la classe en début de séance et sera rendue accessible par un simple navigateur web (firefox, chrome, safari, etc). De son côté, l'enseignant aura, lui aussi, accès à distance à *tous* les postes des étudiants en simultanée. Il pourra prendre le contrôle de la station de travail, si nécessaire, avec sa souri et son clavier, en même temps que l'étudiant affecté au poste, en cliquant sur le poste de l'étudiant depuis une page web de contrôle de la salle. Il pourra ainsi assister l'ensemble des étudiants dans la réalisation de la séance de TP (on s’appuiera sur un logiciel de visioconférence, comme BBB, Meet, Teams ou Zoom, pour communiquer de vive voix avec la classe ou, à minima, sur un logiciel de messagerie instantanée). Le nom du projet, Mariotel, s'explique par l'idée originale de rendre le logiciel Marionnet utilisable à distance, dans une fenêtre de navigateur. À présent, le projet dépasse largement cet objectif initial et couvre l'ensemble des besoins en TP informatique réalisables sous le système d'exploitation GNU/Linux, ce qui reste (et restera) l'unique contrainte. La plateforme peut aussi être exploitée pour allouer des salles en libre service en dehors des heures de cours (certains enseignants réservent des salles en libre service pour des petits groupes, parfois le soir, voire la nuit). Dans les premiers mois de service (de septembre 2020 à mai 2021, incluant les confinements de fin 2020 et début 2021), Mariotel a été utilisé par plus de 40 enseignants différents (de l'IUT et de l'IG de l'USPN), pour plus de 4500 sessions étudiant (réellement connectés), c'est-à-dire 18000 heures étudiant au total.

Bibliothèque OCaml généraliste, complément des bibliothèques standards, sous licence libre GNU GPL

Logiciel pédagogique de simulation de réseaux d'ordinateurs, sous licence libre GNU GPL. Utilisé par plusieurs universités en France et à l'étranger. Financé par l'IUT de Villetaneuse et l'Institut Galilée

Démonstration à la conférence EIAH 2007 (Environnements Informatiques pour l'Apprentissage Humain) Projet E-Learning Université Paris 13

Utilitaire permettant d'automatiser l'analyse lexicale, syntaxique et en partie sémantique des paramètres d'appel d'un script bash. Code source OCaml, licence GPL.

Cdrom amorçable, auto-configurable, dérivé de Knoppix 5.0.1, francisé et spécialisé pour les enseignements aux dép. R&T et INFO de l'IUT Villetaneuse. Licence GPL.

Application (en mode texte) de simulation d'un réseaux d'ordinateurs qui exploite la technologie UML (User Mode Linux) et repose sur un DVD amorçable, auto-configurable, dérivé de Knoppix 3.8. Code source OCaml, licence GPL.

Cdrom amorçable, auto-configurable, dérivé de Knoppix 3.8, francisé et spécialisé pour les enseignements au dép. GTR de l'IUT Villetaneuse. Licence GPL.