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
-
Definitional Proof-Irrelevance without K
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
Accepted at POPL 2019
-
Equivalences for Free
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Accepted at ICFP 2018, distinguished paper
-
A Classical Sequent Calculus with Dependent Types
Étienne Miquey
Accepted for TOPLAS special edition
-
Every λ-Term is Meaningful for the Infinitary Relational Model
Pierre Vial
Accepted at LICS 2018
-
A sequent calculus with dependent types for classical arithmetic
Étienne Miquey
Accepted at LICS 2018
-
Towards Certified Meta-Programming with Typed Template-Coq
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau
Accepted at ITP 2018
-
Formalizing Implicative Algebras in Coq
Étienne Miquey
Accepted at ITP 2018
Team Leader
Nicolas Tabareau (Nicolas.Tabareau@Inria.fr)