#
Pierre Corbineau's homepage

*
Voir cette page en
français
*

Contact information

I am an assistant professor in the
Distributed and Complex Systems Group of the
VERIMAG laboratory, teaching at the
Polytech'Grenoble engineering school of the
Joseph Fourier University.

I am a former post-doc in the
"Foundations" group of the Intelligent Systems theme of the
Institute for Computing and Information Sciences at the
*
Radboud Universiteit Nijmegen*.

I am a former PhD student at the in the *
Laboratoire de Recherche en Informatique* in the Démons
team.

## Research

My research topics include:

- Certified Provable Security of
protocols in the computational model

- Providing better proof languages for mathematicians
- Web-based collaborative interactive formal proof interfaces

- First-order intuitionnistic logic proof-search
- Equational proof search
- Representation and checking of first-order proofs in type theory

**Here you can find is a list of my publications.
**

## Teaching

I am a permanent teacher at
Polytech'Grenoble in the engineering cursus, in both the regular and sandwich course departments 3I (Computer Engineering and Instrumentation) and E2I (Electronics and Computer Engineering). I am the pedagogic manager for the Year 3 in 3I.

I am managing the following courses:
- Micro-controllers (3I,3)
- Object-Oriented Programming (E2I,4)

I also teach in the following courses:
- Embedded Systems Project (3I,3)
- Algorithms and Programming (E2I,3)
- UNIX System Programming (E2I,5)

In 2010-2011, I have also taugh the Logics part of The Computer Science optuion for the preparation to the Agrégation of Mathematics.

## Programming

- C-zar: the declarative proof language for Coq :
here.
- A small PTS (pure type systems) typeckecker / evaluator :
here.
- An implementation in Objective Caml of randomized binary trees :
here
- Reflected first-order proofs in Coq :
v8.0pl3 / SVN
- Contributions to the Coq proof assistant

*
Voir cette page en
français
*