Gallinette

Gallinette is a joint team of Inria and of the Laboratory of Digital Science of Nantes (LS2N), co-located at IMT Atlantique and at the Faculty of Science.

Project

The Gallinette team aims at enabling a new generation of proof assistants, with the belief that practical experiments must go hand in hand with foundational investigations:

• We advance proof assistants both as certified programming languages and mechanised logical systems, via the integration of advanced programming and mathematical paradigms, notably dependent types and effects. We implement new programming and logical paradigms on top of Rocq by considering the latter as a target language for compilation.
• We extend the boundaries of the Curry-Howard correspondence beyond its currently-understood limits. A finer understanding of this correspondence will advance the foundations of programming languages and logic, and provide new methodologies essential to the development of proof assistants.

Extending the current capabilities of proof assistants is a kind of experimental endeavour, probing every aspect of the correspondence, from programming languages and type theory to proof theory, rewriting, and algebra.

News

• Mechanized Metatheory and Certified Compilation for The Rocq Prover

  Matthieu Sozeau (2026)

  Habilitation à Diriger des Recherches, Université de Nantes

  PDF Bibtex

• Confluence Techniques for Dependent Type Theory with Typed Conversion

  Thiago Felicissimo, Théo Winterhalter (2026)

  Preprint

  PDF Bibtex

• Cohomologically tropical varieties

  Edvard Aksnes, Omid Amini, Matthieu Piquerez, Kris Shaw (2025)

  Journal of the Institute of Mathematics of Jussieu

  PDF Bibtex

• In Cantor Space No One Can Hear You Stream

  Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot (2026)

  ESOP 2026 - 35th European Symposium on Programming and Systems

  PDF Bibtex

• Divide and Check: Logical Relations, No Algorithms Attached

  Josselin Poiret, Kenji Maillard, Nicolas Tabareau (2026)

  Preprint

  PDF Bibtex

• Definitional Proof Irrelevance Made Accessible

  Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, Théo Winterhalter (2026)

  Preprint

  PDF Bibtex

• Sulfur: a Reflective Tactic for Substitution Simplification

  Mathis Bouverot-Dupuis, Théo Winterhalter, Kathrin Stark, Kenji Maillard (2026)

  RocqPL 2026 - Rocq for Programming Languages

  PDF Bibtex

• Bounded Sort Polymorphism with Elimination Constraints

  Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter (2026)

  Proceedings of the ACM on Programming Languages

  PDF Bibtex

• Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting

  Thiago Felicissimo, Jean-Pierre Jouannaud (2025)

  30th International Conference on Automated Deduction

  PDF Bibtex

• S4 modal sequent calculus as intermediate logic and intermediate language

  Jean Caspar, Guillaume Munch-Maccagnoni (2026)

  PEPM 2026 - ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

  PDF Bibtex

• Encode the Cake and Eat it Too

  Yann Leray, Théo Winterhalter (2026)

  Proceedings of the ACM on Programming Languages

  PDF Bibtex

• Certifying the Decidability of the Word Problem in Monoids at Large

  Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D Mitchell, Finn Smith (2026)

  CPP 2026 - 15th ACM SIGPLAN International Conference on Certified Programs and Proofs

  PDF Bibtex

• Geometric Reasoning in Lean: from Algebraic Structures to Presheaves

  Yiming Xu, Kenji Maillard (2025)

  TYPES 2025 - 31st International Conference on Types for Proofs and Programs

  PDF Bibtex

• Upon This Quote I Will Build My Church Thesis

  Pierre-Marie Pédrot (2025)

  Communications of the ACM

  PDF Bibtex

• Linear Effects, Exceptions, and Resource Safety

  Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence (2026)

  ESOP 2026 - 35th European Symposium on Programming

  PDF Bibtex

• Classical notions of computation and the Hasegawa-Thielecke theorem

  Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni (2026)

  Proceedings of the ACM on Programming Languages

  PDF Bibtex

• AdapTT: Functoriality for Dependent Type Casts

  Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard (2026)

  Proceedings of the ACM on Programming Languages

  PDF Bibtex

• Nested Inductive Types

  Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, Nicolas Tabareau (2025)

  Preprint

  PDF Bibtex

• Babel-formal: Translation of Proofs between Lean and Rocq

  Théo Stoskopf, Cyril Cohen, Nicolas Tabareau (2025)

  The 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025

  PDF Bibtex

Team Leader

Nicolas Tabareau (Nicolas.Tabareau@Inria.fr)