kenji no uchi

Computer science & mathematics

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.

Info & Contact

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

Email: first name at last name dot blue

Publications & Pre-publications

Personal orcid

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

The slides of the presentation can be found here.


The slides are often updated versions, sometimes with major changes, of the original presentations


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

Various stuff

More stuff might come at some point