3.2.1 A definitional proof-irrelevant version of Coq.

In the Coq proof assistant, the sort $\mathrm{𝐏𝐫𝐨𝐩}$ stands for the universe of types which are propositions. That is, when a term $P$ has type $\mathrm{𝐏𝐫𝐨𝐩}$, the only relevant fact is whether $P$ is inhabited (that is true) or not (that is false). This property, known as proof irrelevance, can be expressed formally as: $\forall xy:P,x=y$. Originally, the raison d'être of the sort $\mathrm{𝐏𝐫𝐨𝐩}$ was to characterise types with no computational meaning with the intention that terms of such types could be erased upon extraction. However, the assumption that every element of $\mathrm{𝐏𝐫𝐨𝐩}$ should be proof irrelevant has never been integrated to the system. Indeed, in Coq, proof irrelevance for the sort $\mathrm{𝐏𝐫𝐨𝐩}$ is not incorporated into the theory: it is only compatible with it, in the sense that its assumption does not give rise to an inconsistent theory. In fact, the exact status of the sort $\mathrm{𝐏𝐫𝐨𝐩}$ in Coq has never been entirely clarified, which explains in part this lack of integration. Homotopy type theory brings fresh thinking on this issue and suggests turning $\mathrm{𝐏𝐫𝐨𝐩}$ into the collection of terms that a certain static inference procedure tags as proof irrelevant. The goal of this task is to integrate this insight in the Coq system and to implement a definitional proof-irrelevant version of the sort $\mathrm{𝐏𝐫𝐨𝐩}$.

3.2.2 Extend the Coq proof assistant with a computational version of univalence

The univalence principle is becoming widely accepted as a very promising avenue to provide new foundations for mathematics and type theory. However, this principle has not yet been incorporated into a proof assistant. Indeed, the very mathematical structures (known as $\infty$-groupoids) motivating the theory remain to this day an active area of research. Moreover, a correct and decidable type checking procedure for the whole theory raises both computational complexity and logical coherence issues. Observational type theory 36, as implemented in Epigram, provides a first-stage approximation to homotopy type theory, but only deals with functional extensionality and does not capture univalence. Coquand and his collaborators have obtained significant results on the computational meaning of univalence using cubical sets 44, 49. Bickford has initiated a promising formalisation work 1 in the NuPRL system. However, a complete formalisation in intensional type theory remains an open problem.

Hence a major objective is to achieve a complete internalisation of univalence in intensional type theory, including an integration to a new version of Coq. We will strive to keep compatibility with previous versions, in particular from a performance point of view. Indeed, the additional complexity of homotopy type theory should not induce an overhead in the type checking procedure used by the software if we want our new framework to become rapidly adopted by the community. Concretely, we will make sure that the compilation time of Coq’s Standard Library will be of the same order of magnitude.

3.2.3 Extend the logical power of type theory without axioms in a modular way

Extending the power of a logic using model transformations (e.g., forcing transformation 76, 75 or the sheaf construction 106) is a classic topic of mathematical logic 50, 81. However, these ideas have not been much investigated in the setting of type theory, even though they may provide a useful framework for extending the logical power of proof assistant in a modular way. There is a good reason for this: with a syntactic notion of equality, the underlying structure of type theory does not conform to the structure of topos used in mathematical logic. A direct incorporation of the standard techniques is therefore not possible. However, a univalent notion of equality brings type theory closer to the required algebraic structure, as it corresponds to the notion of $\infty$-topos recently studied by Lurie 88. The goal of this task is to revisit model transformations in the light of the univalence principle, and to obtain in this way new internal transformations in type theory which can in turn be seen as compilation phases. The general notion of an internal syntactical translation has already been investigated in the team 45.

3.2.4 Methodology: Extending type theory with different compilation phases

The Gallinette project advocates the use of distinct compilation phases as a methodology for the design of a new generation of proof assistants featuring modular extensions of a core logic. The essence of a compiler is the separation of the complexity of a translation process into modular stages, and the organization of their re-composition. This idea finds a natural application in the design of complex proof assistants (Figure 1). For instance, the definition of type classes in Coq follows this pattern, and is morally given by the means of a translation into a type-class free kernel. More recently, a similar approach by compilation stages, using the forcing transformation, was used to relax the strict positivity condition guarding inductive types 76, 75. We believe that this flavour of compilation-based strategies offers a promising direction of investigation for the purpose of defining a decidable type checking algorithm for HoTT.

3.3.1 Models for integrating effects with dependent types

A crucial step is the integration of dependent types with effects, a topic which has remained “currently under investigation”  96 ever since the beginning. The difficulty resides in expressing the dependency of types on terms that can perform side-effects during the computation. On the side of denotational semantics, several extensions of categorical models for effects with dependent types have been proposed 33, 113 using axioms that should correspond to restrictions in terms of expressivity but whose practical implications, however, are not immediately transparent. On the side of logical approaches 71, 72, 82, 94, one first considers a drastic restriction to terms that do not compute, which is then relaxed by semantic means. On the side of systems for certified programming such as ${\mathrm{F}}^{☆}$, the type system ensures that types only depend on pure and terminating terms.

Thus, the recurring idea is to introduce restrictions on the dependency in order to establish an encapsulation of effects. In our approach, we seek a principled description of this idea by developing the concept of semantic value (thunkables, linears) which arose from foundational considerations 61, 108, 98 and whose relevance was highlighted in recent works  85, 102. The novel aspect of our approach is to seek a proper extension of type theory which would provide foundations for a classical type theory with axiom of choice in the style of Herbelin  71, but which moreover could be generalised to effects other than just control by exploiting an abstract and adaptable notion of semantic value.

