Pierre Castéran's Home page

Contact (My first name).(my last name)@labri.fr
tel/ +33 540003526



The first book on Coq by Yves Bertot and myself

Commented developments in Coq

Hydra battles, ordinals and the Coq proof assistant

A development in Coq on Kirby and Paris' hydra battles, Ketonen and Solovay's combinatorial work on ordinals, etc (work in progress).


Copy of the documentation (pdf)
Note The latex source is regularly updated in the coq-community site.

html links may be inactive in this copy.

Addition chains

A commented development on exponentiation algorithms based on addition chains.

Please click here.

Copy of the documentation (pdf)
Note The latex source is regularly updated in the framagit site.

html links may be inactive in this copy.

Comments and contributions are welcome !

Tutorial on [co]-inductive types in Coq (by Eduardo Gimenez and myself)

Revision July 28th 2006 (for Coq V8.1 beta)

Tutorial on Type Classes and Relations in Coq (by Matthieu Sozeau and myself)

Hilbert's Epsilon operator and partial functions in Coq (V8.1)

The module ClassicalEpsilon of the new standard library (V8.1 beta) allows us to use Hilbert's epsilon operator.
File Epsilon.v contains the definition of the definite description operator iota, as well as some tactics for dealing with descriptions and partial functions.
A small example is given, comparing partial functions with some (total) implementations.

A A paper (in French) presented at JFLA'2007
The slides (pdf)

A course on Coq (in French)

Slides for the course given at The JFLA 2006 in Pauillac.
Le Coq au Pauillac et aux omégas (in pdf)

Séminaires à Limoges (27 et 28 janvier 2010)

Maths pour tous (pdf)
introduction à Coq

Séminaire SIESTE à l'ENS Lyon (28 Février 2007)

A3PAT Project (Assisting proof assistants)

This project is devoted to provide proof assistants with more automation: automatic tools should provide the assistant with some trace it will use to build a certified proof term.
the project's site

Des omégas dans le Vouvray (in French)

Ordinal notations and rpo : A contribution for Coq (8.1) , (joint work with Evelyne Contéjean and Florian Hatat). This development (work in progress !) includes:
A small description

Book review

On Adapting Proof-as-Programs: The Curry-Howard Protocol, by Poernomo, Crossley and Wirsing.
Follow this Link

Art Gallery


ACM Software System Award (2013)

The video of the ACM software system award for the Coq development team.


Coq's official site


Logique et Preuve

Formal Methods