Works in Coq

Master's thesis: Coq en Coq (Coq in Coq)

Abstract: Documents available:

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 here.


Directors: Gérard Huet and Benjamin Werner


Self-validation of a proof assistant with inductives families.

Ph.D. dissertation:

Postscript version, BibTeX reference.