Works in Coq
Master's thesis: Coq en Coq (Coq in Coq)
The essential step of the formal verification of a proof-checker such
as Coq is the verification of its kernel: a type-checker for the
Calculus of Inductive Constructions (CIC) which is its underlying
The present work is a first small-scale attempt on a significative
fragment of CIC: the Calculus of Constructions (CC). We formalize the
definition and the metatheory of (CC) in Coq.
In particular, we prove strong normalization and
decidability of type inference. From the latter proof, we extract a
certified Caml Light program, which performs type inference (or
type-checking) for an arbitrary typing judgement in CC. Integrating
this program in a larger system, including a parser and
pretty-printer, we obtain a stand-alone proof-checker, called CoC,
for the Calculus of Constructions. As an example, the formal
proof of Newman's lemma, build with Coq, can be re-verified by
CoC with reasonable performance.
Generalization to PTS's with abstract subtyping
This work was generalized to the case of Pure Type Systems with an
abstract subtyping relation. The Coq development can be found
Gérard Huet and
Self-validation of a proof assistant with inductives families.