Publications

Conferences

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 (TYPES2025) 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 (TYPES2025) book of abstracts.
3. A Generic Deskolemization Strategy (BibTeX | DOI)
   Johann Rosain, Richard Bonichon, Julie Cailler & Olivier Hermant (May, 2024).
   In 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-25).
4. Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (BibTeX | DOI)
   Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard & Hinde Lilia Bouziane (August, 2022).
   In 11th International Joint Conference On Automated Reasoning (IJCAR22).

Talks

1. A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and Metarocq
   At TYPES2025, University of Strathclyde, Glasgow in June 2025.
2. Extending Sort Polymorphism with Elimination Constraints
   At TYPES2025, University of Strathclyde, Glasgow in June 2025.
3. Computational Difficulties in Cubical Type Theory: a Case Study
   At VeriDis Seminar, LORIA, Nancy in October 2024.
4. Do Integers Really Exist?
   At LIRMM Semindoc, LIRMM, Montpellier in June 2023.

Reports

• 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’m in the process of 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