# Pierre Castéran's Home page

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

tel/ +33 540003526

`
`## Research

### Coq'Art

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).

https://github.com/coq-community/hydra-battles

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:

- 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

## Distinction

### ACM Software System Award (2013)

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

Coq's official site
## Teaching

Logique et Preuve

Formal Methods