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.

Ph.D.

Directors: Gérard Huet and Benjamin Werner

Subject:

Self-validation of a proof assistant with inductives families.

Ph.D. dissertation:

Postscript version, BibTeX reference.