Publications

You can also find my articles on my Google Scholar profile.

Conference Papers

AdapTT: Functoriality for Dependent Type Casts

Published: July 18, 2025

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 gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.

Recommended citation: Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard. Arxiv Preprint
Download Paper

AdapTT: A Type Theory with Functorial Types

Published in 31st International Conference on Types for Proofs and Programs (TYPES 2025), 2025

Many type theoretic features, from subtyping to observational equality and cast calculi in gradual typing, center around the ability to cast values from one type to another. These casts all act in a conspicuously similar fashion, which actually corresponds to the fact that type formers in dependent type theory are functorial. We propose and extensively study a type theory, AdapTT, which makes systematic and precise this idea of functorial type formers

Recommended citation: Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard. AdapTT: A Type Theory with Functorial Types 31st International Conference on Types for Proofs and Programs TYPES 2025 University of Strathclyde, Glasgow, Scotland, 9–13 June 2025 Abstracts https://msp.cis.strath.ac.uk/types2025/
Download Paper | Download Slides

Martin-Löf à la Coq

Published in CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

We present an extensive mechanization of the metatheory of Martin-Löf Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show not only the decidability of conversion, but also the decidability of type checking, using an approach guided by bidirectional type checking. From our proof of decidability, we obtain a certified and executable type checker for a full-fledged version of MLTT with support for Π, Σ, ℕ, and Id types, and one universe. Our development does not rely on impredicativity, induction-recursion or any axiom beyond MLTT extended with indexed inductive types and a handful of predicative universes, thus narrowing the gap between the object theory and the metatheory to a mere difference in universes. Furthermore, our formalization choices are geared towards a modular development that relies on Coq’s features, e.g. universe polymorphism and metaprogramming with tactics.

Recommended citation: Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. 2024. Martin-Löf à la Coq. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). Association for Computing Machinery, New York, NY, USA, 230–245. https://doi.org/10.1145/3636501.3636951
Download Paper