Inductive types are a fundamental abstraction mechanism in type theory and proof assistants, supporting the definition of data structures and rich specifications. Nested inductive types extend this mechanism by allowing constructors to use parametric types instantiated with the type being defined (lists or trees of the type to be defined). They are widely used in large verification projects – including CompCert, Iris, Verinum, and MetaRocq – to express complex, structured specifications. Despite this widespread use, the treatment of nested inductive types in both and is unsatisfactory. rejects many practical definitions while accepts definitions for which no usable elimination principle can be defined. Neither system provides reliable automatic generation of elimination principles. As a result, developers must define custom eliminators by hand, leading to fragility, duplication, and significant proof engineering overhead. This paper introduces a novel validity criterion for nested inductive types that guarantees that they can be elaborated into well-formed mutual inductive types. Under this criterion, the elimination principle for the original nested definition is provably equivalent to that of its elaborated mutual form. Our condition strictly generalizes Lean’s current check while ruling out exactly the problematic cases accepted in . Using this foundation, we give a systematic method for automatically generating correct elimination principles for nested inductive types, and we provide an implementation integrated into , along with an implementation plan for .

Proof assistants based on dependent type theory-such as AGDA, LEAN, and ROCQ-employ different universes to classify types, typically combining a predicative tower for computationally relevant types with a possibly impredicative universe for proof-irrelevant propositions. Several other universes with specific logical and computational principles have been explored in the literature. In general, a universe is characterized by its sort (e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve modularity and better avoid code duplication, sort polymorphism has recently been introduced and integrated in the ROCQ prover. However, we observe that, due to its unbounded formulation, sort polymorphism is currently insufficiently expressive to abstract over valid definitions with a single polymorphic schema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between different sorts must be carefully controlled, as exemplified by the forbidden elimination of irrelevant terms to produce relevant ones. As a result, generic functions that eliminate values of inductive types from one sort to another cannot be made polymorphic; dually, polymorphic records that encapsulate attributes of different sorts cannot be defined. This lack of expressiveness also breaks the possibility to infer principal types, which is highly desirable for both metatheoretical and practical reasons. To address these issues, we extend sort polymorphism with bounds that reflect the required elimination constraints on sort variables. We present the metatheory of bounded sort polymorphism, paying particular attention to the consistency of the resulting constraint graph. We implement bounded sort polymorphism in ROCQ and illustrate its benefits through concrete examples. Bounded sort polymorphism with elimination constraints is a natural and general solution that effectively addresses current limitations and fosters the development of, and practical experimentation with, multi-sorted type theories.

Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.

CoQ is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in CoQ is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in CoQ. This article presents the first implementation of a type checker for the kernel of CoQ (without the module system, template polymorphism and eta-conversion), which is proven sound and complete in CoQ with respect to its formal specification. Note that because of G & ouml;del's second incompleteness theorem, there is no hope to prove completely the soundness of the specification of CoQ inside CoQ (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the METACoQ project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of CoQ. It is worth mentioning that during the verification process, we have found a source of incompleteness in CoQ's official type checker, which has then been fixed in CoQ 8.14 thanks to our work. In addition to the kernel implementation, another essential feature of CoQ is the so-called extraction mechanism: the production of executable code in functional languages from CoQ definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for CoQ in the future.

One of the central claims of fame of the Coq proof assistant is extraction, i.e. the ability to obtain efficient programs in industrial programming languages such as OCaml, Haskell, or Scheme from programs written in Coq’s expressive dependent type theory. Extraction is of great practical usefulness, used crucially e.g. in the CompCert project. However, for such executables obtained by extraction, the extraction process is part of the trusted code base (TCB), as are Coq’s kernel and the compiler used to compile the extracted code. The extraction process contains intricate semantic transformation of programs that rely on subtle operational features of both the source and target language. Its code has also evolved since the last theoretical exposition in the seminal PhD thesis of Pierre Letouzey. Furthermore, while the exact correctness statements for the execution of extracted code are described clearly in academic literature, the interoperability with unverified code has never been investigated formally, and yet is used in virtually every project relying on extraction. In this paper, we describe the development of a novel extraction pipeline from Coq to OCaml, implemented and verified in Coq itself, with a clear correctness theorem and guarantees for safe interoperability. We build our work on the MetaCoq project, which aims at decreasing the TCB of Coq’s kernel by re-implementing it in Coq itself and proving it correct w.r.t. a formal specification of Coq’s type theory in Coq. Since OCaml does not have a formal specification, we make use of the project specifying the semantics of the intermediate language of the OCaml compiler. Our work fills some gaps in the literature and highlights important differences between the operational semantics of Coq programs and their extraction. In particular, we focus on the guarantees that can be provided for interoperability with unverified code, and prove that extracted programs of first-order data type are correct and can safely interoperate, whereas for higher-order programs already simple interoperations can lead to incorrect behaviour and even outright segfaults.

By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.

Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity , is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte : basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class functions, type polymorphism and modules. As logical systems, however, modularity is lacking, and understandably so: incompatible reasoning principles -- such as univalence and uniqueness of identity proofs -- can indirectly lead to logical inconsistency when used in a given development, even when they appear to be confined to different modules. The lack of logical modularity in proof assistants also hinders the adoption of richer programming constructs, such as effects. We propose the multiverse, a general type-theoretic approach to endow proof assistants with logical modularity. The multiverse consists of multiple universe hierarchies that statically describe the reasoning principles and effects available to define a term at a given type. We identify sufficient conditions for this structuring to modularly ensure that incompatible principles do not interfere, and to locally restrict the power of dependent elimination when necessary. This extensible approach generalizes the ad-hoc treatment of the sort of propositions in the Coq proof assistant. We illustrate the power of the multiverse by describing the inclusion of Coq-style propositions, the strict propositions of Gilbert et al., the exceptional type theory of Pédrot and Tabareau, and general axiomatic extensions of the logic.

Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implementations. However, proof assistant implementations themselves are seldom verified, although they take a major share of the trusted code base in any such certification effort. In this area, proof assistants based on Higher-Order Logic enjoy stronger guarantees, as self-certified implementations have been available for some years. One cause of this difference is the inherent complexity of dependent type theories together with their extensions with inductive types, universe polymorphism and complex sort systems, and the gap between theory on paper and practical implementations in efficient programming languages. MetaCoq is a collaborative project that aims to tackle these difficulties to provide the first fully-certified realistic implementation of a type checker for the full calculus underlying the Coq proof assistant. To achieve this, we refined the sometimes blurry, if not incorrect, specification and implementation of the system. We show how theoretical tools from this community such as bidirectional type-checking, Tait-Martin-L\"of/Takahashi's confluence proof technique and monadic and dependently-typed programming can help construct the following artefacts: a specification of Coq's syntax and type theory, the Polymorphic Cumulative Calculus of (Co)-Inductive Constructions (PCUIC); a monad for the manipulation of raw syntax and interaction with the Coq system; a verification of PCUIC's metatheory, whose main results are the confluence of reduction, type preservation and principality of typing; a realistic, correct and complete type-checker for PCUIC; a sound type and proof erasure procedure from PCUIC to untyped lambda-calculus, i.e., the core of the extraction mechanism of Coq.

Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda. The actual objects that can be checked are not proof-terms, but derivations of proof-terms. This suggests that any derivation of ETT can be translated into a typecheckable proof term of intensional type theory (ITT). However, this result, investigated categorically by Hofmann in 1995, and 10 years later more syntactically by Oury, has never given rise to an effective translation. In this paper, we provide the first effective syntactical translation from ETT to ITT with uniqueness of identity proofs and functional extensionality. This translation has been defined and proven correct in Coq and yields an executable plugin that translates a derivation in ETT into an actual Coq typing judgment. Additionally, we show how this result is extended in the context of homotopy type theory to a two-level type theory.

At the heart of Coq’s kernel is an implementation of a typechecker for the (Polymorphic, Cumulative) Calculus of Inductive Constructions (PCUIC), a well defined type-theoretic system. However, in its entirety, the kernel consists of 20k lines of relatively complicated OCaml code that has to be trusted. This is due on one hand to the complexity of Coq’s full calculus, including modules and sections, and on the other hand to the inclusion of high-performance conversion tests (bytecode and native compilation) along with user-friendly features like delayed checking of opaque proofs and support for nested global declarations. We report on our ongoing work on verifying a reasonably large subset of Coq’s kernel in Coq, as part of the MetaCoq project [Anand et al. 2018; Sozeau et al. 2019]. The MetaCoq project provides metaprogramming facilities to turn terms and declarations in Coq into a reified inductive datatype of CIC terms. We specify typing and reduction relations for PCUIC and prove meta-theoretical properties like confluence and subject reduction. Based on this specification, we then implement a verified, sound type checker. In addition to the kernel implementation, an essential feature of Coq is so-called extraction [Letouzey 2004]: the production of executable code in functional languages from Coq definitions. We will present a verified version of this subtle type-and-proof erasure step, which links to the CertiCoq verified compiler going from erased terms to CompCert’s C-light language. During the presentation, we hope to demonstrate uses of the checker and extraction procedure and provide empirical evaluation results.1 This work also provides insights into possible simplifications or generalizations of the calculus and its implementation. Definition (Cot Cot Codet2). French, Interjection: (1) cackle (the cry of a hen, especially one that has laid an egg)

This final version contains mainly bugfixes over 1.2beta2, see announcement for more details. It has been tested with the 8.10beta1 release of Coq.

Definitional equality—or conversion—for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this paper, taking inspiration from homotopy type theory, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) by using techniques coming from recent development on dependent pattern matching without UIP. We show the generality of our approach by providing implementations for both Coq and Agda, both of which are planned to be integrated in future versions of those proof assistants.

Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.

