Kenji Maillard

31 papers A* 2A 1B 2Journal 22Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
AdapTT: Functoriality for Dependent Type Casts.
Proc. ACM Program. Lang.
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard
2026 J jnl
Bounded Sort Polymorphism with Elimination Constraints.
Proc. ACM Program. Lang.
Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter
2025 J jnl
AdapTT: Functoriality for Dependent Type Casts.
CoRR
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard
2025 J jnl
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants.
Proc. ACM Program. Lang.
Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2025 J jnl
Incremental Certified Programming.
Proc. ACM Program. Lang.
Tomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2024 — conf
Artifact Description - Definitional Functoriality for Dependent (Sub)Types.
ESOP (1)
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
2024 — conf
Definitional Functoriality for Dependent (Sub)Types.
ESOP (1)
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
2024 J jnl
Gradual Indexed Inductive Types.
Proc. ACM Program. Lang.
Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2024 B conf
Martin-Löf à la Coq.
CPP
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
2023 J jnl
Definitional Functoriality for Dependent (Sub)Types.
CoRR
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
2023 J jnl
Martin-Löf à la Coq.
CoRR
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
2023 J jnl
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
ACM Trans. Program. Lang. Syst.
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
2022 J jnl
A Reasonably Gradual Type Theory.
CoRR
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
2022 J jnl
A reasonably gradual type theory.
Proc. ACM Program. Lang.
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
2022 J jnl
Gradualizing the Calculus of Inductive Constructions.
ACM Trans. Program. Lang. Syst.
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2021 A conf
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
CSF
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
2021 J jnl
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
IACR Cryptol. ePrint Arch.
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
2021 J jnl
The Multiverse: Logical Modularity for Proof Assistants.
CoRR
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2020 J jnl
Gradualizing the Calculus of Inductive Constructions.
CoRR
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2020 J jnl
The next 700 relational program logics.
Proc. ACM Program. Lang.
Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder
2019 J jnl
Dijkstra Monads for All.
CoRR
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
2019 J jnl
Dijkstra monads for all.
Proc. ACM Program. Lang.
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
2019 — —
Principles of Program Verification for Arbitrary Monadic Effects. (Principes de la Vérification de Programmes à Effets Monadiques Arbitraires).
Kenji Maillard
2019 J jnl
The Next 700 Relational Program Logics.
CoRR
Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder
2018 B conf
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.
CPP
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2018 J jnl
Recalling a witness: foundations and applications of monotonic state.
Proc. ACM Program. Lang.
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2017 J jnl
A Monadic Framework for Relational Verification (Functional Pearl).
CoRR
Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2017 A* conf
Dijkstra monads for free.
POPL
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2017 J jnl
Recalling a Witness: Foundations and Applications of Monotonic State.
CoRR
Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2015 A* conf
A Fibrational Account of Local States.
LICS
Kenji Maillard, Paul-André Melliès