معرفی
Kenji Maillard is a junior researcher (Inria Starting Faculty Position) at Inria Rennes, affiliated with the Gallinette team and LS2N at Université de Nantes, France. He has been in this role since December 2022, following a postdoctoral fellowship in the same group under Nicolas Tabareau and Éric Tanter.
- PhD: ENS Ulm and Inria Paris (2019)
- Supervisor: Cătălin Hrițcu
- Thesis: Principles of Program Verification For Arbitrary Monadic Effects
Kenji's research lies at the intersection of computer science and mathematics, focusing on programming languages, proof assistants, and formal methods. His work spans the metatheory of dependent type systems—leveraging category theory, homotopy theory, and model theory—as well as their verified implementation in proof assistants like Coq. He is particularly interested in gradual typing for dependent types, logical modularity, and the formalization of mathematical reasoning.
His recent publications reflect a consistent focus on advancing type theory and verification frameworks. Key themes include gradualization of the Calculus of Inductive Constructions, indexed inductive types, sort polymorphism, and the integration of logical and computational principles in proof assistants. These works contribute to making formal verification more scalable and accessible.
Kenji is an active contributor to the programming languages community, serving on program committees for POPL, ICFP, CPP, and other top-tier venues. He advocates for open access in academic publishing and maintains a strong public presence through his website, GitHub, and presentations.
- Member, POPL Program Committee (2026)
- PC Member, ICFP, OOPSLA, CPP, CoqPL
- Artifact Evaluation Committee, PLDI, POPL
He has collaborated extensively with researchers such as Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter, and others. His work is primarily conducted within the Gallinette team at Inria, which focuses on the foundations and applications of proof assistants and type theory.
