A Fibrational Account of Local States. - Kenji Maillard; Paul-André Melliès (LICS, 2015)

Dijkstra monads for free. - Danel Ahman; Catalin Hritcu; Kenji Maillard; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (POPL, 2017)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

A Monadic Framework for Relational Verification (Functional Pearl). - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CoRR, 2017)

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CPP, 2018)

Recalling a witness: foundations and applications of monotonic state. - Danel Ahman; Cédric Fournet; Catalin Hritcu; Kenji Maillard; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2018)

Dijkstra monads for all. - Kenji Maillard; Danel Ahman; Robert Atkey; Guido Martínez; Catalin Hritcu; Exequiel Rivas; Éric Tanter (Proc. ACM Program. Lang., 2019)

Principles of Program Verification for Arbitrary Monadic Effects. (Principes de la Vérification de Programmes à Effets Monadiques Arbitraires). - Kenji Maillard (2019)

The next 700 relational program logics. - Kenji Maillard; Catalin Hritcu; Exequiel Rivas; Antoine Van Muylder (Proc. ACM Program. Lang., 2020)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. - Carmine Abate; Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Catalin Hritcu; Kenji Maillard; Bas Spitters (CSF, 2021)

The Multiverse: Logical Modularity for Proof Assistants. - Kenji Maillard; Nicolas Margulies; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (CoRR, 2021)

A reasonably gradual type theory. - Kenji Maillard; Meven Lennon-Bertrand; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2022)

Gradualizing the Calculus of Inductive Constructions. - Meven Lennon-Bertrand; Kenji Maillard; Nicolas Tabareau; Éric Tanter (ACM Trans. Program. Lang. Syst., 2022)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. - Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Carmine Abate; Nikolaj Sidorenco; Catalin Hritcu; Kenji Maillard; Bas Spitters (ACM Trans. Program. Lang. Syst., 2023)

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

Definitional Functoriality for Dependent (Sub)Types. - Théo Laurent; Meven Lennon-Bertrand; Kenji Maillard (ESOP (1), 2024)

Artifact Description - Definitional Functoriality for Dependent (Sub)Types. - Théo Laurent; Meven Lennon-Bertrand; Kenji Maillard (ESOP (1), 2024)

Gradual Indexed Inductive Types. - Mara Malewski; Kenji Maillard; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2024)

All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. - Josselin Poiret; Gaëtan Gilbert; Kenji Maillard; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2025)

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