3.3.2 Intuitionistic depolarisation

In our view, the common idea that evaluation order does not matter for pure and terminating computations should serve as a bridge between our proposals for dependent types in the presence of effects and traditional type theory. Building on the previous goal, we aim to study the relationship between semantic values, purity, and parametricity theorems 107, 63. Our goal is to characterise parametricity as a form of intuitionistic depolarisation following the method by which the first game model of full linear logic was given (Melliès 91, 92). We have two expected outcomes in mind: enriching type theory with intensional content without losing its properties, and giving an explanation of the dependent types in the style of Idris and ${\mathrm{F}}^{☆}$ where purity- and termination-checking play a role.

3.3.3 Developing the rewriting theory of calculi with effects

An integrated type theory with effects requires an understanding of evaluation order from the point of view of rewriting. For instance, rewriting properties can entail the decidability of some conversions, allowing the automation of equational reasoning in types  31. They can also provide proofs of computational consistency (that terms are not all equivalent) by showing that extending calculi with new constructs is conservative  110. In our approach, the $\lambda$-calculus is replaced by a calculus modelling the evaluation in an abstract machine  56. We have shown how this approach generalises the previous semantic and proof-theoretic approaches 37, 84, 86, and overcomes their shortcomings 99.

One goal is to prove computational consistency or decidability of conversions purely using advanced rewriting techniques following a technique introduced in 110. Another goal is the characterisation of weak reductions: extensions of the operational semantics to terms with free variables that preserve termination, whose iteration is equivalent to strong reduction 32, 59. We aim to show that such properties derive from generic theorems of higher-order rewriting 115, so that weak reduction can easily be generalised to richer systems with effects.

3.3.4 Direct models and categorical coherence

Proof theory and rewriting are a source of coherence theorems in category theory, which show how calculations in a category can be simplified with an embedding into a structure with stronger properties 89, 80. We aim to explore such results for categorical models of effects 84, 55. Our key insight is to consider the reflection between indirect and direct models 61, 98 as a coherence theorem: it allows us to embed the traditional models of effects into structures for which the rewriting and proof-theoretic techniques from the previous section are effective.

Building on this, we are further interested in connecting operational semantics to 2-category theory, in which a second dimension is traditionally considered for modelling conversions of programs rather than equivalences. This idea has been successfully applied for the $\lambda$-calculus 77, 73 but does not scale yet to more realistic models of computation. In our approach, it has already been noticed that the expected symmetries coming from categorical dualities are better represented, motivating a new investigation into this long-standing question.

3.3.5 Models of effects and resources

The unified theory of effects and resources 55 prompts an investigation into the semantics of safe and automatic resource management, in the style of Modern C++ and Rust. Our goal is to show how advanced semantics of effects, resources, and their combination arise by assembling elementary blocks, pursuing the methodology applied by Melliès and Tabareau in the context of continuations 93. For instance, combining control flow (exceptions, return) with linearity allows us to describe in a precise way the “Resource Acquisition Is Initialisation” idiom in which the resource safety is ensured with scope-based destructors. A further step would be to reconstruct uniqueness types and borrowing using similar ideas.

3.4.1 Gradual Certified Programming

One of the main issues faced by a programmer starting to internalise in a proof assistant code written in a more permissive world is that type theory is constrained by a strict type discipline which lacks flexibility. Concretely, as soon as you start giving a more precise type/specification to a function, the rest of the code interacting with this function needs to be more precise too. To address this issue, the Gallinette team will put strong efforts into the development of gradual typing in type theory to allow progressive integration of code that comes from a more permissive world.

Indeed, 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 direction 112. This work, however, suffers from a number of limitations, the most important being the lack of a mechanism for handling the possibility of runtime errors within Coq. Instead of relying on axioms, this project will explore the application of Section 3.3 to embed effects in Coq. This way, instead of postulating axioms for parts of the development that are too hard/marginal to be dealt with, the system adds dynamic checks. Then, after extraction, we get a program that corresponds to the initial program but with dynamic checks for parts that have not been proven, ensuring that the program will raise an error instead of going outside its specification.

This will yield new foundations of gradual certified programming, both more expressive and practical. We will also study how to integrate previous techniques with the extraction mechanism of Coq programs to OCaml, in order to exploit the exception mechanism of OCaml.

3.4.2 Imperative features and object polymorphism in the Coq proof assistant

3.4.3 Robust tactics for proof engineering for the scaling of formalised libraries

When developing certified software, a major part of the effort is spent not only on writing proof scripts, but on rewriting them, either for the purpose of code maintenance or because of more significant changes in the base definitions. Regrettably, proof scripts suffer more often than not from a bad programming style, and too many proof developers casually neglect the most elementary principles of well-behaved programmers. As a result, many proof scripts are very brittle, user-defined tactics are often difficult to extend, and sometimes even lack a clear specification. Formal libraries are thus generally very fragile pieces of software. One reason for this unfortunate situation is that proof engineering is very badly served by the tools currently available to the users of the Coq proof assistant, starting with its tactic language. One objective of the Gallinette team is to develop better tools to write proof scripts.

