Brève bio: J'ai fait une thèse en 1995-99 sous la direction de Christine Paulin, sur la preuve de programmes impératifs dans le système Coq. Juste après ma thèse, à l'automne 1999, j'ai refait l'architecture du système Coq, afin d'isoler un noyau ; c'est brièvement décrit dans ce papier. Puis je suis parti en post-doc au SRI, dans l'équipe PVS, où j'ai entrepris le développement de la procédure de décision ICS. Après mon retour, j'ai commencé en 2001 le développement d'un outil de vérification déductive de programmes appelé Why, utilisé notamment pour la preuve de programmes C dans l'outil Caduceus (aujourd'hui remplacé par Frama-C) et pour la preuve de programmes Java dans l'outil Krakatoa. En 2010, l'outil Why est devenu Why3.
Publications / Comités de programme / Jurys de thèse
Je suis un programmeur enthousiaste depuis 1984 (j'avais 13 ans). Mon premier ordinateur fut un Thomson TO7/70, sur lequel je programmais en Basic et en assembleur 6809. En 1986, j'ai changé pour l'Atari 520 ST, sur lequel je programmais en GFA Basic et en assembleur 68000. Je suis progressivement passé au PC au début des années 1990. Aujourd'hui je programme principalement en OCaml, sous Linux. Il y a quelques années, j'ai découvert le Project Euler ; si vous aimez les maths et la programmation, vous allez adorer.
Je suis le (co)auteur des programmes suivants :
J'enseigne à l'École Normale Supérieure. Je suis responsable du cours langages de programmation et compilation.
J'enseigne à l'École Polytechnique. Je suis responsable des cours INF411 et INF564.
Je suis co-auteur des livres suivants :
|
Sylvain Conchon et Jean-Christophe Filliâtre. Apprendre à programmer avec OCaml. Algorithmes et structures de données. Éditions Eyrolles. Septembre 2014. [site web | Eyrolles | amazon.fr] |
|
Benjamin Wack, Sylvain Conchon, Judicaël Courant, Marc de Falco,
Gilles Dowek, Jean-Christophe Filliâtre, Stéphane Gonnord. Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python. Éditions Eyrolles. Août 2013. [site web | Eyrolles | amazon.fr] |
|
Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyễn Numérique et Sciences Informatiques, 30 leçons avec exercices corrigés. Première. Éditions Ellipses. Août 2019. [site web | Ellipses | amazon.fr] |
|
Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyễn Numérique et Sciences Informatiques, 24 leçons avec exercices corrigés. Terminale. Éditions Ellipses. Juillet 2020. [site web | Ellipses | amazon.fr] |
|
Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyễn, Laurent Sartre Informatique - MPI2/MPI - CPGE 1re et 2e années: Cours et exercices corrigés. Éditions Ellipses. Août 2022. [site web | Ellipses | amazon.fr] |
Autres ressources plus anciennes :
Mes livres d'informatique préférés, et pourquoi.
De l'usage de break, continue et return (version PDF).
Concevoir, rédiger et corriger un sujet d'informatique (PDF)
Dix bonnes raisons de lire ou relire The Art of Computer Programming
