@inproceedings{DBLP:conf/cade/CaillerRDRB22,
	author = {Julie Cailler and
                  Johann Rosain and
                  David Delahaye and
                  Simon Robillard and
                  Hinde{-}Lilia Bouziane},
	editor = {Jasmin Blanchette and
                  Laura Kov{\'{a}}cs and
                  Dirk Pattinson},
	title = {Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)},
	booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
                  2022, Haifa, Israel, August 8-10, 2022, Proceedings},
	series = {Lecture Notes in Computer Science},
	pages = {359--368},
	publisher = {Springer},
	year = {2022},
	url = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03793406v1/document},
	doi = {10.1007/978-3-031-10769-6_22},
	timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
	biburl = {https://dblp.org/rec/conf/cade/CaillerRDRB22.bib},
	bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/RosainC26,
	author = {Johann Rosain and Julie Cailler},
	editor = {Ekateina Komendantskaya and Tobias Nipkow},
	title = {{TableauxRocq}: A Deep Embedding of Free-Variable Tableaux in Rocq},
	booktitle = {17th International Conference on Interactive Theorem Proving, {ITP}
                  2026, Lisbon, Portugal, July 26-29, 2026},
	series = {LIPIcs},
	pages = {13:1--13:22},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
	year = {2026},
	url = {https://arxiv.org/pdf/2605.16952},
	timestamp = {Tue, 26 May 2026 14:19:35 +0100},
	bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lpar/RosainBCH24,
	author = {Johann Rosain and
                  Richard Bonichon and
                  Julie Cailler and
                  Olivier Hermant},
	editor = {Nikolaj S. Bj{\o}rner and
                  Marijn Heule and
                  Andrei Voronkov},
	title = {A Generic Deskolemization Strategy},
	booktitle = {{LPAR} 2024: Proceedings of 25th Conference on Logic for Programming,
                  Artificial Intelligence and Reasoning, Port Louis, Mauritius, May
                  26-31, 2024},
	series = {EPiC Series in Computing},
	pages = {246--263},
	publisher = {EasyChair},
	year = {2024},
	url = {https://easychair.org/publications/paper/VgpS/open},
	doi = {10.29007/G1TM},
	timestamp = {Tue, 05 Aug 2025 22:41:07 +0200},
	biburl = {https://dblp.org/rec/conf/lpar/RosainBCH24.bib},
	bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-2601-19426,
	author = {Samy Avrillon and
                  Ambrus Kaposi and
                  Ambroise Lafont and
                  Niyousha Najmaei and
                  Johann Rosain},
	title = {For Generalised Algebraic Theories, Two Sorts Are Enough},
	volume = {abs/2601.19426},
	year = {2026},
	url = {https://arxiv.org/pdf/2601.19426},
	doi = {10.48550/ARXIV.2601.19426},
	eprinttype = {arXiv},
	eprint = {2601.19426},
	timestamp = {Thu, 26 Feb 2026 09:55:24 +0100},
	biburl = {https://dblp.org/rec/journals/corr/abs-2601-19426.bib},
	bibsource = {dblp computer science bibliography, https://dblp.org},
	keywords = {preprint}
}

@article{DBLP:journals/pacmpl/RosainDMSTTW26,
	author = {Johann Rosain and
                  Tom{\'{a}}s D{\'{i}}az and
                  Kenji Maillard and
                  Matthieu Sozeau and
                  Nicolas Tabareau and
                  {\'{E}}ric Tanter and
                  Th{\'{e}}o Winterhalter},
	title = {Bounded Sort Polymorphism with Elimination Constraints},
	journal = {{POPL} 2026: Proceedings of the 53rd Conference on the Principle of Programming Languages, Rennes, France, January 14-16, 2026},
	volume = {10},
	number = {{POPL}},
	pages = {2614--2642},
	year = {2026},
	url = {https://dl.acm.org/doi/pdf/10.1145/3776732},
	doi = {10.1145/3776732},
	timestamp = {Tue, 03 Feb 2026 08:26:31 +0100},
	biburl = {https://dblp.org/rec/journals/pacmpl/RosainDMSTTW26.bib},
	bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Misc{DBLP:misc/rocqshop/DiazMRSTTW25,
	url = {https://coq-workshop.gitlab.io/2025/files/EA8.pdf},
	year = {2025},
	journal = {The Rocqshop 2025},
	title = {Extending Sort Polymorphism with Elimination Constraints in Rocq},
	author = {Tom{\'{a}}s D{\'{i}}az and Kenji Maillard and Johann Rosain and Matthieu Sozeau and Nicolas Tabareau and {\'{E}}ric Tanter and Th{\'{e}}o Winterhalter}
}

@Misc{DBLP:misc/types/AvrillonKLNR26,
	url = {https://types2026.cse.chalmers.se/abstracts/27.pdf},
	year = {2026},
	title = {For Generalised Algebraic Theories, Two Sorts Are Enough},
	author = {Samy Avrillon and Ambroise Kaposi and Ambrus Lafont and Niyousha Najmaei and Johann Rosain},
	journal = {32nd International Conference on Types for Proofs and Programs}
}

@Misc{DBLP:misc/types/DiazRSTW25,
	url = {https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper47.pdf},
	year = {2025},
	title = {Extending Sort Polymorphism with Elimination Constraints},
	author = {Tom{\'{a}}s D{\'{i}}az and Johann Rosain and Matthieu Sozeau and Nicolas Tabareau and Th{\'{e}}o Winterhalter},
	journal = {31st International Conference on Types for Proofs and Programs}
}

@Misc{DBLP:misc/types/RosainSW25,
	url = {https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper81.pdf},
	year = {2025},
	title = {A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and MetaRocq},
	author = {Johann Rosain and Matthieu Sozeau and Th{\'{e}}o Winterhalter},
	journal = {31st International Conference on Types for Proofs and Programs}
}

@TechReport{DBLP:report/ensl/Rosain24,
	institution = {ENS de Lyon},
	year = {2024},
	title = {Analyzing Proof Terms in Homotopical Type Theory: Toward Better Proofs},
	author = {Johann Rosain},
	url = {content/tech-reports/m1-proof-terms.pdf},
}

@TechReport{DBLP:report/ensl/Rosain23,
	institution = {ENS de Lyon},
	year = {2023},
	title = {Skolemisation in First-Order Logic: Certification and Optimisation},
	author = {Johann Rosain},
	url = {content/tech-reports/bachelor-deskolemisation.pdf},
}