Completing and maintaining a large corpus of formalised mathematics requires a well-designed tactic language. This language should both accommodate the possible specific needs of the theories at stake, and help with diagnostics at refactoring time. Coq's tactic language is in fact two-leveled. First, it includes a basic tactic language, to organise the deductive steps in a proof script and to perform the elementary bureaucracy. Its second layer is a meta-programming language, which allows users to define their own new tactics at toplevel. Our first direction of work consists in the investigation of the appropriate features of the basic tactic language. For instance, the design of the Ssreflect tactic language, and its support for the small scale reflection methodology 66, has been a key ingredient in at least two large scale formalisation endeavours: the Four Colour Theorem 65 and of the Odd Order Theorem 64. Building on our experience with the Ssreflect tactic language, we will contribute to the ongoing work on the basic tactic language for Coq. The second objective of this task is to contribute to the design of a typed tactic language. In particular, we will build on the work of Ziliani and his collaborators 114, extending it with reasoning about the effects that tactics have on the “state of a proof” (e.g. number of sub-goals, metavariables in context). We will also develop a novel approach for incremental type checking of proof scripts, so that programmers gain access to a richer discovery- engineering interaction with the proof assistant.

3.5.1 Certified Code Refactoring

In the context of refactoring of C programs, we intend to formalise program transformations that are written in an imperative style to test the usability of our addition of effects in the proof assistant. This subject has been chosen based on the competence of members of the team.

We are currently working on the formalisation of refactoring tools in Coq 52. Automatic refactoring of programs in industrial languages is difficult because of the large number of potential interactions between language features that are difficult to predict and to test. Indeed, all available refactoring tools suffer from bugs : they fail to ensure that the generated program has the same behaviour as the input program. To cope with that difficulty, we have chosen to build a refactoring tool with Coq : a program transformation is written in the Coq programming language, then proven correct on all possible inputs, and then an OCaml executable program is generated by the platform. We rely on the CompCert C formalisation of the C language. CompCert is currently the most complete formalisation of an industrial language, which justifies that choice. We have three goals in that project :

• Build a refactoring tool that programmers can rely on and make it available in a popular platform (such as Eclipse, IntelliJ or Frama-C).
• Explore large, drastic program transformations such as replacing a design architecture for an other one, by applying a sequence of small refactoring operations (as we have done for Java and Haskell programs before 51, 48, 34), while ensuring behaviour preservation.
• Explore the use of enhancements of proof systems on large developments. For instance, refactoring tools are usually developed in the imperative/object paradigm, so the extension of Coq with side effects or with object features proposed in the team can find a direct use-case here.

3.5.2 Certified Constraint Programming

We plan to make use of the internalisation of the object-oriented paradigm in the context of constraint programming. Indeed, this domain is made of very complex algorithms that are often developed using object-oriented programming (as it is the case for instance for CHOCO, which is developed in the Tasc Group at IMT Atlantique, Nantes). We will in particular focus on filtering algorithms in constraint solvers, for which research publications currently propose new algorithms with manual proofs. Their formalisation in Coq is challenging. Another interesting part of constraint solving to formalise is the part that deals with program generation (as opposed to extraction). However, when there are numerous generated pieces of code, it is not realistic to prove their correctness manually, and it can be too difficult to prove the correctness of a generator. So we intend to explore a middle path that consists in generating a piece of code along with its corresponding proof (script or proof term). A target application could be interval constraints (for instance Allen interval algebra or region connection calculus) that can generate thousands of specialised filtering algorithms for a small number of variables 41.

Finally, Rémi Douence has already worked (articles publishing 68, 105, 58, 42, 39, 38, PhD Thesis advising 104, 40) with different members of the Tasc team. Currently, he supervises with Nicolas Beldiceanu the PhD Thesis of Jovial Cheukam Ngouonou in the Tasc team. He studies graph invariants to enhance learning algorithms. This work requires proofs, manually done for now, we would like to explore when these proofs could be mechanized.

3.5.3 Certified Symbolic Computation

We will investigate how the addition of effects in the Coq proof assistant can facilitate the marriage of computer algebra with formal proofs. Computer algebra systems on one hand, and proof assistants on the other hand, are both designed for doing mathematics with the help of a computer, by the means of symbolic computations. These two families of systems are however very different in nature: computer algebra systems allow for implementations faithful to the theoretical complexity of the algorithms, whereas proof assistants have the expressiveness to specify exactly the semantics of the data-structures and computations.

Experiments have been run that link computer algebra systems with Coq 57, 47. These bridges rely on the implementation of formal proof-producing core algorithms like normalisation procedures. Incidentally, they require non trivial maintenance work to survive the evolution of both systems. Other proof assistants like the Isabelle/HOL system make use of so-called reflection schemes: the proof assistant can produce code in an external programming language like SML, but also allows to import the values output by these extracted programs back inside the formal proofs. This feature extends the trusted base of code quite significantly but it has been used for major achievements like a certified symbolic/numeric ODE solver 74.

We would like to bring Coq closer to the efficiency and user-friendliness of computer algebra systems: for now it is difficult to use the Coq programming language so that certified implementations of computer algebra algorithms have the right, observable, complexity when they are executed inside Coq. We see the addition of effects to the proof assistant as an opportunity to ease these implementations, for instance by making use of caching mechanisms or of profiling facilities. Such enhancements should enable the verification of computation-intensive mathematical proofs that are currently beyond reach, like the validation of Helfgott's proof of the weak Goldbach conjecture 70.

6.1.1 Ltac2

• Keywords: Coq, Proof assistant
• Functional Description: A replacement for Ltac, the tactic language of Coq.
• Contact: Pierre-Marie Pédrot

6.1.2 Equations

