In which I investigate the exact meta-theoretic requirements to certify various properties of various conversion-checking and typing algorithms.
In which we report on the MetaCoq project, up to its 1.2 version.
In which we extend a dependent type theory with definitionally functorial operations, and use these to obtain a well-behaved coercive subtyping.
In which we report on a formalization, in Coq, of a fully certified type-checker for Martin-Löf Type Theory.
In which we extend our Gradual Calculus of Inductive Constructions to internalize precision and allow for sound reasoning over gradual programs.
In which we investigate gradual variations on the Calculus of Inductive Construction. Presented at POPL '22.
In which I presents a bidirectional type system for the Calculus of Inductive Constructions.
Under Creative Commons CC0 License, source on github. Built using Pelican. Theme adapted from pelican-svbhack by Giulio Fidente.