Guillaume GENESTIER
Doctorant
Mon sujet de thèse
J'ai démarré en septembre 2017 une thèse avec
Frédéric Blanqui et
Olivier Hermant sur la vérification de la terminaison d'un système de réécriture dans le λΠ-calcul modulo théorie et l'implémentation d'un vérificateur de terminaison pour
Dedukti.
Enseignement
2019-2020
Introduction à l'algorithmique et à la programmation C++ - L1 IUT d'Orsay
Ce cours aura lieu du 9 septembre au 25 octobre.
Les cours magistraux sont faits par Cécile Balkanski et Hélène Maynard.
Vous trouverez la totalité des documents utiles sur le
Moodle de l'IUT d'Orsay (nécessitant malheureusement un compte).
Corrigés
Années précédentes
2018-2019
2017-2018
Publications (et autres documents)
- Ma thèse de doctorat intitulée Dependently-Typed Termination
and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting et les slides de la soutenance;
- Encoding Agda Programs Using Rewriting, FSCD 2020, Juillet 2020
- Universe Polymorphism Expressed as a Rewriting System, Types et les slides présentée uniquement à l'ENS Paris-Saclay, suite à l'annulation de l'événement, Mars 2020
- SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent Types, Higher-Order Rewriting et les slides, Juin 2019
- Avec Frédéric Blanqui et Olivier Hermant, Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, Formal Structures for Computation and Deduction (FSCD), Juin 2019
- Avec Frédéric Blanqui et Olivier Hermant, Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, Types, Juin 2019
-
Exposé lors des portes ouvertes du LSV, présentant les ordinaux dénombrables et destiné aux L3 de l'ENS Cachan :
En finir avec la terminaison ?,
septembre 2018
-
Avec Frédéric Blanqui,
Termination of Lambda-Pi modulo rewriting using the size-change principle,
présenté au WorkShop on Termination (WST),
et les slides associées,
juillet 2018
-
Présentation de Dedukti lors de la journée des doctorants de la SIF :
Slides,
juin 2018
-
Avec Frédéric Blanqui,
note sur la sémantique des règles non-linéaires de Dedukti,
mars 2018
-
Exposé lors des Rencontres GeoCal-LAC dont voici les slides,
novembre 2017
-
Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint,
Rapport de stage de recherche,
septembre 2017
et les slides de la soutenance associée
Développement logiciel
- Co-mainteneur de Dedukti, un vérificateur de types pour le λΠ-calcul modulo réécriture;
- Développeur de SizeChangeTool, un vérificateur de terminaison pour la réécriture d'ordre supérieure avec types dépendants;
- Développeur avec Jesper Cockx de Agda2Dedukti, un traducteur des programmes d'Agda en Dedukti.
Me contacter
N'hésitez pas me contacter par
mail.