Johann Rosain

Publications
Talks
Softwares
Activities
Miscellaneous

strange image

Bonjour, I'm a 4th year french student at ENS de Lyon in computer science, currently in a 4-months visit with Ambrus Kaposi in the Budapest Type Theory Group to work on a coherent syntax for type theory. I'll start a PhD in September under the supervision of Matthieu Sozeau in Nantes.

The academic program at ENS de Lyon focuses on research through experience, so I've previously visited some other places (from least recent to most recent): the LIRMM in Montpellier, the TYPES team in Gothenburg, the Gallinette team in Nantes and the PARTOUT team in Palaiseau, next to École Polytechnique.

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.

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: 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] For Generalised Algebraic Theories, Two Sorts Are Enough — Samy Avrillon, Ambroise Kaposi, Ambrus Lafont, Niyousha Najmaei, and Johann Rosain (2026).

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

^{[7] 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.}

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

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

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

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

Technical Reports

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

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

Talks

Bounded Sort Polymorphism With Elimination Constraints: At POPL 2026, 16 Jan. 2026 (video).
Extending SortPoly With Elimination Constraints in Rocq: At the Rocqshop 2025, 27 Sept. 2025 (video).
Theory and Metatheory of Elimination in Rocq: Master's 2 Internship Defense, 10 July 2025.
A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and Metarocq: At TYPES 2025, 13 June 2025 (video).
Extending Sort Polymorphism with Elimination Constraints: At TYPES 2025, 10 June 2025 (video).
Computational Difficulties in Cubical Type Theory: a Case Study: At the VeriDis Seminar, in LORIA, Nancy, 28 Oct. 2024.
On the Computation of Proof Terms in Homotopical Type Theory: Master's 1 Internship Defense, 4 Sept. 2024.
Deskolemisation in First-Order Logic: Optimisation and Certification (in French): Bachelor's Internship Defense, 5 Sept. 2023.
Do Integers Really Exist?: At the LIRMM PhD Seminar, Montpellier, 29 June 2023.

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.
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 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.