Gabriel Hondet’s web page

Gabriel Hondet

1 PhD topic

Under the supervision of Frédéric Blanqui and Gilles Dowek.

The broad topic is the translation of PVS specifications and proofs into the λΠ calculus modulo theory.

PVS is a an environment made of a theorem prover, a type checker and a parser which allows to develop specifications and prove them. It has been used by the NASA (see https://shemesh.larc.nasa.gov/fm/fm-pvs.html), Fujitsu &c. In particular, it implements predicate sub-typing, which allows to write concise specifications and provides a rich type system.

λΠ calculus modulo extends λ calculus with

Pragmatically, the target of the translation is Dedukti, our implementation of the λΠ calculus modulo in OCaml.

An automatic translator is being developed. At the date of writing (August 2020), we translate 120kb of PVS’ standard library.

2 Teaching

At ENS Paris-Saclay in L3 and M1.

2.1 Projet programmation 1

Base de code du projet

2.1.1 Ressources pour Emacs

2.1.2 Cheatsheets

2.2 Architecture système

2.2.1 Devoir Maison: compter les mots plus vite que Linux

Consignes: PDF
Fichiers de départs: mwc-starter.tar.gz

2.3 Rewriting

2.3.1 Homework

Homework, deadline: 2020-11-02, 12:00 GMT+01

2.4 BDD

3 Publications

4 Contact

gabriel 🧶 hondet ✨ lsv 🧶 fr
Mastodon
GPG fingerprint: E5EA DC25 705C 8DDD CFD4 5700 31BC 8105 F659 D425