Computer sciences & mathematics

I spend most of my time thinking, studying and hacking dependent type theories. On their metatheoretical aspects, involving category theory, homotopy theory and model theory for dependent types. On the pratical aspects of their verified implementation in proof assistants. On their use as frameworks for theorem provers in order to formalize elegant mathematical proofs.

The somewhat mysterious reasoning principles ruling over side-effects in programming languages has been and remain my motivating quest in this journey at the edge of computer sciences and mathematics.

I am currently a junior researcher (ISFP) in the team Gallinette at Inria Rennes located in Nantes.

Info & Contact

My name is Kenji Maillard, written unofficially 賢士. My CV is here to find out more.

Drafts and submitted articles

• The Multiverse: Logical Modularity for Proof Assistants Nicolas Marguliès, Mathieu Sozeau, Nicolas Tabareau and Éric Tanter

Publications

• Gradual Indexed Inductive Types Mara Malewski, Nicolas Tabareau and Éric Tanter Published at ICFP'24.

• Definitional Functoriality for Dependent (Sub)Types Théo Laurent and Meven Lennon-Bertrand Published at ESOP'24.

• Martin-löf à la Coq A. Adjedj, M. Lennon-Bertrand, P.-M. Pédrot and L. Pujet Published at CPP'24. Repository of the development.

• A Reasonably Gradual Type Theory Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter Published and presented at ICFP'22

• Gradualizing the Calculus of Inductive Constructions Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter Published in TOPLAS, presented at POPL'22

• SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq C. Abate, P. G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Hriţcu and B. Spitters Presented and published at CSF'21

  The formal development is accessible on github

• Mettons de l'ordre dans CIC ! Théo Laurent (presented at JFLA 21, in French)

  A short abstract presenting a work in progress program to develop ordered syntactic models of the Calculus of Constructions. The formal development corresponding to the note is available here.

• On relational verification for monadic programs Cătălin Hriţcu, Exequiel Rivas and Antoine Van Muylder Presented and published at POPL'20

• Dijkstra Monads for All D. Ahman, R. Atkey, G. Martinez, C. Hriţcu, E. Rivas, É. Tanter Presented and published at ICFP'19

• Recalling a Witness: monotonic state in F* D. Ahman, C. Fournet, C. Hritcu, A. Rastogi, N. Swamy Presented and published at POPL'18

• Monadic reification in F* N. Grimm, C. Fournet, C. Hriţcu, M. Maffei, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy, S. Zanella-Béguelin Presented and published at CPP'18

• Dijkstra Monads for Free D. Ahman, C. Hriţcu, G. Martinez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy Presented and published at POPL'17

• A Fibrational Account of Local States Paul-André Mèllies Presented and published at LICS'15

Presentations

• On gradual indexed inductive types (slides - ICFP'24, Sep. 24)
• On a mechanized logical relation for MLTT in Coq (presentation at TYPES'23, Jun 2023)
• On investigation of boolean extensionality in intensional type theory (presentation at GT Scalp'22, Feb 2023; presentation at LHC'24 ; presentation at Types'24)
• On gradual dependent type theories: presentation at gdt Plume, Dec 2021; presentation at Types'22, June 2022; presentation at ICFP'22, Sep 2022)
• On syntactic models of CIC (slides presented at LHC 21)
• On Dijkstra monads (slides - GT Scalp 18, Prosecco Seminar (Dec. 18), Eutypes 19)
• On μ̃μ (slides - at Gallium Seminar (Oct. 18) - small variation on Gabriel's HOPE'18 presentation)
• On the F* language (slides - GeoCal-Lac 17, ChoCoLa (Dec. 17), Eutypes 18)
• On the local state monad (slides - Gallium seminar, Sep. 2015)

News from the days of yore

Between December 2019 and November 2022, I did a post-doc at Gallinette, Inria Rennes with Nicolas Tabareau and Éric Tanter around dependent types, universes and effects (with gradual stuff interleaved).

Before that (October 2016 - November 2019), I worked under the supervision of Cătălin Hriţcu around the programming language F* (and more precisely Dijkstra Monads - see publications for details or this PhD manuscript) in the team Prosecco, at Inria Paris and also spent some time torturing robots at Mujin.

Thèse de doctorat (PhD)

I prepared my PhD under the supervision of Cătălin Hriţcu at ENS Ulm and team Prosecco, Inria Paris on Principles of Program Verification For Arbitrary Monadic Effects. I defended on November 25th, 2019 at Inria, Paris in front of a jury composed by

• President: Hugo Herbelin
• Reviewer: Shin-Ya Katsumata
• Reviewer: Bas Spitters
• Examiner: Robert Atkey
• Examiner: Gilles Barthe
• Examiner: Pierre-Évariste Dagand
• Examiner: Christine Paulin-Mohring
• Examiner: Nicolas Tabareau
• Advisor: Cătălin Hriţcu

Cooking

I really like cooking, in particular french and japanese cuisine !

Various stuff

• I strongly support open-access, and pledged to review only for conferences and journals with open-access proceedings
• a short article on excluded-middle in type theory (in French) posted on Gallinette's blog