Jean-Christophe Filliâtre

Recherche

Je co-organise les workshops suivants :

• VSTTE 2009
• PLPV 2010

Publications récentes :

• Invited tutorial at AFM 09 : Why: an Intermediate Language for Deductive Program Verification
• Combining Coq and Gappa for Certifying Floating-Point Programs (Calculemus 2009), avec Sylvie Boldo et Guillaume Melquiond
• A Functional Implementation of the Garsia--Wachs Algorithm (Workshop on ML 2008); code
• Invited talk at SMT'08 : Using SMT Solvers for Deductive Verification of C and Java Programs
• 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)

Toutes mes publications

Programmation

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

• 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

Si vous aimez les maths et la programmation, vous allez adorer Project Euler.

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