# Pierre Castéran's Home page

### Contact `(My first name).(my last name)@labri.fr`

`
`## ACM Software System Award (2013)

The video of the ACM software system award for the Coq development team.
## 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
## Assistants de preuves / Computer aided proofs

### Coq'Art

The first book on Coq
by Yves Bertot and myself

### 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:

- 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

Informatique Théorique 1

Follow this Link, too
## 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