Johann Rosain

Publications
Talks
Teaching
Softwares
Activities
Miscellaneous

strange image

Bonjour, I'm Johann Rosain, a french PhD student at the Gallinette INRIA team, affiliated with the LS2N at Nantes Université. I'm supervised by Matthieu Sozeau and Nicolas Tabareau, and I'm working on improving sort and universe polymorphism in the Rocq proof assistant and MetaRocq.

Previously, I was a student at ENS de Lyon, which has a formation that focuses on research through experience, so I've been to many great places for short-term research stays (between two and six months). From my least recent stay to my most recent one, I've been to: the LIRMM in Montpellier, the TYPES team in Gothenburg, the Gallinette team in Nantes, the PARTOUT team in Palaiseau, next to École Polytechnique, and the Budapest Type Theory Group.

Everything is detailed in my resume (updated 05/2026).

If you wish to contact me, please use the following (permanent) address: (λxy. x.y@ens-lyon.org) johann rosain. It is a redirect-only mailbox that points to my current institution's address.

Picture taken by my personal photographer, Julie, in summer 2025.

Publications

This section is automatically generated using a BibTeX file (where most entries originate from dblp) together with a custom CSL style (that you can find here). Feel free to steal everything that you may need. For a more complete workflow, you can find the sources of this website on my codeberg.

Preprints

^{[1] For Generalised Algebraic Theories, Two Sorts Are Enough — Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Niyousha Najmaei, and Johann Rosain (2026).}

In Conferences

^{[2] TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq — Johann Rosain and Julie Cailler (2026).

In: The 17th International Conference on Interactive Theorem Proving (ITP 2026), Lisbon, Portugal, July 26-29, 2026.}

^{[3] Bounded Sort Polymorphism with Elimination Constraints — Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter (2026).

In: POPL 2026: Proceedings of the 53rd Conference on the Principle of Programming Languages, Rennes, France, January 14-16, 2026.}

^{[4] A Generic Deskolemization Strategy — Johann Rosain, Richard Bonichon, Julie Cailler, and Olivier Hermant (2024).

In: LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024.}

^{[5] Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) — Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, and Hinde-Lilia Bouziane (2022).

In: Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings.}

Extended Abstracts & Workshops

^{[6] Towards Robust Programming Interfaces in Rocq — Johann Rosain (2026).

In: The Rocqshop 2026.}

^{[7] For Generalised Algebraic Theories, Two Sorts Are Enough — Samy Avrillon, Ambroise Kaposi, Ambrus Lafont, Niyousha Najmaei, and Johann Rosain (2026).

In: The 32nd International Conference on Types for Proofs and Programs.}

^{[8] Extending Sort Polymorphism with Elimination Constraints in Rocq — Tomás Díaz, Kenji Maillard, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter (2025).

In: The Rocqshop 2025.}

^{[9] A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and Metarocq — Johann Rosain, Matthieu Sozeau, and Théo Winterhalter (2025).

In: The 31st International Conference on Types for Proofs and Programs.}

^{[10] Extending Sort Polymorphism with Elimination Constraints — Tomás Díaz, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter (2025).

In: The 31st International Conference on Types for Proofs and Programs.}

Technical Reports

^{[11] Analyzing Proof Terms in Homotopical Type Theory: Toward Better Proofs — Johann Rosain (2024).}

^{[12] Skolemisation in First-Order Logic: Certification and Optimisation — Johann Rosain (2023).}

