en ¦ fr > Publications

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

In which we report on the MetaCoq project, up to its 1.2 version.

Pdf Hal

Definitional Functoriality for Dependent (Sub)Types

In which we extend a dependent type theory with definitionally functorial operations, and use these to obtain a well-behaved coercive subtyping.

Pdf Hal

Martin-Löf à la Coq

In which we report on a formalization, in Coq, of a fully certified type-checker for Martin-Löf Type Theory.

Doi Pdf Hal ArXiv BibTeX GitHub

A Reasonably Gradual Type Theory

In which we extend our Gradual Calculus of Inductive Constructions to internalize precision and allow for sound reasoning over gradual programs.

Doi Pdf Hal BibTeX

Gradualizing the Calculus of Inductive Constructions

In which we investigate gradual variations on the Calculus of Inductive Construction. Presented at POPL '22.

Doi Pdf Hal ArXiv BibTeX

Complete Bidirectional Typing for the Calculus of Inductive Constructions

In which I presents a bidirectional type system for the Calculus of Inductive Constructions.

Doi Pdf Hal ArXiv BibTeX

Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.