Publications

Preprints

• For Generalised Algebraic Theories, Two Sorts Are Enough (arXiv)
  Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Niyousha Najmaei & Johann Rosain (January, 2026).

Conferences

1. Bounded Sort Polymorphism with Elimination Constraints (BibTeX | DOI | HAL | Artifact)
   Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter & Théo Winterhalter (January, 2026).
   In 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026).
2. A Generic Deskolemization Strategy (BibTeX | DOI | HAL)
   Johann Rosain, Richard Bonichon, Julie Cailler & Olivier Hermant (May, 2024).
   In 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-25).
3. Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (BibTeX | DOI | HAL)
   Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard & Hinde Lilia Bouziane (August, 2022).
   In 11th International Joint Conference On Automated Reasoning (IJCAR22).

Abstract and Workshops

1. A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and MetaRocq (abstract) (BibTeX)
   Johann Rosain, Matthieu Sozeau & Théo Winterhalter (June, 2025).
   In 31st International Conference on Types for Proofs and Programs (TYPES 2025) book of abstracts.
2. Extending Sort Polymorphism with Elimination Constraints (abstract) (BibTeX) Tomás Díaz, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau & Théo Winterhalter (June, 2025).
   In 31st International Conference on Types for Proofs and Programs (TYPES 2025) book of abstracts.
3. Extending Sort Polymorphism with Elimination Constraints in Rocq (abstract) (BibTeX) Tomás Díaz, Kenji Maillard, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter and Théo Winterhalter (September, 2025).
   At The Rocqshop 2025.

Talks

1. Bounded Sort Polymorphism With Elimination Constraints (Video)
   At POPL 2026, Rennes in January 2026.
2. Extending SortPoly With Elimination Constraints in Rocq (Video)
   At The Rocqshop 2025, Reykjavic in September 2025.
3. A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and Metarocq (Video)
   At TYPES2025, University of Strathclyde, Glasgow in June 2025.
4. Extending Sort Polymorphism with Elimination Constraints (Video)
   At TYPES2025, University of Strathclyde, Glasgow in June 2025.
5. Computational Difficulties in Cubical Type Theory: a Case Study
   At VeriDis Seminar, LORIA, Nancy in October 2024.
6. Do Integers Really Exist?
   At LIRMM Semindoc, LIRMM, Montpellier in June 2023.

Activities

• Subreviewer for the JFLA 2026.
• Volunteer student at ICGT 2022.

Theses and Internship Reports

• Theory and Metatheory of Elimination in Rocq (coming soon) (Slides)
  Johann Rosain (July, 2025).
  In this thesis, Rocq’s SortPoly type system is extended with bounded sort polymorphism. We show some properties on its metatheory, e.g., its consistency.
  The POPL 2026 paper Bounded Sort Polymorphism With Elimination Constraints is based on this work.
• Analyzing Proof Terms in Homotopical Type Theory: Toward Better Proofs (BibTeX | Slides)
  Johann Rosain (August, 2024).
  This report provides a computational analysis of Egbert Rijke’s proof of finiteness of finite structures up to isomorphism in HoTT.
• Skolemisation in First-Order Logic: Certification and Optimisation (BibTeX | Slides (in French))
  Johann Rosain (August, 2023).
  This report proposes a new algorithm to certify tableaux proofs with different Skolemisation techniques.
  This is the preliminary work that has led to LPAR-25’s article.

Softwares

I’ve contributed to the following softwares:

• Goéland – a first-order tableau concurrent automated theorem prover developped by Julie Cailler. I’ve mainly contributed by implementing efficient unification, deduction modulo theory, polymorphism and the deskolemization algorithm that led to the translation of its proofs in the languages of different proof assistants.
• postt – an implementation of cubical type theory by Jonas Höfer and Thierry Coquand that allows the analysis of proofs. I’ve contributed a part of the standard library of the tool that includes the proof of homotopy finiteness, i.e., the counting of structures up to isomorphism.
• Rocq – the well-known proof assistant based on the polymorphic cumulative calculus of inductive constructions. I have worked on adding elimination constraints that allow, for instance, to derive the most general elimination principle.

Others

Some useful documents, here (mostly) for my own convenience.

• Handling Bound Variables via De Bruijn’s Indices
• Decidable Equality Implies UIP, the Easy Way