• Keywords: Coq, Dependent Pattern-Matching, Proof assistant, Functional programming
• Scientific Description:

  Equations is a tool designed to help with the definition of programs in the setting of dependent type theory, as implemented in the Coq proof assistant. Equations provides a syntax for defining programs by dependent pattern-matching and well-founded recursion and compiles them down to the core type theory of Coq, using the primitive eliminators for inductive types, accessibility and equality. In addition to the definitions of programs, it also automatically derives useful reasoning principles in the form of propositional equations describing the functions, and an elimination principle for calls to this function. It realizes this using a purely definitional translation of high-level definitions to core terms, without changing the core calculus in any way, or using axioms.

  The main features of Equations include:

  Dependent pattern-matching in the style of Agda/Epigram, with inaccessible patterns, with and where clauses. The use of the K axiom or a proof of K is configurable, and it is able to solve unification problems without resorting to the K rule if not necessary.

  Support for well-founded and mutual recursion using measure/well-foundedness annotations, even on indexed inductive types, using an automatic derivation of the subterm relation for inductive families.

  Support for mutual and nested structural recursion using with and where auxilliary definitions, allowing to factor multiple uses of the same nested fixpoint definition. It proves the expected elimination principles for mutual and nested definitions.

  Automatic generation of the defining equations as rewrite rules for every definition.

  Automatic generation of the unfolding lemma for well-founded definitions (requiring only functional extensionality).

  Automatic derivation of the graph of the function and its elimination principle. In case the automation fails to prove these principles, the user is asked to provide a proof.

  A new dependent elimination tactic based on the same splitting tree compilation scheme that can advantageously replace dependent destruction and sometimes inversion as well. The as clause of dependent elimination allows to specify exactly the patterns and naming of new variables needed for an elimination.

  A set of Derive commands for automatic derivation of constructions from an inductive type: its signature, no-confusion property, well-founded subterm relation and decidable equality proof, if applicable.

• Functional Description:

  Equations is a function definition plugin for Coq (supporting Coq 8.11 to 8.13, with special support for the Coq-HoTT library), that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle.

  Equations is based on a simplification engine for the dependent equalities appearing in dependent eliminations that is also usable as a separate tactic, providing an axiom-free variant of dependent destruction.

• Release Contributions:

  This version of Equations is based on an improved simplification engine for the dependent equalities appearing during dependent eliminations that is also usable as a separate dependent elimination tactic, providing an axiom-free variant of dependent destruction and a more powerful form of inversion.

  This is a bugfix release of version 1.2 working with Coq 8.11 to Coq 8.13 See https://mattam82.github.io/Coq-Equations/equations/2019/05/17/1.2.html for the 1.2 release notes. New in this version:

  Fixed issue #297: dependent elimination simplification mistreated let-bindings Fixed issue #295: discrepancy between the syntax in the manual and the implementation Ensure that NoConfusion is derived before EqDec as it is necessary to solve the corresponding obligation.

• News of the Year: Equations 1.2.3, released first in June 2020 brings bugfixes, a fixed grammar and more robust proof automation tactics.
• URL: http://mattam82.github.io/Coq-Equations/
• Publications: hal-01671777, hal-01248807, inria-00628862
• Authors: Cyprien Mangin, Matthieu Sozeau, Matthieu Sozeau
• Contact: Matthieu Sozeau
• Participants: Matthieu Sozeau, Cyprien Mangin

6.1.3 Math-Components

• Name: Mathematical Components library
• Keyword: Proof assistant
• Functional Description: The Mathematical Components library is a set of Coq libraries that cover the prerequiste for the mechanization of the proof of the Odd Order Theorem.
• Release Contributions: This releases is compatible with Coq 8.10, 8.11 and Coq 8.12 The main changes are: - support for Coq 8.7, 8.8 and 8.9 have been dropped, - a change of implementation of intervals and the updated theory, - the addition of kernel lemmas for matrices, - generalized many lemmas for path and sorted, - several lemma additions, name changes and bug fixes.
• URL: http://math-comp.github.io/math-comp/
• Contacts: Assia Mahboubi, Enrico Tassi, Georges Gonthier
• Participants: Alexey Solovyev, Andrea Asperti, Assia Mahboubi, Cyril Cohen, Enrico Tassi, François Garillot, Georges Gonthier, Ioana Pasca, Jeremy Avigad, Laurence Rideau, Laurent Théry, Russell O'Connor, Sidi Ould Biha, Stéphane Le Roux, Yves Bertot

6.1.4 math-comp-analysis

• Name: Mathematical Components Analysis
• Keyword: Proof assistant
• Functional Description: This library adds definitions and theorems for real numbers and their mathematical structures
• Release Contributions: Compatible with MathComp 1.12.0, and Coq 8.11 and 8.12.
• News of the Year: In 2019, there were 3 releases.
• URL: https://github.com/math-comp/analysis
• Publication: hal-01719918
• Contacts: Cyril Cohen, Georges Gonthier, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Laurence Rideau, Pierre-Yves Strub, Reynald Affeldt
• Partners: Ecole Polytechnique, AIST Tsukuba

6.1.5 MetaCoq