Coq is built around a well-delimited kernel that perfoms typechecking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq (without the module system and template polymorphism), which is proven correct in Coq with respect to its formal specification and axiomatisation of part of its metatheory. Note that because of Gödel's incompleteness theorem, there is no hope to prove completely the correctness of the specification of Coq inside Coq (in particular strong normalisation or canonicity), but it is possible to prove the correctness of the implementation assuming the correctness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the MetaCoq project which provides metaprogramming facilities to work with terms and declarations at the level of this kernel. Our type checker is based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq and the verification of a relatively efficient and sound type-checker for it. In addition to the kernel implementation, an essential feature of Coq is the so-called extraction: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type-and-proof erasure step, therefore enabling the verified extraction of a safe type-checker for Coq.

Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet clear how to extend them to handle univalence internally. In this paper, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. In particular, univalent parametricity strengthens parametricity to ensure preservation of type equivalences. We present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. Our approach handles both type and term dependency. We study how to maximize the effectiveness of these transports in terms of computational behavior, and identify a fragment useful for certified programming on which univalent transport is guaranteed to be effective. This work paves the way to easier-to-use environments for certified programming by supporting seamless programming and proving modulo equivalences.

Template-Coq is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declarations , as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq's AST in Gallina. Recently, its use was extended for the needs of the CertiCoq certified compiler project, which uses it as its front-end language and to derive parametricity properties, and the work of Forster on extracting Coq terms to a CBV λ-calculus. However, the syntax currently lacks semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq itself. This is an issue for CertiCoq where both a non-deterministic small step semantics and a deterministic call-by-value big step semantics had to be defined and preserved, without an official reference specification to refer to. Our hope with this work is to remedy this situation and provide a formal semantics of Coq's implemented type theory, that can independently be refined and studied. By implementing a (partial) independent checker in Coq, we can also help formalize certified translations from Coq to Coq.