I am mostly interested in programming languages, logic, category theory and geometric insights on these subjects as can be given by algebraic topology and algebraic geometry.
I am currently doing 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, 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.
My name is Kenji Maillard, written unofficially 賢士. My CV is here to find out more.
Email: first name at last name dot blue
The formal development is accessible on github
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.
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
I really like cooking, in particular french and japanese cuisine !