Bonjour, I’m a French Computer Science student at ENS de Lyon.

My academic interests are centered around type theory: their syntax, properties and semantics via the Curry-Howard-Lambek correspondance, and proof assistants: their usage, implementation and meta-theory. Check my detailed research interests and the research page for more information.

In my free time, I also like to promote and contribute to open-source softwares and to take part in programming contests (see: miscellaneous).

My (synthetic) resume (updated 09/2025) is available in english and en français.

Contact: johann [dot] rosain [at] ens-lyon [dot] org

Picture taken during the summer 2025, courtesy of Julie.

Detailed Research Interests

My main interest lies in type theory. I’d like to contribute in easing the usage of proof assistants via improving their type system. This is a subject that I’ve already worked on during my M2 internship, where I’ve implemented bounded sort polymorphism in Rocq, which allows users to avoid code duplication and makes proofs more robust. I’m also interested in homotopy type theory and (higher) observational type theory, that seem like good candidates to simplify the use of proof assistants.

With the same idea of having easier-to-use interactive provers, I’ve previously worked on the usage of automated theorem provers in proof assistants. In particular, I’m an active contributor of Goéland, a prover developed by Julie Cailler, for which I’ve taken over the maintenance in May 2025. Together with Julie and Olivier, we have developed and implemented in Goéland a strategy to translate (optimized) tableaux proofs to certified proofs (first in Rocq, then in Lambdapi).

I also like to formalize stuff, mostly in Rocq, and in my free time, I’m working on a library for free-variable tableaux proofs that aims at providing an efficient and certified proof checker.