en ¦ fr > Publications

AdapTT: Functoriality for Dependent Type Casts

Where we explore a type theory for type casting, and how to obtain structural type-casting from functoriality of type formers.

Hal GitHub

What does it take to certify a conversion checker?

In which I investigate the exact meta-theoretic requirements to certify various properties of various conversion-checking and typing algorithms.

Doi Pdf ArXiv BibTeX GitHub

Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation

In which we report on an experimental implementation of normalisation by evaluation for a type theory with observational equality.

Doi Pdf BibTeX GitHub

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.

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

Doi Pdf Hal ArXiv BibTeX

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.