• Keyword: Coq
• Scientific Description:

  The MetaCoq project aims to provide a certified meta-programming environment in Coq. It builds on Template-Coq, a plugin for Coq originally implemented by Malecha (Extensible proof engineering in intensional type theory, Harvard University, 2014), which provided a reifier for Coq terms and global declarations, as represented in the Coq kernel, as well as a denotation command. Recently, it was used in the CertiCoq certified compiler project (Anand et al., in: CoqPL, Paris, France, 2017), as its front-end language, to derive parametricity properties (Anand and Morrisett, in: CoqPL’18, Los Angeles, CA, USA, 2018). However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq ’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. MetaCoq generalizes it to handle the entire polymorphic calculus of cumulative inductive constructions, as implemented by Coq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq’s logical environment. The MetaCoq framework allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. Examples of implemented plugins include a parametricity translation and a certified extraction to call-by-value lambda-calculus. The meta-theory of Coq itself is verified in MetaCoq along with verified conversion, type-checking and erasure procedures providing higly trustable alternatives to the procedures in Coq's OCaml kernel. MetaCoq is hence a foundation for the development of higher-level certified tools on top of Coq's kernel. A meta-programming and proving framework for Coq.

  MetaCoq is made of 4 main components: - The entry point of the project is the Template-Coq quoting and unquoting library for Coq which allows quotation and denotation of terms between three variants of the Coq AST: the OCaml one used by Coq's kernel, the Coq one defined in MetaCoq and the one defined by the extraction of the MetaCoq AST, allowing to extract OCaml plugins from Coq implementations. - The PCUIC component is a full formalization of Coq's typing and reduction rules, along with proofs of important metatheoretic properties: weakening, substitution, validity, subject reduction and principality. The PCUIC calculus differs slightly from the Template-Coq one and verified translations between the two are provided. - The checker component contains verified implementations of weak-head reduction, conversion and type inference for the PCUIC calculus, along with a verified checker for Coq theories. - The erasure compoment contains a verified implementation of erasure/extraction from PCUIC to untyped (call-by-value) lambda calculus extended with a dummy value for erased terms.

• Functional Description: MetaCoq is a framework containing a formalization and verified implementation of Coq's kernel in Coq along with a verified erasure procedure. It provides tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.
• Release Contributions: This version is a beta-release including a fully-functional reification and denotation support, and the verified type-checking and erasure procedures. The metatheory proofs are not entirely completed.
• News of the Year: The verification of Coq's typechecking and conversion algorithm was completed, resulting in a publication at POPL'20. During this year we improved the erasure procedure, verified completeness in addition to soundness of the conversion algorithm and completed the subject reduction and principality proofs for the PCUIC calculus. MetaCoq was used to show the confluence and subject reduction of an extension of Coq with rewrite rules, presented in an article at POPL'21.
• URL: https://metacoq.github.io
• Publications: hal-02901011, hal-02380196, hal-02167423, hal-01809681
• Contact: Matthieu Sozeau
• Participants: Abhishek Anand, Danil Annenkov, Meven Bertrand, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, Theo Winterhalter
• Partners: Concordium Blockchain Research Center, Aarhus University, Denmark, Saarland University

6.1.6 Coq

• Name: The Coq Proof Assistant
• Keywords: Proof, Certification, Formalisation
• Scientific Description: Coq is an interactive proof assistant based on the Calculus of (Co-)Inductive Constructions, extended with universe polymorphism. This type theory features inductive and co-inductive families, an impredicative sort and a hierarchy of predicative universes, making it a very expressive logic. The calculus allows to formalize both general mathematics and computer programs, ranging from theories of finite structures to abstract algebra and categories to programming language metatheory and compiler verification. Coq is organised as a (relatively small) kernel including efficient conversion tests on which are built a set of higher-level layers: a powerful proof engine and unification algorithm, various tactics/decision procedures, a transactional document model and, at the very top an IDE.
• Functional Description: Coq provides both a dependently-typed functional programming language and a logical formalism, which, altogether, support the formalisation of mathematical theories and the specification and certification of properties of programs. Coq also provides a large and extensible set of automatic or semi-automatic proof methods. Coq's programs are extractible to OCaml, Haskell, Scheme, ...
• Release Contributions:

  Some highlights from this release are:

  - Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays. - Introduction of definitional proof irrelevance for the equality type defined in the SProp sort. - Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior.

  See the Zenodo citation for more information on this release: https://zenodo.org/record/4501022#.YB00r5NKjlw

• News of the Year:

  Coq version 8.13 integrates many usability improvements, as well as extensions of the core language. The main changes include: - Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays. - Introduction of definitional proof irrelevance for the equality type defined in the SProp sort. - Cumulative record and inductive type declarations can now specify the variance of their universes. - Various bugfixes and uniformization of behavior with respect to the use of implicit arguments and the handling of existential variables in declarations, unification and tactics. - New warning for unused variables in catch-all match branches that match multiple distinct patterns. - New warning for Hint commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default behavior of importing hints only when using Require. The recommended fix is to declare hints as export, instead of the current default global, meaning that they are imported through Require Import only, not Require. See the following rationale and guidelines for details. - General support for boolean attributes. - Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior. - Tactic improvements in lia and its zify preprocessing step, now supporting reasoning on boolean operators such as Z.leb and supporting primitive integers Int63. - Typing flags can now be specified per-constant / inductive. - Improvements to the reference manual including updated syntax descriptions that match Coq's grammar in several chapters, and splitting parts of the tactics chapter to independent sections.

  See the changelog for an overview of the new features and changes, along with the full list of contributors. https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13

