16 citations · 32 across the 9 of their papers we have counts for
9 papers
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity a…
Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation
Meven Lennon Bertrand, Alexis Saurin
Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follo…
AdapTT: Functoriality for Dependent Type Casts
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin +1
The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradua…
What does it take to certify a conversion checker?
Meven Lennon-Bertrand
We report on a detailed exploration of the properties of conversion (definitional equality) in dependent type theory, with the goal of certifying decision procedures for it. While…
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard +2
We present an extensive mechanization of the meta-theory of Martin-Löf Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show no…
Definitional Functoriality for Dependent (Sub)Types -- Extended version
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper…
A Reasonably Gradual Type Theory
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau +1
Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently…
Complete Bidirectional Typing for the Calculus of Inductive Constructions
Meven Lennon-Bertrand
This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and chec…
Gradualizing the Calculus of Inductive Constructions
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau +1
We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucia…