From the 3 of 5 linked papers with an AI index.
5 citations · 6 across the 4 of their papers we have counts for
5 papers
Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-ÄubriÄ Interpolation
Meven Lennon Bertrand, Alexis Saurin
The paper presents a new proof of the proof‑relevant Craig interpolation theorem for the simply‑typed lambda calculus using bidirectional typing techniques, and provides a formalis…
What does it take to certify a conversion checker?
Meven Lennon-Bertrand
The paper investigates how to formally certify conversion (definitional equality) checkers in dependent type theory, emphasizing injectivity properties as sufficient for correctnes…
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
The paper presents a domain‑theoretic proof technique that establishes definitional inversion properties (injectivity and no‑confusion) of type constructors in dependent type syste…
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…
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…