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.

Publications & Pre-publications

• 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 the F* language (slides - GeoCal-Lac 17, ChoCoLa (Dec. 17), Eutypes 18)
• On μ̃μ (slides - at Gallium Seminar (Oct. 18) - small variation on Gabriel's HOPE'18 presentation)
• On Dijkstra monads (slides - GT Scalp 18, Prosecco Seminar (Dec. 18), Eutypes 19)
• On syntactic models of CIC (slides presented at LHC 21)
• On gradual dependent type theories: presentation at gdt Plume, Dec 2021; presentation at Types'22, June 2022; presentation at ICFP'22, Sep 2022)
• On investigation of boolean extensionality in intensional type theory (presentation at GT Scalp'22, Feb 2023)

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