Pierre Corbineau

Pierre Corbineau is an Assistant Professor in the Distributed and Complex Systems Group at the VERIMAG laboratory, teaching at Polytech'Grenoble engineering school within Joseph Fourier University. Previously, he held postdoctoral positions at Radboud University Nijmegen and completed his PhD at Laboratoire de Recherche en Informatique (LRI) in the Démons team.

Education:

• PhD in Computer Science (2005), University Paris 11
• Master's thesis (2001), University Paris 7

Research Interests: Focuses on certified security protocols, formal proof systems, and web-based collaborative theorem proving. Develops declarative proof languages (e.g., C-zar for Coq) and contributes to automated reasoning in type theory. Explores first-order logic proof search and equational reasoning.

Teaching: Manages courses in microcontrollers, object-oriented programming, and UNIX system programming. Serves as pedagogic manager for Year 3 in the 3I department. Previously taught logic for mathematics aggregation preparation.

Software Contributions: Developed C-zar (part of Coq since v8.1), a PTS type checker, and probabilistic binary tree implementations. Contributed to Coq's core functionality through reflective proof techniques and formal validation frameworks.