Jean-Christophe Filliâtre

Research

Recent publications:

• 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), with Sylvain Conchon
• Formal Verification of MIX Programs (Conference in honor of Donald E. Knuth)
• A Persistent Union-Find Data Structure (Workshop on ML 2007), with Sylvain Conchon ; see the Coq formalization
• The Why/Krakatoa/Caduceus platform for deductive program verification (tool presentation at 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), with Sylvie Boldo
• Type-Safe Modular Hash-Consing (Workshop on ML 2006), with Sylvain Conchon
• Backtracking iterators (Workshop on ML 2006) English translation of this article

All publications

Software

• Why, a software verification tool; don't miss my gallery of certified programs
• Caduceus, a verification tool for C programs

• Mlpost, an Objective Caml interface to MetaPost
• ocamlgraph, a graph library for Objective Caml
• bibtex2html, a BibTeX to HTML translator
• ocamlweb, a literate programming tool for Objective Caml

Teaching

Lecture on Why and Caduceus at the TYPES Summer School 2007: notes (PDF) / slides (PDF) / lab exercises (PDF)

I wrote an Introduction to functional programming (in French).

Some Computer Science problems in Caml submitted to first degree students (in French)

Miscellaneous

• Science Fiction
• FTP