Jean-Christophe Filliâtre

Recherche

• Publications

• Union-Find Persistant, avec Sylvain Conchon ; Preuve en Coq
• Type-Safe Modular Hash-Consing, avec Sylvain Conchon (Workshop on ML 2006)
• Backtracking iterators (Workshop on ML 2006) Traduction anglaise de Itérer avec persistance (JFLA 2006)
• Draft: Combining the Coq Proof Assistant with First-Order Decision Procedures
• Multi-Prover Verification of C Programs (ICFEM 2004)
• Formalisation d'une bibliothèque d'ensembles finis en Coq.
• Une implantation fonctionnelle de l'algorithme de Koda-Ruskey ( le code). Présenté à JFLA 2002 (transparents).
• Transparents sur la procédure de décision ICS (voir le site web)
• Transparents sur la nouvelle architecture du système Coq (version 7)
• Thèse : preuve de programmes impératifs en théorie des types.

Programmation

• Why, un outil de verification de programmes ; ne manquez pas ma galerie de programmes certifiés
• Caduceus, un outil de vérification de programmes C

• ocamlgraph une bibliothèque de graphes pour Objective Caml
• bibtex2html, un traducteur BibTeX vers HTML
• ocamlweb, un outil de programmation littéraire pour Objective Caml

Enseignement

J'assure également une partie du cours Calcul des Constructions Inductives du Master Parisien de Recherche en Informatique (MPRI). Voir mes notes de cours.

J'ai écrit un polycopié d'Initiation à la programmation fonctionnelle

TP d'Informatique en Caml (classes préparatoires option info)

Divers

• Voyage dans le temps, avec mes premiers ordinateurs
• Science Fiction
• FTP