GECO GECO

The GECO associate team

Gradual verification and robust proof Engineering for COq

Inria associate team (2018-2020)

INRIA INRIA





GECO in a nutshell


GECO is an Inria associate team between the Gallinette team in Inria Nantes and the Pleiad lab of the University of Chile, whose goal is to support and advance the state-of-the-art of certified software engineering in Coq by providing more convenient tools and mechanisms to programmers.
GECO is also involved in the Chilean-funded CSEC project (2018-2019), in partnership with Inria Chile.

The GECO team

Members of the team (French side)

Xavier Montillet PhD Student

Pierre-Marie Pédrot Permanent member

Matthieu Sozeau Permanent member

Nicolas Tabareau Permanent member

Members of the team (Chilean side)

Hans Fehrmann Master student

Ismael Figueroa Permanent member

Federico Olmedo Permanent member

Éric Tanter Permanent member

Matías Toro PhD student


Activities and Results

Visits

  • Nicolas Tabareau will visit Pleiad (UChile) in March 2019.
  • Matias Toro will visit Gallinette (Inria Nantes) and PiR2 (Inria Paris) in January 2019.
  • Éric Tanter has visited Gallinette (Inria Nantes) in August 2018.
  • Kickoff meeting of the GECO/CSEC projects, held at University of Chile, March 2018.
    All French members attended and have visited Pleiad (UChile) for one or two weeks.

Publications

Software

  • 
The ICFP’18 publication comes with a Coq library (link) which as been certified as a valuable artifact by the Artifact Evaluation Committee of ICFP’18. This is joint work of Matthieu Sozeau (Inria Paris), Nicolas Tabareau (Inria Nantes) and Éric Tanter (UChile). This constitutes a major advancement for Objective 3 of the project.

  • 
We are working on the implementation of a consistent version of Exceptional Type Theory [ESOP’18]. This implementation has been started by Pierre-Marie Pédrot (Inria Nantes) and has been mostly pursued by Hans Fehrmann (UChile). The implementation is a work in progress and can be found on GitHub. The is part of Objective O1 (link).

Description of the project


The development of tools to construct software systems that respect a given specification is a major challenge of current and future research in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their effectiveness to prove correctness of important pieces of software like the C compiler of the CompCert project. Certified programming with dependent types is attracting a lot of attention recently, and Coq is the de facto standard for such endeavors, with an increasing amount of users, pedagogical material, and large-scale projects. Nevertheless, significant work remains to be done to make Coq more usable from a software engineering point of view. This collaboration project gathers the expertise of researchers from Chile (Inria Chile, Universidad de Chile, Universidad Católica de Valparaíso) and France (Inria Nantes, Inria Paris), in different areas that are crucial to develop the vision of certified software engineering. The focus of this project is both theoretical and practical, covering novel foundations and methods, design of concrete languages and tools, and validation through specific case studies. The end result will be a number of enhancements to the Coq proof assistant (frameworks, tactic language) together with guidelines and demonstrations of their applicability in realistic scenarios.

Research Topics

  • O1: Foundations and practice of gradual verification.
    On the way to full verification, programmers can take advantage of a gradual approach in which some properties are simply asserted instead of proven, subject to dynamic verification. Tabareau and Tanter have made preliminary progress in this regard [DLS’15], which suffers from a number of limitations, the most important being the way to integrate the possibility for runtime errors within Coq. Instead of relying on axioms, this project will explore the application of a recent technique by Pédrot and Tabareau [LICS’17] to embed effects in Coq. This will yield new foundations of gradual certified programming, both more expressive and practical. We will also study how to integrate that technique with the extraction mechanism of Coq programs to OCaml, in order to exploit the exception mechanism of OCaml.
    • [DLS’15] Éric Tanter, Nicolas Tabareau. Gradual certified programming in Coq. DLS 2015: 26-40
    • [LICS’17] Pierre-Marie Pédrot, Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence. LICS 2017.
  • O2: Robust tactics for proof engineering.
    During certified software development, a major part of the effort is spent on proofs. Proof engineering is however very badly served by current tools, such as the tactic language of Coq. Proof developers tend to neglect elementary engineering qualities such as robustness and evolvability when creating tactics, yielding proof scripts that are very brittle. An objective of this project is to develop better tools to assist in the development of robust tactics. In particular, we will build on the work of Beta Ziliani on a typed tactic language [JFP’15], extending it with reasoning about the effects that tactics have on the “state of a proof” (eg. number of sub-goals, metavariables in context). We will also develop a novel approach for incremental type checking of proof scripts, allowing programmers to have a richer discovery-engineering interaction with the proof assistant.
    • [JFP’15] Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis. Mtac: A monad for typed tactic programming in Coq. J. Funct. Program. 25 (2015).
  • O3: Univalence at work.
    At the heart of the Coq proof assistant is type theory. A particularly important concept for easing certified programming is to exploit the notion of equivalences between types in order to establish properties of programs by operating on equivalent, though more amenable, structures. In recent work, Dagand, Tabareau and Tanter exploit partial type equivalences to facilitate dependently-typed programming with [ICFP’16]. This project will go a step further, by studying how the notion of univalence from homotopy type theory [HoTT’13] can be put in practice for certified software engineering. Univalence, in principle, allows to rewrite any program through equivalences; being an axiom, however, it has no computational content. A theoretical insight of this proposal is that we can give a partial computational meaning to univalence, leading to a novel notion of ad-hoc univalence that could be applied for lifting entire libraries to interoperate in new contexts.

    • [HoTT’13] Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book/.
    • [ICFP’16] Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter. Partial type equivalences for verified dependent interoperability. ICFP 2016: 298-310
  • O4: Case studies.
    We will validate the different frameworks and tools developed in the above tracks through case studies in various domains. This includes textbook verification of functional algorithms [VFA’17], as well as state-of-the-art verification techniques for probabilistic programs (eg. CertiCrypt). We will also analyze specific software systems developed at the University of Chile (by the Center for Mathematical Modeling), which are currently used in industry and other national organizations, in order to study how best to approach the certification in Coq of their key critical components.


Where to contact the PI of the project

I am available @

My email : nicolas.tabareau@inria.fr