Report

Teaser, summary, work performed and final results

Periodic Reporting for period 3 - CoqHoTT (Coq for Homotopy Type Theory)

Teaser

Every year, software bugs cost hundreds of millions of euros to companies and administrations, as assessed by Intel Pentium division bug or Ariane 5 first flight failure. Hence, software quality is a notion that becomes more and more prevalent, going beyond the usual scope of...

Summary

Every year, software bugs cost hundreds of millions of euros to companies and administrations, as assessed by Intel Pentium division bug or Ariane 5 first flight failure. Hence, software quality is a notion that becomes more and more prevalent, going beyond the usual scope of embedded systems. In particular, the development of tools to construct softwares that respect a given specification is a major challenge of current and future researches in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their efficiency to prove correctness of important pieces of software like the C compiler of the CompCert project. One main interest of using such theorem provers from a computer science point of view is the ability to extract the code that has been proven directly from the proof, being able to run it as any other pieces of code. Unfortunately, the democratization of theorem provers such as Coq suffers from a major drawback, the mismatch between the conception of equality in mathematics and equality in type theory. As a consequence, significant Coq developments can be done by virtuosos playing around with advanced concepts of both computer science and mathematics, but not by working computer scientists or mathematicians. A first step towards solving this issue has been performed recently by the development of homotopy type theory (HoTT). This extension of type theory with homotopical concepts is gaining traction in the community because it allows for the first time to marry many expected principles of equality inside the same theory. This new theory is build upon a principle, dubbed univalence, which has never been considered before in type theory and that provides a new base on which to found mathematics together with a new way for computer scientists to reason about isomorphic types and equivalent programs. So far, the univalence principle has been added to type theory as a new axiom. But stating univalence as an axiom breaks one fundamental property of mechanized proofs: it breaks the extraction mechanism, that is the ability to compute with a program that makes use of this axiom. The starting point of the CoqHoTT project is to build a system where univalence is a property of the system—not an axiom.

The main goal of the CoqHoTT project is to provide a new generation of proof assistants with a computational version of univalence and use them as a base to implement effective logical model transformation so that the power of the internal logic of the proof assistant needed to prove the correctness of a program can be decided and changed at compile time—according to a trade-off between efficiency and logical expressivity. Our approach is based on a radically new compilation phase technique into a core type theory to modularize the difficulty of finding a decidable type checking algorithm for homotopy type theory and other richer type theories.

Work performed

We describe the major achievements of the project using the decomposition of work packages originally given in the proposal. Overall, the project fits with its original scheduling.

- Work Package 1: Define an internalization of homotopy type theory in Coq.
The work on the adaptation of the forcing construction in Type Theory [LICS’16] provides the necessary corner stone to define an internalization of homotopy type theory in Coq. We are currently working with Coquand’s group in Göteborg, Sweden, to use forcing in order to implement their Cubical Type Theory in Coq.

- Work Package 2: Develop a decidable type checking procedure for homotopy type theory.
The approach that we have taken in WP1 gives rise to a direct implementation of the type checking procedure. The remaining effort will be on efficiency.

- Work Package 3: Implement CoqHoTT, an extension of Coq to homotopy type theory.
 Not started. This task is schedule after 36 months of the project.

- Work Package 4: Define and implement a general notion of higher inductive types.
 Matthieu Sozeau (researcher) and Cyprien Mangin (PhD candidate) are working on the implementation. Ambroise Lafont (PhD candidate) and Benedikt Ahrens (post-doc) are working on the general theory justifying higher inductive types. Gaetan Gilbert has published his work on the formalization of real numbers using HITs provided by
the implementation of Matthieu and Cyprien [CPP\'17]

- Work Package 5: Extend homotopy type theory with new logical/computational principles.
 Kevin Quirin and Nicolas Tabareau have developed Lawvere-Tierney sheafification in homotopy type theory [Journal of Formalised Reasoning]. This, together with the development of forcing in type theory, constitute the two main theoretical part of this WP. The remaining effort is on the implementation and use of those ideas. We have also work on
other translations of type theory providing for instance ad-hoc polymorphism on types [CPP\'17].

Final results

Our implementation of new logical and computational paradigms directly in mainstream proof assistants, without axioms, was something that was out of reach before.
Apart from the publications that assessed its recognition in the community, Nicolas Tabareau has been invited to give an invited talk at CoqPL 2017
and the Coq Workshop 2018 to talk on the recent progress of the team. Some of our publications are now cited on the coq-club mailing list as typical answers to questions ask by
Coq\'s users on the logical expressivity of the system.
One other main achievement is the integration of a new universe in Coq 8.10 which is a direct consequence of our P0PL\'19 paper.

Website & more info

More info: http://coqhott.gforge.inria.fr/.