Gallinette is a joint team of Inria and of the Laboratory of Digital Science of Nantes (LS2N), colocated 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 CurryHoward correspondence beyond its currentlyunderstood 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 LennonBertrand, Nicolas Tabareau, Éric Tanter (2022)
Proceedings of the ACM on Programming Languages

Russian Constructivism in a Prefascist Theory
PierreMarie 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
PierreMarie Pédrot, Nicolas Tabareau
POPL 2020

SyTeCi: Automating Contextual Equivalence for HigherOrder 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)