Jean-Christophe Filliâtre's home page

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Jean-Christophe Filliâtre's home page no image

no image

Jean-Christophe Filliâtre

Contact CV

Research

CNRS researcher. I work at the Laboratoire de Recherche en Informatique (Université Paris Sud), in the team Démons which is part of the Proval project.

Publications
I'm co-organizer of the TYPES 2004 workshop
Multi-Prover Verification of C Programs (to be presented at ICFEM 2004)
Formalization of a finite sets library in Coq.
A functional implementation of the Koda-Ruskey algorithm (in French) ( the code). Presented at JFLA 2002 (slides in French).
Slides on the ICS decision procedure (see the web site)
Slides on the new architecture of the system Coq (version 7)
PhD thesis: proof of imperative programs in Type Theory.

Software

I'm the (co)author of the following programs:

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

Many other libraries and applications on that page dedicated to Caml programming. The Caml Language

The Caml Language

Teaching

This year I teach at Université Paris Sud.

Teaching notes: Compilation project and Introduction to functional programming (in French).

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

Miscellaneous

Français

Jean-Christophe.Filliatre[at]lri.fr (formatted with yamlpp).