• URL: http://coq.inria.fr/
• Authors: Bruno Barras, Yves Bertot, Frédéric Besson, Pierre Corbineau, Cristina Cornes, Judicaël Courant, Pierre Courtieu, Pierre Crégut, David Delahaye, Maxime Denes, Jean-Christophe Filliâtre, Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Hugo Herbelin, Gérard Huet, Vincent Laporte, Pierre Letouzey, Assia Mahboubi, Pascal Manoury, Guillaume Melquiond, César Munoz, Chetan Murthy, Amokrane Saibi, Catherine Parent, Christine Paulin Mohring, Pierre-Marie Pédrot, Loïc Pottier, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi, Laurent Théry, Benjamin Werner, Théo Zimmermann
• Contacts: Hugo Herbelin, Matthieu Sozeau
• Participants: Yves Bertot, Frédéric Besson, Tej Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Denes, Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, Érik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot, ClÉment Pit-Claudel, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-Yao Xia, Théo Zimmermann
• Partners: CNRS, Université Paris-Sud, ENS Lyon, Université Paris-Diderot

6.1.7 memprof-limits

• Keyword: Library
• Scientific Description:

  Memprof-limits is an implementation of per-thread global memory limits, and per-thread allocation limits à la Haskell, for OCaml, compatible with multiple threads.

  Memprof-limits interrupts the execution by raising an asynchronous exception: an exception that can arise at almost any location in the program. It is provided with a guide on how to recover from asynchronous exceptions and other unexpected exceptions, thereby summarising practical knowledge acquired in OCaml by the Coq proof assistant as well as in other programming languages, to my knowledge told here for the first time.

  Memprof-limits is probabilistic, as it is based on the statistical memory accountant memprof. It is provided with a statistical analysis that the user can rely on to have guarantees about the enforcement of limits.

• Functional Description:

  Memprof-limits is a probabilistic implementation of per-thread global memory limits, and per-thread allocation limits, for the OCaml language.

  Per-thread global memory limits let you bound the memory consumption of specific parts of your program, in terms of memory used by the whole program.

  Per-thread allocation limits let you bound the execution of parts of the program measured in number of allocation, analogous to the same feature in Haskell. Allocation limits count allocations but not deallocations, and is therefore a measure of the work done which can be more suitable than execution time.

• Release Contributions: Initial version.
• URL: https://gitlab.com/gadmm/memprof-limits
• Author: Guillaume Munch
• Contact: Guillaume Munch

7.1.1 Reasoning about equivalence of programs

7.1.2 Classical Logic

7.1.3 Syntax and Rewriting Systems

Resource management in OCaml

The current multicore OCaml implementation bans so-called "naked pointers", pointers to outside the heap owned by the OCaml garbage collector, unless these pointers follow drastic restrictions. A backwards-incompatible change has been proposed to make way for the new multicore GC in OCaml. Building on our investigations for the design of a resource-management extension for OCaml, we argued in 23 that out-of-heap pointers are not an anomaly, but are part of a better mixing of systems and functional programming, and we designed an alternative approach that would better preserve the backwards-compatiblity aims of OCaml multicore without affecting performances.

7.3.1 Type Theory

7.3.2 Proof Assistants

Cubical Synthetic Homotopy Theory

Homotopy type theory is an extension of type theory that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations of multiple classical results from homotopy theory. However, many proofs are still surprisingly complicated to formalize. One reason for this is the axiomatic treatment of univalence and higher inductive types which complicates synthetic reasoning as many intermediate steps, that could hold simply by computation, require explicit arguments. Cubical type theory offers a solution to this in the form of a new type theory with native support for both univalence and higher inductive types. In 20, we show how the recent cubical extension of Agda can be used to formalize some of the major results of homotopy type theory in a direct and elegant manner.

Competing inheritance paths in dependent type theory: a case study in functional analysis

In 17, we discuss the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical analysis, for the Coq proof assistant. It extends the Mathematical Components library, geared towards algebra, with topics in analysis. Issues of a more general nature related to the inheritance of poorer structures from richer ones arise due to this combination. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints.

9.1.1 Inria International Labs

9.2.1 Visits to international teams

• G. Munch-Maccagnoni visited E. Tanter and M. Toro (U. Chile) from Januray to March (visit ended by the pandemic crisis).
• N. Tabareau visited E. Tanter (U. Chile) from Januray to March (visit ended by the pandemic crisis).

9.3.1 FP7 & H2020 Projects

10.1.1 Scientific Events: Organisation

10.1.2 Scientific Events: Selection

10.1.3 Journal

10.1.4 Invited Talks

• P.-M. Pédrot was planned to give an invited talk at TYPES'20 (cancelled at the last minute due to COVID outbreak).
• P.-M. Pédrot gave an invited talk at MSFP'20.
• P.-M. Pédrot gave a talk at the Birmingham Computer Science Seminar.
• A. Mahboubi gave an invited talk at Colloquium of Mathematics of the University of Ljubljana.
• A. Mahboubi gave a talk at the CRM - Computer Assisted Mathematical Proofs Seminar.

10.1.5 Leadership within the Scientific Community

• N. Tabareau is a member of the scientific committee of the GdR of Algebraic Topology.
• A. Mahboubi is a member of the core managment group of the EUTypes project, and leader of the “Tools” working group.
• A. Mahboubi is a member of the steering committee of the ITP conference.
• A. Mahboubi is a member of the steering committee of the CPP conference.
• A. Mahboubi is a member of the scientific committee of the GdR “Informatique Mathématique”.

10.1.6 Scientific Expertise

G. Munch-Maccagnoni acted as an expert for Nomadic Labs on OCaml-Rust bindings.

10.2.1 Teaching

