Guillaume GENESTIER
PhD Student
My PhD topic
I started in september 2017 a PhD thesis under the direction of
Frédéric Blanqui and
Olivier Hermant on the termination checking of a rewrite rule system in the λΠ-calculus modulo theory and the implementation of it for
Dedukti.
Teaching
All the wordings (in French) can be found on
the French version of this webpage.
-
2019-2020
-
Introduction to algorithmic and C++ programming - L1 IUT d'Orsay
-
2018-2019
-
Databases Project - L3 ENS Paris-Saclay
-
Logic - L3 ENS Paris-Saclay
-
2017-2018
-
Complexity tutoring - L3 ENS Paris-Saclay
-
Logic - L3 ENS Paris-Saclay
Publications (and other documents)
- My PhD thesis entitled Dependently-Typed Termination
and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting and the slides of the defence;
- Encoding Agda Programs Using Rewriting, FSCD 2020, July 2020
- Universe Polymorphism Expressed as a Rewriting System, Types and the slides only presented at ENS Paris-Saclay, due to event cancellation, March 2020
- SizeChangeTool: A Termination Checker for Higher-Order Rewriting with Dependent Types, Higher-Order Rewriting and the slides, June 2019
- With Frédéric Blanqui and Olivier Hermant, Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, Formal Structures for Computation and Deduction (FSCD) and the slides, June 2019
- With Frédéric Blanqui and Olivier Hermant, Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, Types, June 2019
- Presentation on countable ordinals during the open day of the LSV, for 3rd year students (in French): En finir avec la terminaison ?, September 2018
- With Frédéric Blanqui, Termination of Lambda-Pi modulo rewriting using the size-change principle, presented at the WorkShop on Termination (WST), and the slides, July 2018
- Presentation of Dedukti during PhD students day of the French Society of Computer Science : Slides, June 2018
- With Frédéric Blanqui, note on the semantic of non-linear rewrite rules
in Dedukti, March 2018
- Presentation during the GeoCal-LAC Meeting, the slides are here,
November 2017
- Termination checking in the λΠ-calculus modulo theory. From a practical and a theoretical viewpoint,
Master internship report, September 2017 and the associated slides
Software Development
- Co-maintainer of Dedukti, a type checker for the λΠ-calculus modulo rewriting;
- Developper of SizeChangeTool, a termination checker for higher-order rewriting with dependent types;
- Developper with Jesper Cockx of Agda2Dedukti, a translator of programms from Agda to Dedukti.
Contact
Do not hesitate to contact me using my
e-mail.