Jean-Christophe Filliâtre

Research

Recent publications:

• 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

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

Teaching

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