Martin-Löf à la Coq. - Arthur Adjedj; Meven Lennon-Bertrand; Kenji Maillard; Pierre-Marie Pédrot; Loïc Pujet (CPP, 2024)

AdapTT: Functoriality for Dependent Type Casts. - Arthur Adjedj; Meven Lennon-Bertrand; Thibaut Benjamin; Kenji Maillard (CoRR, 2025)