Pierre Castéran's Home page
Contact (My first name).(my last name)@labri.fr
GDR Génie de la programmation et du Logiciel
Groupe de travail : Langages, Types et Preuves
Formal proofs of Local Computation Systems
The Loco project
The algoproof working group at labri
Monitorat Math-Info
Suivre ce lien
Assistants de preuves / Computer aided proofs
Coq'Art
The first book on Coq
by Yves Bertot and myself
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)
Tutorial on [co]-inductive types in Coq (by Eduardo Gimenez and myself)
Revision July 28th 2006 (for Coq V8.1 beta)
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)
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:
- Proof of termination of the rpo with status
- Some results about Hilbert's epsilon operator
- An extension of the Ensembles library : denumerable sets
- Ordinal notations based on Cantor and Veblen normal forms
- Axiomatic definition of countable ordinals (after K. Schütte)
A small description
Book review
On Adapting Proof-as-Programs: The Curry-Howard Protocol, by
Poernomo, Crossley and Wirsing.
Follow this Link
Art Gallery
Contact
Coq's official site
Teaching Formal Methods
Follow this Link
Computational linguistics
ESSLLI'2004 page
Coq files for the course given with Richard Moot :
Proof automation for type logical grammars
Teaching Programming
Master CCSI, 2009-2010