• Licence : Julien Cohen, Discrete Mathematics, 48h, L1 (IUT), IUT Nantes, France
• Licence : Julien Cohen, Introduction to proof assistants (Coq), 8h, L2 (PEIP : IUT/Engineering school), Polytech Nantes, France
• Licence : Julien Cohen, Functional Programming (Scala), 22h, L2 (IUT), IUT Nantes, France
• Master : Julien Cohen, Object oriented programming (Java), 32h, M1 (Engineering school), Polytech Nantes, France
• Master : Julien Cohen, Functional programming (OCaml), 18h, M1 (Engineering school), Polytech Nantes, France
• Master : Julien Cohen, Tools for softaware engineering (proof with Frama-C, test, code management), 20h, M1 (Engineering school), Polytech Nantes, France
• Licence : Rémi Douence, Object Oriented Design and Programming, 45h, L1 (engineers), IMT-Atlantique, Nantes, France
• Licence : Rémi Douence, Object Oriented Design and Programming Project, 30h, L1 (apprenticeship), IMT-Atlantique, Nantes, France
• Master : Rémi Douence, Functional Programming with Haskell, 45h, M1 (engineers), IMT-Atlantique, Nantes, France
• Master : Rémi Douence, Functional Programming with Haskell, 20h, M1 (apprenticeship), IMT-Atlantique, Nantes, France
• Master : Rémi Douence, Formal Methods: Model checking with Alloy and from Haskell to Coq, 11h, M1 (apprenticeship), IMT-Atlantique, Nantes, France
• Master : Rémi Douence, Introduction to scientific research in computer science (Project: compilation in Java of Haskell Class Types), 45h, M2 (apprenticeship), IMT-Atlantique, Nantes, France
• Licence : Hervé Grall, Algorithms and Discrete Mathematics, 25h , L3 (engineers), IMT-Atlantique, Nantes, France
• Licence : Hervé Grall, Object Oriented Design and Programming, 25h , L3 (engineers), IMT-Atlantique, Nantes, France
• Licence, Master : Hervé Grall, Modularity and Typing, 40h, L3 and M1, IMT-Atlantique, Nantes, France
• Master : Hervé Grall, Service-oriented Computing, 40h, M1 and M2, IMT-Atlantique, Nantes, France
• Master : Hervé Grall, Research Project - (Linear) Logic Programming in Coq, 90h (1/3 supervised), M1 and M2, IMT-Atlantique, Nantes, France
• Licence : Guilhem Jaber, Computer Tools for Science, 36h, L1, Université de Nantes France
• Master : Guilhem Jaber, Verification and Formal Proofs, 18h, M1, Université de Nantes, France
• Master : Nicolas Tabareau, Homotopy Type Theory, 24h, M2 LMFI, Université Paris Diderot, France
• Master: Assia Mahboubi, Machine-Checked Mathematics, 22.5h, M2, Vrije Universiteit Amsterdam, the Netherlands
• Master : Matthieu Sozeau, Proof Assistants, 24h, M2 MPRI, Université Paris Diderot, France
• Master : Guillaume Munch-Maccagnoni, Initiation to safe systems programming with Rust, 7h, M1 (apprenticeship), IMT-Atlantique, Nantes, France

10.2.2 Supervision

• PhD defended on Sept 20: Théo Winterhalter, Formalisation and Meta-Theory of Type Theory, Univ Nantes, advisors: Matthieu Sozeau and Nicolas Tabareau
• PhD in progress: Xavier Montillet, Rewriting and solvability for Call-by-push-value, Univ Nantes, advisors: Guillaume Munch-Maccagnoni and Nicolas Tabareau
• PhD in progress: Joachim Hotonnier, Deep Specification for Domain-Specific Modelling, advisors: Gerson Sunye (Naomod team), Massimo Tisi (Naomod team), Hervé Grall.
• PhD in progress: Loïc Pujet, Giving meaning to cubical type theory using forcing, Univ Nantes, advisors: Nicolas Tabareau
• PhD in progress: Meven Bertrand, Gradualizing the calculus of constructions, Univ Nantes, advisors: Nicolas Tabareau
• PhD in progress: Martin Baillon, Syntactic Models of Type Theory and Continuity Principles, Univ Nantes, advisors: Assia Mahboubi and Pierre-Marie Pédrot
• PhD in progress: Pierre Benjamin Giraud, Formalizing extraction of Coq to OCaml, Univ Nantes, advisors: Pierre-Marie Pédrot, Matthieu Sozeau and Nicolas Tabareau
• PhD in progress: Enzo Crance, Automated theorem proving and dependent types: automated reasoning for interactive proof assistants, Univ Nantes, advisors: Denis Cousineau and Assia Mahboubi
• PhD in progress: Antoine Allioux, Coherent Higher Structures in Homotopy Type Theory, Univ Paris Diderot, advisors: Pierre-Louis Curien (Univ. Paris Diderot), Eric Finster (Univ. Birmingham) and Matthieu Sozeau

10.2.3 Juries

• N. Tabareau has served as examiner for the PhD of Ambre Williams defended December 14th at Inria Paris.
• N. Tabareau has served as examiner for the PhD of Thibaut Benjamin defended November 5th at École Polythecnique / Institut Polytechnique de Paris.
• N. Tabareau has served as external member on the PhD jury of Houssem Hachmaoui defended October 16th at Université Paris Saclay.
• A. Mahboubi has served as member in the jury of the 2020 Gilles Kahn PhD prize.
• A. Mahboubi has served as external member on the PhD jury of Théo Winterhalter defended on September 18th at Nantes University.

10.3.1 Internal or external Inria responsibilities

• A. Mahboubi participates to the Irisa/Inria mentoring program.

10.3.2 Education

