First-Order Reasoning in the Calculus of Inductive Constructions. - Pierre Corbineau (TYPES, 2003)

Reflecting Proofs in First-Order Logic with Equality. - Evelyne Contejean; Pierre Corbineau (CADE, 2005)

Deciding Equality in the Constructor Theory. - Pierre Corbineau (TYPES, 2006)

Cooperative Repositories for Formal Proofs. - Pierre Corbineau; Cezary Kaliszyk (Calculemus/MKM, 2007)

A Declarative Language for the Coq Proof Assistant. - Pierre Corbineau (TYPES, 2007)

A Real Semantic Web for Mathematics Deserves a Real Semantics. - Cezary Kaliszyk; Pierre Corbineau; Freek Wiedijk; James McKinna; Herman Geuvers (SemWiki, 2008)

A New Elimination Rule for the Calculus of Inductive Constructions. - Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Luis Sacchini (TYPES, 2008)

Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. - Pierre Corbineau; Mathilde Duclos; Yassine Lakhnech (CPP, 2011)

On the Generation of Positivstellensatz Witnesses in Degenerate Cases. - David Monniaux; Pierre Corbineau (ITP, 2011)

A Framework for Certified Self-Stabilization. - Karine Altisen; Pierre Corbineau; Stéphane Devismes (Log. Methods Comput. Sci., 2017)

Squeezing Streams and Composition of Self-stabilizing Algorithms. - Karine Altisen; Pierre Corbineau; Stéphane Devismes (FORTE, 2019)

Certified Round Complexity of Self-Stabilizing Algorithms. - Karine Altisen; Pierre Corbineau; Stéphane Devismes (DISC, 2023)

Certification of an exact worst-case self-stabilization time. - Karine Altisen; Pierre Corbineau; Stéphane Devismes (Theor. Comput. Sci., 2023)