Talks

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq: At ITP 2026, Lisbon, Portugal, 28 July 2026. (slides)
RocqInterface: Robust Programming Interfaces in Rocq: At the Rocqshop 2026, Lisbon, Portugal, 25 July 2026. (slides)
For Generalized Algebraic Theories, Two Sorts Are Enough: At the Budapest Type Theory seminar, Budapest, Hungary, 01 July 2026. (notes)
Bounded Sort Polymorphism With Elimination Constraints: At POPL 2026, Rennes, France, 16 Jan. 2026. (slides, video)
At the Rocqshop 2025, Reykjavik, Iceland (online), 27 Sept. 2025. (slides, video)
Master's 2 Internship Defense, Lyon, France, 10 July 2025. (slides)
At TYPES 2025, Glasgow, Scotland, 10 June 2025. (slides, video)
A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and Metarocq: At TYPES 2025, Glasgow, Scotland, 13 June 2025. (slides, video).
On the Computation of Proof Terms in Homotopical Type Theory: At the VeriDis Seminar, in LORIA, Nancy, France, 28 Oct. 2024. (slides)
Master's 1 Internship Defense, Lyon, France, 4 Sept. 2024. (slides)
Deskolemisation in First-Order Logic: Optimisation and Certification: Bachelor's Internship Defense, Lyon, France, 5 Sept. 2023. (slides, in French)
Do Integers Really Exist?: At the LIRMM PhD Seminar, Montpellier, France, 29 June 2023. (slides)

Teaching

I'm a teaching assistant at Nantes Université. I am in charge of:

Tutorials of Theory of Programming Languages (3rd-year bachelor course, 2026-2027). Course coordinator: Guilhème Jaber. In order to train the students' redaction skill, I have written some additional exercise sheets (in French):
- Feuille d'exercice sur les relations binaires.
- Correction de l'exercice 6 du TD 1 et exercices sur les propriétés des infs et lubs discutées en classe.
Practicals of Functional Programming (3rd-year bachelor course, 2026-2027). Course coordinator: Guilhème Jaber.

Softwares

I'm the author of the following projects:

TableauxRocq — a Rocq library that provides a deep embedding of free-variable tableaux together with a fully certified fast proof checker, POULET.
Rocq-Interface — a small Rocq plugin that enables abstract programming interfaces, even in the presence of dependent types.
sd-mode.el — an emacs mode that interacts with Damien Pous's tool to vizualize string diagram.
dmanager — a lightweight document manager inspired of pass.

I've contributed to the following projects:

Goéland — a first-order tableau-based automated theorem prover developped by Julie Cailler. I've implemented many features and I've been maintaining this project since May 2025.
Rocq — the well-known proof assistant based on dependent types. I've mainly implemented the kernel algorithms of elimination constraints.
postt — an implementation of Cubical Type Theory modeled by presheaves over partially ordered sets by Jonas Höfer. I've contributed most of the mechanized library.

Activities

Article Reviews: Sub-reviewer for the 35th EACSL Annual Conference on Computer Science Logic (CSL 2027).
Sub-reviewer for the Journées Francophones des Langages Applicatifs 2026 (JFLA 2026).
Volonteer Student: In The 11th International Colloquium on Graph Theory and Combinatorics (ICGT 2022).

Miscellaneous

Are you interested in a 6-lines proof that having decidable equality implies UIP? If so, go read my post Decidable Equality implies UIP, the Easy Way. If not, then you should really be interested in such a proof; who in their right mind is not?

I'm also a yearly devoted participant to the advent of code, which proposes some small algorithmic puzzles at the start of the month of December. My solutions in different languages (depending on the mood of the year) can be found here.

I'm a very enthusiastic supporter of the FLOSS philosophy and I think that most (if not all) proprietary software are malwares. If you don't, please read Richard Stallman's post on the principles of free software. Also, recall that free and open software are at the basis of all (even proprietary) systems.

Of course, this means that I give up GitHub as much as I can. There are great alternatives out there (I'm using codeberg, but there are many ethical forgejo instances with open registrations out there).

No GenAI

This also means that I'm against GenAI. Besides its widespread usage by students, which is really harmful for the overall literacy of the youth, and ignoring the ethical and moral issues that arise from the use of generative AI, they are the antithesis of the FLOSS philosophy—even for open-source ones. Consequently, I'm a signatory of the manifeste d’objection de conscience face à l’IA générative, which is a french text underlining some of the issues introduced by GenAIs.

You can find me on Google Scholar, ORCID, codeberg and GitHub.