Jean-Christophe Filliâtre

Recherche

Publications récentes :

• A Functional Implementation of the Garsia--Wachs Algorithm (Workshop on ML 2008); code
• Invited talk at SMT'08 : slides
• Semi-Persistent Data Structures (ESOP 2008), avec Sylvain Conchon
• Formal Verification of MIX Programs (Journées en l'honneur de Donald E. Knuth)
• A Persistent Union-Find Data Structure (Workshop on ML 2007), avec Sylvain Conchon ; voir la preuve en Coq
  Version anglaise de Union-Find Persistant (JFLA 2007)
• The Why/Krakatoa/Caduceus platform for deductive program verification (présentation d'outil àCAV 2007)
• Queens on a Chessboard: an Exercise in Program Verification (draft)
• Designing a Generic Graph Library using ML Functors (TFP 2007)
• Formal Verification of Floating-Point Programs (ARITH 18), avec Sylvie Boldo
• Type-Safe Modular Hash-Consing (Workshop on ML 2006), avec Sylvain Conchon
• Backtracking iterators (Workshop on ML 2006) Version anglaise de Itérer avec persistance (JFLA 2006)

Toutes mes publications

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

• Mlpost, une bibliothèque Objective Caml au dessus de MetaPost
• 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'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