- HAL publications
GALLINETTE Research team
Gallinette: developing a new generation of proof assistants
- Leader : Nicolas Tabareau
- Type : Project team
- Research center(s) : Rennes
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Proofs and Verification
- Partner(s) : Université Nantes,IMT Atlantique Bretagne-Pays de la Loire
- Collaborator(s) : Laboratoire des Sciences du numerique de Nantes (UMR6004)
- The goal is to advance proof assistants both as certified programming languages and mechanised logical systems. Advanced programming and mathematical paradigms must be integrated, notably dependent types and effects. The distinctive approach is to implement new programming and logical paradigms on top of Coq by considering the latter as a target language for compilation.
- The aim of foundational investigations is to extend the boundaries of the Curry-Howard correspondence. It is seen both as providing foundations for programming languages and logic, and as a purveyor of techniques essential to the development of proof assistants. Under this perspective, the development of proof assistants is seen as a total experiment using the correspondence in every aspect: programming languages, type theory, proof theory, rewriting and algebra.
1. Enhance the computational and logical power of proof assistants
The democratization of proof assistants based on Type Theory suffers from a major drawback, the mismatch between the conception of equality in mathematics and equality in Type Theory. Indeed, some basic principles that are used implicitly in mathematics—such as Church’s principle of propositional extensionality, which says that two propositions are equal when they are logically equivalent—are not derivable in Type Theory. More problematically from a computer science point of view, the basic concept of two functions being equal when they are equal at every “point” of their domain is also not derivable and need to be set as an axiom. Of course, those principles are consistent with Type Theory and their addition as axioms is safe. But any development using them in a definition will produce a piece of code that does not compute, being stuck at points where axioms have been used, because axioms are computational black boxes.
We propose to investigate how expressive logical transformations (such as forcing, sheafification, …) could be used to enhance the computational and logical power of proof assistants—with a particular insight on an integration to the Coq proof assistant through effective translations (or compilation phases). One of the main aspect, in connection to the ERC project CoqHoTT is the integration of new concepts showing up around Homotopy Type Theory such as univalence, or higher inductive types.
2. Effects in type theory
We propose to incorporate effects in the theory of proof assistants. We notice that at stake is not only the certification of programs with effects, but that it has also implications in semantics and logic.
Type theory is based on the lambda calculus which is purely functional. Noticing that any realistic program contains effects (state, exceptions, input-output…), many works are focusing on certified programming with effects: notably Ynot, and more recently F* and Idris, which propose various ways for encapsulating effects and restricting the dependency of types on effectful terms. Effects are either specialised, with monads with Hoare-style pre- and post-conditions found in Ynot or F*, or more general, with algebraic effects implemented in Idris. There is on the other hand a deficit of logical and semantic investigations.
Yet, a type theory that integrates effects would have logical, algebraic and computational implications through the Curry-Howard correspondence. For instance, effects such as delimited control operators provide computational interpretations to axioms such as A ≅ ¬¬A and ¬∀xA ≅ ∃x¬A, in contrast with the usual type theory which considers that classical logic is non-constructive. A whole literature on the constructive contents of classical proofs is to be explored and integrated.
The goal is to develop a type theory with effects that accounts both for practical experiments in certified programming, and for clues from denotational semantics and logical phenomena, starting from the unifying setting of (linear) call-by-push-value.
3. Improving the interconnection between proof assistants and mainstream programming languages
We propose to internalize concepts found in mainstream programming languages, like objects, within proof assistants, in order to provide a better integration with common practice in the industry. By internalization, we mean a shallow embedding of (part of) mainstream programming languages in order to be able to certify and synthesise programs written in these languages directly inside proof assistants.
But there is a gap between the programming paradigm underlying the Curry-Howard correspondence, pure functional programming, and the dominant programming paradigm for writing software applications in industry, notably object-oriented programming. One of the main issue with the internalization approach is that type theory is constrained by a strict type discipline which is often more flexible if not absent in mainstream language. To address this issue, the Gallinette team will put strong efforts on the development of gradual typing in type theory to allow progressive integration of code that comes from a more permissive world. Also, to enable the interconnection, we plan to develop dependent interoperability to marry dependent types as present in type theory and simple types with properties as present in mainstream languages. More generally, the internalisation will provide a common framework to express a series of oppositions:
- object-oriented programming versus functional programming,
- object polymorphism versus parametric polymorphism,
- interoperability versus intra-operability,
- procedural data abstraction versus abstract data types,
- subsumptive subtyping versus coercive subtyping ,
- co-algebraic interpretations versus algebraic ones.
International and industrial relations
ERC Starting Grant CoqHoTT (http://coqhott.gforge.inria.fr/)
Research teams of the same theme :
- ANTIQUE - Static Analysis by Abstract Interpretation
- CELTIQUE - Software certification with semantic analysis
- CONVECS - Construction of verified concurrent systems
- DEDUCTEAM - DEDUCTEAM
- GALLIUM - Programming languages, types, compilation and proofs
- MARELLE - Mathematical, Reasoning and Software
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- MOCQUA - Designing the Future of Computational Models
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- SUMO - SUpervision of large MOdular and distributed systems
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems