Kenji Maillard

According to our database, Kenji Maillard authored at least 18 papers between 2015 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Gradual Indexed Inductive Types.

Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter

Proc. ACM Program. Lang., 2024

Artifact Description - Definitional Functoriality for Dependent (Sub)Types.

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

Proceedings of the Programming Languages and Systems, 2024

Definitional Functoriality for Dependent (Sub)Types.

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

Proceedings of the Programming Languages and Systems, 2024

Martin-Löf à la Coq.

Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet

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

2023

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., September, 2023

2022

Gradualizing the Calculus of Inductive Constructions.

Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter

ACM Trans. Program. Lang. Syst., 2022

A reasonably gradual type theory.

Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter

Proc. ACM Program. Lang., 2022

2021

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

IACR Cryptol. ePrint Arch., 2021

The Multiverse: Logical Modularity for Proof Assistants.

Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter

CoRR, 2021

2020

The next 700 relational program logics.

Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder

Proc. ACM Program. Lang., 2020

2019

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

Kenji Maillard

PhD thesis, 2019

Dijkstra monads for all.

Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter

Proc. ACM Program. Lang., 2019

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

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

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

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

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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Dijkstra monads for free.

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2015

A Fibrational Account of Local States.

Kenji Maillard, Paul-André Melliès

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015