GECO in a nutshell
GECO is an Inria associate team between the Gallinette team
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
GECO is also involved in the Chilean-funded CSEC
in partnership with Inria Chile
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.
O1: Foundations and practice of gradual
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.
[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.