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

• Impredicative Observational Equality

  Loïc Pujet, Nicolas Tabareau (2023)

  POPL 2023 - 50th ACM SIGPLAN Symposium on Principles of Programming Languages

• A Reasonably Gradual Type Theory

  Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter (2022)

  Proceedings of the ACM on Programming Languages

• Russian Constructivism in a Prefascist Theory

  Pierre-Marie Pédrot

  LICS 2020

• Competing inheritance paths in dependent type theory: a case study in functional analysis

  Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi

  IJCAR 2020

• The Fire Triangle

  Pierre-Marie Pédrot, Nicolas Tabareau

  POPL 2020

• SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References

  Guilhem Jaber

  POPL 2020

• Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq

  Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter

  POPL 2020

• Reduction Monads and Their Signatures

  Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

  POPL 2020

Team Leader

Nicolas Tabareau (Nicolas.Tabareau@Inria.fr)