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.
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.
Nicolas Tabareau (Nicolas.Tabareau@Inria.fr)