Author: lmvadm

[November 2024] Talk by Thibaut Benjamin

Mechanisation of computation for identity types in Martin-Löf type theory
Thibaut Benjamin (University of Cambridge)
November 25, 2024
Martin-Löf type theory is a powerful theory that is at the foundation of modern proof assistants such as Coq, Lean, Agda. It provides a unifying framework to formalise mathematics and software. Although this framework is powerful enough to formalise and verify very complex software (like for instance the CompCert C compiler, formally verified in Coq), its practical use is constrained by the large proof effort it requires, rendering the adoption of such tools slower. Various techniques are considered to simplify and streamline the use of proof-assistants. For instance, identity types, that represent equalities have a very rich and complex structure, and it is common to ignore that structure by adding a principle called Uniqueness of Identity Proofs (UIP). This axiom states that any two identity proofs are equal thus enforcing in a way proof irrelevance for equality. Another example is the so-called univalent axiom (originally coming from a connection with homotopy theory) that for computer scientists mean that the formalisation can be done in a way that is independent of the choice of datatypes, as long as those datatypes encode the same information. This is not only a powerful reasoning principle that allows one to reason on simple but inefficient datatypes and transport the results to finicky but efficient ones, it also reflects the very common computer science practice of hiding the implementation of datatypes under an API to make the programs more modular. Unfortunately, UIP and the univalence axiom are incompatible. In this talk, I will present a workflow that I am designing to handle and automate complex computation on identity types, in an effort to reduce the need for UIP and render practical the use of the univalence axiom. I will in particular show the implementation of this workflow as a Coq plugin, that uses a secondary tool called CaTT, which is specifically designed to handle the algebraic structure of identity types, called higher groupoid.

[June 2024] The four-year For-CoaLa project is funded by ANR

Coordinator: Hélène Coulon, IMT Atlantique
Partners: IMT Atlantique (Stack Inria Team), Université d’Orléans (LIFO, LMV Team)

Large distributed software systems (applications or infrastructures) are now ubiquitous, with component-based systems (e.g., service-oriented architectures or microservices) offering a convenient way to structure large systems, in particular distributed systems deployed in the Cloud, in the core, or at the edge of the network. DevOps operations, that include system configurations and reconfigurations, are required to handle various kinds of scenarios such as fault tolerance, scalability, software updates, or various optimizations, etc. Such changes may lead to faults. A study of 597 unplanned outages that affected popular cloud services between 2009 and 2015 found that 16% of them were caused by a system upgrade.

On the one hand, many configuration tools and languages exist in the DevOps community, some of them being specific to the provisioning of resources in Cloud providers, packaging problems, containerized deployments, configuration of applications or infrastructures, etc. The main advantage of these tools is their full integration and adoption in the DevOps community. Their disadvantage is they lack both formal and textual specifications. Moreover, their contours are blurred. On the other hand, many initiatives have been studied in academia to contribute to the deployment, configuration, and reconfiguration of distributed software, bringing improvements such as expressivity, speed, safety, etc. Many come with precise and sometimes formal definitions. However, they lack the breadth of the mainstream DevOps tools.

The goal of For-CoaLa is twofold: (1) understand and bridge the gap between a popular tool from the DevOps community (Ansible) and a tool from academia (Concerto); (2) improve the understanding of these languages based on mechanized formal semantics and develop verified semantic-preserving cross-language transformations.