• Hervé Grall has contributed to the project Merite, which aims to promote science learning in middle and high schools. He is the main contributor to the theme "Communication between machines". The project is coordinated by IMT-Atlantique in partnership with 7 other french higher education institutions, the rectorates of the Nantes and Rennes academies, and financed by the "Investments in the Future" and the fund FEDER Pays-de-la-Loire.

International journals

• 8 articleBenediktB. Ahrens, AndréA. Hirschowitz, AmbroiseA. Lafont and MarcoM. Maggesi. Reduction Monads and Their SignaturesProceedings of the ACM on Programming LanguagesJanuary 2020, 1-29
  HALDOIback to text
• 9 articleDimitriD. Ara and MaximeM. Lucas. The folk model category structure on strict $$-categories is monoidal'Theory and Applications of Categories3521May 2020, 745-808
  HALback to text
• 10 articleSimonS. Boulier and NicolasN. Tabareau. Model structure on the universe of all types in interval type theoryMathematical Structures in Computer ScienceOctober 2020, 1-32
  HALDOIback to text
• 11 article JesperJ. Cockx, NicolasN. Tabareau and ThéoT. Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions Proceedings of the ACM on Programming Languages 2020
  HAL back to text
• 12 articleGuilhemG. Jaber. SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with ReferencesProceedings of the ACM on Programming Languages282020, 1-28
  HALDOIback to text
• 13 articlePierre-MarieP.-M. Pédrot and NicolasN. Tabareau. The Fire Triangle: How to Mix Substitution, Dependent Elimination, and EffectsProceedings of the ACM on Programming LanguagesJanuary 2020, 1-28
  HALDOIback to text
• 14 article MatthieuM. Sozeau, AbhishekA. Anand, SimonS. Boulier, CyrilC. Cohen, YannickY. Forster, FabianF. Kunze, GregoryG. Malecha, NicolasN. Tabareau and ThéoT. Winterhalter. The MetaCoq Project Journal of Automated Reasoning February 2020
  HAL DOI back to text
• 15 articleMatthieuM. Sozeau, SimonS. Boulier, YannickY. Forster, NicolasN. Tabareau and ThéoT. Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in CoqProceedings of the ACM on Programming LanguagesJanuary 2020, 1-28
  HALDOIback to text
• 16 articleNicolasN. Tabareau, ÉricÉ. Tanter and MatthieuM. Sozeau. The Marriage of Univalence and ParametricityJournal of the ACM (JACM)681January 2021, 1-44
  HALDOI

International peer-reviewed conferences

• 17 inproceedingsReynaldR. Affeldt, CyrilC. Cohen, MarieM. Kerjean, AssiaA. Mahboubi, DamienD. Rouhling and KazuhikoK. Sakaguchi. Competing inheritance paths in dependent type theory: a case study in functional analysisIJCAR 2020 - International Joint Conference on Automated ReasoningParis, FranceJune 2020, 1-19
  HALback to text
• 18 inproceedingsAndréA. Hirschowitz, TomT. Hirschowitz and AmbroiseA. Lafont. Modules over monads and operational semantics5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)167Leibniz International Proceedings in Informatics (LIPIcs)Paris, France2020, 12:1--12:23
  HALDOIback to text
• 19 inproceedingsÉtienneÉ. Miquey. Revisiting the duality of computation: an algebraic analysis of classical realizability modelsCSL 2020 - Conference on Computer Science Logic152LIPIcs, CSL 2020Barcelone, SpainJanuary 2020, 1-52
  HALDOIback to text
• 20 inproceedingsAndersA. Mörtberg and LoïcL. Pujet. Cubical Synthetic Homotopy TheoryCPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and ProofsNew Orleans, United Stateshttps://popl20.sigplan.org/home/CPP-2020January 2020, 1-14
  HALDOIback to text
• 21 inproceedingsPierre-MarieP.-M. Pédrot. Russian Constructivism in a Prefascist TheoryLICS 2020 - Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer ScienceSaarbrücken, GermanyNovember 2020, 1-14
  HALDOIback to text

Conferences without proceedings

• 22 inproceedingsÉtienneÉ. Miquey, XavierX. Montillet and GuillaumeG. Munch-Maccagnoni. Dependent Type Theory in Polarised Sequent Calculus (abstract)TYPES 2020 - 26th International Conference on Types for Proofs and ProgramsTorino, Italyhttps://types2020.di.unito.it/March 2020, 1-3
  HALback to text
• 23 inproceedings GuillaumeG. Munch-Maccagnoni. Towards better systems programming in OCaml with out-of-heap allocation ML Workshop Jersey City, United States August 2020
  HAL back to text

Doctoral dissertations and habilitation theses

• 24 thesis AssiaA. Mahboubi. Machine-checked computer-aided mathematics Université de Nantes (UN), Nantes, FRA. January 2021
  HAL back to text

Reports & preprints

• 25 misc AntoineA. Allioux, EricE. Finster and MatthieuM. Sozeau. Types are internal infinity-groupoids January 2021
  HAL back to text
• 26 misc SophieS. Bernard, CyrilC. Cohen, AssiaA. Mahboubi and Pierre-YvesP.-Y. Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory February 2021
  HAL
• 27 misc MevenM. Bertrand, KenjiK. Maillard, NicolasN. Tabareau and ÉricÉ. Tanter. Gradualizing the Calculus of Inductive Constructions November 2020
  HAL back to text
• 28 misc GuilhemG. Jaber and Andrzej S.A. Murawski. Complete trace models of state and control January 2021
  HAL
• 29 misc MarieM. Kerjean. Chiralities in topological vector spaces February 2020
  HAL DOI back to text
• 30 misc MevenM. Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions February 2021
  HAL