Pierre Corbineau's homepage

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.

• Micro-controllers (3I,3)
• Object-Oriented Programming (E2I,4)

• 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