Coq. The correctness proof requires fairly involved reasoning with an accumulator to account for these dependencies. It also requires particular inversion lemmas which have to be set up very carefully, accounting for the non-determinism of the erasure relation. We refer the reader to the Coq formalization for details.

# 7 RELATED WORK

Mechanized meta-theory and certified type-checkers. Barras [1996] proposed the first substantial work in the area of formal correctness of proof assistants by proving subject reduction and strong normalization of a subset of Coq (namely CoC, the Calculus of Constructions) in Coq, together with the correctness of a type checker for this subset, which can then be extracted to Caml Light. Our work is a spiritual successor to this one, but is more focused on verification of an implementation that on proving strong normalization of the system. Furthermore, we deal with a subset of Coq that is almost feature complete, compared to the rather small fragment considered by Barras [1996], which for instance does not contain any inductive types. This work was the inspiration of other metatheoretical studies of extensions to CoC [Sozeau 2008] and general Pure Type Systems [Siles and Herbelin 2012] in Coq, similarly focusing on idealized, small languages.

Abel et al. [2018b] present a normalization-by-evaluation algorithm for deciding definitional equality of an idealized dependent type theory with only one universe and natural numbers, verified in Agda, implemented using a stronger type theory with inductive-recursive types [Dybjer and Setzer 2003]. Their methodology provides soundness and completeness results and deals with $\eta$-laws by comparing $\beta\eta$ normal forms, while we do not handle these. However, their algorithm is rather naive, as it systematically reduces terms to deep normal form, and works directly on the proof of reducibility. On the contrary, our implementation does not necessarily compute deep normal forms, which is crucial for performance in practice. Moreover, we use the *Prop/Type* distinction of Coq to enable extraction of a reasonably efficient implementation using erasure. Finally, they stop at definitional equality, but do not tackle decidability of type checking.

Strub et al. [2012] provide a methodology to build a self-certifying type checker for a large subset of $F^*$, whose metatheory is formalized in Coq. Our work is complementary in the sense that it reduces the trusted code base involved in that methodology to the specification of PCUIC, and no longer to its ML kernel implementation. Furthermore, they only tackle soundness of the type checker, while we also prove completeness.

Anand and Rahli [2014] formalize the meta-theory of the Nuprl proof assistant in Coq and prove its consistency, but do not verify programs related to it.

Œuf [Mullen et al. 2018] formalizes a simply typed subset of Coq with predetermined base types and the corresponding eliminators and provide a verified compiler from this language to Assembly code. As such our work is on a much larger scale as it deals with almost all of Coq.

Certified erasure and extraction. Hupel and Nipkow [2018] implement a verified extraction from Isabelle/HOL into CakeML. The first phase of their compiler consists of a proof-producing translation implemented in Standard ML, translating terms of Isabelle/HOL into a deeply embedded term language. The second part of their compiler is a verified translation from the deeply embedded language into CakeML.

Myreen and Owens [2014] implement a certifying extraction from HOL Light code to CakeML. Their approach can translate programs in a state-and-exception monad into stateful ML code and was used by Abrahamsson et al. [2022] to extract a verified HOL Light compiler to CakeML.

Forster and Kunze [2019] report on a certifying translation from a subset of Coq to the weak call-by-value $\lambda$-calculus. Their extraction is implemented in the *METACOQ* framework as well, but they produce correctness proofs for their extract in Coq's tactic language LTac.
saying that the produced term is in weak-head normal form (Fig. 13):

**Theorem reduce_term_complete X:**

$$ \forall \Gamma t (h : \forall \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \text{welltyped} \Sigma \Gamma t) \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \| \text{whnf} \Sigma \Gamma (\text{reduce\_term} \Gamma t h) \|. $$

### 6.3.3 Safe Conversion.
We define safe conversion and cumulativity while proving it sound and complete by having it return either a conversion or cumulativity proof for its inputs, or an error message together with a proof of the negation of conversion or cumulativity, using the monadic style explained in §6.1.

At the beginning of the section, we hinted at the fact that our conversion and cumulativity checker proceeds in different phases. We record the current phase using what we call *state*, defined below.

**Inductive state** := **Reduction** | **Term** | **Args** | **Fallback**.

Initially, we are in **Reduction** mode in which we start by weak-head reducing both terms (except for $\delta$-reduction, meaning we do not unfold any definition). In this phase we also decompose each term into a term and a stack, moving all application nodes to the stack and consuming them when possible, as we described in §6.3.2.

We then move to the **Term** phase where we inspect the two terms below their respective stacks. Essentially in this phase we check whether the two terms have the same head, in which case we compare the subterms recursively (back to phase **Reduction**). For instance, when comparing two $\lambda$-abstractions, this is sufficient and we can directly raise an error message if subterm comparison fails. The proof of completeness ensures that we are not missing a case. It exploits properties of injectivity of weak-head normal forms (shown in PCUIC: **Conversion** and PCUIC: **ConvCumInversion**), which follow from confluence. There are still some special cases to consider. For instance, when comparing two constants, we first check whether they happen to be instances of the exact same constant (i.e., the same global reference with equal universe instances), but in case they are not, it does not necessarily mean that the terms are different. We then unfold one of the constants and resume comparison from the **Reduction** phase. We need to do similar things for pattern matching, (co)fixpoints and projections.

When the previous phase succeeds (i.e., when the two terms have the same head and convertible subterms), we proceed to verify that the applications present on top of the two stacks are themselves pointwise convertible. This **Args** phase simply looks through the two stacks and compares the application arguments (in **Reduction** mode). If this succeeds, we can conclude the whole terms are indeed in the conversion or cumulativity relation.

In the **Term** phase we may however end up with two terms with different heads. Once again, this does not mean that they are not in the cumulativity relation. We end up in the **Fallback** case in which we check whether one of the terms could be further reduced by unfolding a constant. This happens when the term is itself a constant, but also when it is a pattern matching or projection applied to a stuck term, or a fixpoint whose recursive argument is stuck. In those cases we reduce the argument to weak-head normal form (including $\delta$-reductions) and check whether we can make progress (e.g., it is a constructor for pattern matching). If progress can be made, we go back to the **Term** phase (no need to go through **Reduction** again as the terms are still in weak-head normal form). In case no progress can be made on either side, as a last resort we compare the terms syntactically. This is needed for heads like sorts or variables that have not been considered before, as well as for all neutral expressions (i.e., stuck terms).

These phases are defined respectively in open recursion through the functions **_isconv_red**, **_isconvprog**, **_isconv_args**, and **_isconv_fallback**. They are combined together into **isconv_full**.
Barras and Bernardo [2008] propose the Implicit Calculus of Constructions as an alternative way to specify computationally irrelevant content, whose pen-and-paper metatheory extends that of CIC [Bernardo 2015] and with a complex type inference decidability proof. It could be studied in the present framework.

Glondu [2012] verifies the syntactic proof given by Letouzey [2004] in Coq. They formalize a correctness proof w.r.t. arbitrary small-step reduction, but work in a slightly idealized calculus with no exploitable correspondence to the actual implementation of Coq. They do not consider a verified type checker or the verification of an executable type and proof erasure function.

*Work building on META-CoQ.* Annenkov et al. [2021] build on META-CoQ's verified erasure to extend the extraction capabilities of CoQ in a verified way to more programming languages such as the web functional language Elm, the Liquidity and CameLIGO smart contract languages, or even Rust as part of the ConCert project [Annenkov et al. 2022; Nielsen et al. 2023]. Olesen [2021] goes further and extends ConCert to obtain certified extraction to the Futhark language.

The CERTICOQ project [Anand et al. 2017] is a work-in-progress verified compiler from CoQ to C (as specified in COMPCERT). Before entering a complex compilation chain with various intermediate languages and optimizations, CERTICOQ uses the type and proof erasure procedure described in this paper. Consequently, an end-to-end correctness theorem for CERTICOQ would be composed of an end-to-end theorem connecting the weak call-by-value evaluation relation of $\lambda_\square$ to the operational semantics of the compiled C program and our correctness theorem for the erasure function.

# 8 CONCLUSION AND FUTURE WORK

The whole development we presented includes the certified type-preserving translation from CoQ's syntax to PCUIC's syntax, specification of typing, metatheory, verified checker and conversion and erasure phase. All this is done assuming the existence of a guard condition on fixpoints and cofixpoints that endows the system with strong normalization. From these specifications and implementations, a number of applications are possible. Certified translations and plugins were surveyed by Sozeau et al. [2019a], we focus here on what our contributions bring in addition.

With respect to CoQ's currently implemented type theory, we depart by not considering $\eta$-equalities for functions and primitive record types in our specification of definitional equality. We leave these extensions to future work. We also leave out the module system: thankfully, it is orthogonal to the term language and it is unclear if we should not rather explain them through an elaboration, in the style of Rossberg et al. [2014] rather than bake them in the core calculus.

In the future, we want to extend PCUIC and erasure to also handle the sort SProp [Gilbert et al. 2019], implemented since CoQ 8.10. Since SProp is a proof-irrelevant analogue to Prop, adapting erasure is almost trivial: SProp can be erased like Prop and eliminations need no special care.

We also want to extend our account of erasure to other evaluation orders (most notably call-by-name evaluation to be able to target lazy languages). Currently, we support axioms which do not block call-by-value evaluation—which is rarely the case. Letouzey [2004] introduces a semantic account of erasure correctness, which would allow the treatment of axioms. We want to verify such a semantic correctness theorem.

Another exciting endeavor is to refine the specification to fit into the standard models of dependent type theory, beginning with the set theoretic model developed by Barras [1999]. A first step towards this goal will be to tackle the difficult guard and productivity conditions.

# ACKNOWLEDGMENTS

The work described in this paper received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101024493.
which involves an order slightly more complicated than for reduction as the phase (state) is also taken into account. We also call this order R and show it is well founded.

Finally, starting from empty stacks, we define conversion checking for well-typed terms, named `isconv_term`, and show it sound and complete. Again, the theorems are stated for any abstract environment X.

**Theorem isconv_term{term\_sound} X:**

$$ \forall \Sigma (wf\Sigma : X \sim_{ext} \Sigma) \Gamma R_1 e t_1 h_1 t_2 h_2, $$

$$ \mathit{isconv\_term} \Gamma R_1 t_1 h_1 t_2 h_2 = \mathit{ConvSuccess} \rightarrow \| \Sigma ; \Gamma \vdash t_1 \preceq_s^{R_1 e} t_2 \|. $$

**Theorem isconv\_term\_complete X:**

$$ \forall \Sigma (wf\Sigma : X \sim_{ext} \Sigma) \Gamma R_1 e t_1 h_1 t_2 h_2 e, $$

$$ \mathit{isconv\_term} \Gamma R_1 t_1 h_1 t_2 h_2 = \mathit{ConvError} e \rightarrow \neg \| \Sigma ; \Gamma \vdash t_1 \preceq_s^{R_1 e} t_2 \|. $$

## 6.4 A Typechecking Algorithm for PCUIC

Given the work already done in §4.3, the definition of a type checking algorithm itself is quite straightforward: it closely follows the structure laid out by the mutually defined bidirectional judgments, and poses no termination issue—as opposed to conversion—since the type checker operates by a simple induction on the structure of the term. Actually, rather than a type checker, the main function we define is type inference,<fnref n="28" /> from which we can easily define type checking. In more details, the function takes a term t in well-formed environment Σ and context Γ, and returns a type together with a derivation of Σ ; Γ ⊢ t ▷ A, the inductively defined inference judgment, so the function is correct by construction. We cannot separate the definition from the correctness proof, since the conversion checker that is called as a sub-routine expects a well-typed term as input in order to be terminating. We do not detail the definition of type inference here, as it follows scrupulously the bidirectional representation, we just need to replace propositional assumptions, such as convertibility or universe constraints, by the corresponding decision procedures.

We also provide a retyping algorithm, which takes a term and a proof that this term is well typed and computationally infers an explicit type for it. This is an optimized version of type inference where many conversion and type-checking tests can be elided, because we know they are valid thanks to the assumption that the initial term is well typed. For instance, to retype an application `tApp tu`, it is only necessary to retype `t` and get a type `tProd na A B`, and we can directly return `B{0 := u}`, as we know that `u` checks against `A` since the term is well typed. This retyping algorithm is used by extraction, to detect types and proofs in the term that can be erased.

Finally, we define a function checking well-formedness of an environment, by iteratively checking each constant or inductive declaration as specified in §3.6.

### 6.4.1 Performance of our Type Checker.
We ran the extracted code of our type checker on the `HoTT\_light.v` file of the Equations library on an 11th Gen Intel® Core™ i7-1165G7 @ 2.80GHz with CoQ version 8.19.0 and OCaml version 4.14.1. We have ensured that no thermal throttling occurs and the frequency of 2.80GHz is maintained. On this file, our checker runs on average 11.2 times longer than CoQ's kernel. We conjecture that this slowdown is due to our very naïve universe checking algorithm.

## 7 TYPE AND PROOF ERASURE FOR PCUIC

One of the key features of the CoQ proof assistant is extraction [Letouzey 2004], used for instance in the CompCert compiler [Leroy 2006]. The current implementation of extraction [Letouzey 2002]

<footnote n="28">²⁸Which is decidable due to our Church-style syntax, i.e., using annotated abstractions, as opposed to a Curry-style one.</footnote>
## REFERENCES

Martin Abadi, Luca Cardelli, P-L Curien, and J-J Lévy. 1991. Explicit substitutions. *Journal of functional programming* 1, 4 (1991), 375–416.

Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2004. Representing Nested Inductive Types Using W-Types. In *Automata, Languages and Programming, Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 59–71.

Andreas Abel, Joakim Öhman, and Andrea Vezzosi. 2018a. Decidability of conversion for type theory in type theory. *PACMPL* 2, POPL (2018), 23:1–23:29. https://doi.org/10.1145/3158111

Andreas Abel, Joakim Öhman, and Andrea Vezzosi. 2018b. Decidability of conversion for type theory in type theory. *PACMPL* 2, POPL (2018), 23:1–23:29. https://doi.org/10.1145/3158111

Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: programming infinite structures by observations. In *The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013*, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 27–38. https://doi.org/10.1145/2429069.2429075

Oskar Abrahamsson, Magnus O Myreen, Ramana Kumar, and Thomas Sewell. 2022. Candle: A Verified Implementation of HOL Light. In *13th International Conference on Interactive Theorem Proving (ITP 2022)*. Schloss Dagstuhl-Leibniz-Zentrum für Informatik.

Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In *CoqPL*. Paris, France. http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq

Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. In *ITP 2018 (Lecture Notes in Computer Science, Vol. 10895)*, Jeremy Avigad and Assia Mahboubi (Eds.). Springer, 20–39. https://doi.org/10.1007/978-3-319-94821-8_2

Abhishek Anand and Vincent Rahli. 2014. Towards a Formally Verified Proof Assistant. In *Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8558)*, Gerwin Klein and Ruben Gamboa (Eds.). Springer, 27–44. https://doi.org/10.1007/978-3-319-08970-6_3

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2021. Extracting smart contracts tested and verified in Coq. In *Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs*. 105–121.

Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2022. Extracting functional programs from Coq, in *Coq. Journal of Functional Programming* 32 (2022), e11.

ANSSI. 2021. *Requirements on the Use of Coq in the Context of Common Criteria Evaluations*. v1.1. French National Cybersecurity Agency. https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf.

Bruno Barras. 1996. *Coq en Coq*. Rapport de Recherche 3026. INRIA.

Bruno Barras. 1999. *Auto-validation d'un système de preuves avec familles inductives*. Thèse de Doctorat. Université Paris 7. http://pauillac.inria.fr/~barras/publi/these_barras.ps.gz

Bruno Barras. 2012. *Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families*. Habilitation Thesis.

Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In *FoSSaCS (Lecture Notes in Computer Science, Vol. 4962)*, Roberto M. Amadio (Ed.). Springer, 365–379.

Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, and Robert E. Tarjan. 2015. A New Approach to Incremental Cycle Detection and Related Problems. *ACM Trans. Algorithms* 12, 2, Article 14 (Dec. 2015), 22 pages. https://doi.org/10.1145/2756553

Bruno Bernardo. 2015. *Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable. (An implicit Calculus of Constructions with dependent sums and decidable type inference)*. Ph. D. Dissertation. École Polytechnique, Palaiseau, France. https://tel.archives-ouvertes.fr/tel-01197380

Marc Bezem and Thierry Coquand. 2022. Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. *Theoretical Computer Science* 913 (2022), 1–7. https://doi.org/10.1016/j.tcs.2022.01.017

T. Coquand. 1989. *Metamathematical investigations of a calculus of constructions*. Ph. D. Dissertation. https://hal.inria.fr/inria-00075471

Thierry Coquand and Gérard Huet. 1988. The Calculus of Constructions. *Information and Computation* 76, 2–3 (February/–March 1988), 95–120.

Thierry Coquand and Christine Paulin. 1990. Inductively defined types. In *COLOG-88*, Per Martin-Löf and Grigori Mints (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 50–66.

Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. *Comput. Surveys* 54, 5, Article 98 (2021), 38 pages. https://doi.org/10.1145/3450952
<figure><img src="image_5.png" /><figcaption>Fig. 16. Syntax of $\lambda_{\square}$</figcaption></figure>

consists of a general procedure to erase types and proofs and several mechanisms to extract these erased terms into industrial programming languages like OCAML, HASKELL, or SCHEME. We verify the type and proof erasure procedure for PCUIC with respect to big-step call-by-value evaluation as introduced in §5.6. In future work, we plan to also verify Coq's extraction mechanism to OCAML and other languages. Already Letouzey's work [Letouzey 2004] separates the erasure to pure, untyped $\lambda$-calculus (equivalent to ours) from the MiniML extraction that is actually implemented by extraction (inserting `Obj.magic` to embed untyped terms and applying optimizations).

In this section, we first introduce the target calculus of erasure, which is a simplified version of PCUIC with one extra constructor $\square$ denoting erased terms. We then define an erasure function $\mathcal{E}$, using the retyping algorithm from §6.4. Following Letouzey [2004], we introduce an erasure relation extending the erasure function, prove its correctness and deduce the strongest possible correctness result for the erasure function: if a program of first-order inductive type (i.e., an inductive type containing no proofs or functions) evaluates to a value, its erasure evaluates to the same value. As a corollary, we also get that in case the return type of a function $f$ is a first-order inductive type, $f$ can be erased separately to some function which will evaluate to the same value as $f$ once applied to enough arguments.

Note that, like in the extraction currently implemented in Coq, the rule `Prop ≤ Type` has to be disabled for type checking (using the flag structure explained at the end of §3.5) to ensure that erasability is stable by expansion.

## 7.1 The Target Calculus $\lambda_{\square}$

The target of the type and proof erasure procedure is $\lambda_{\square}$, an untyped $\lambda$-calculus. $\lambda_{\square}$ is syntactically similar to PCUIC (see syntax in Fig. 16). It has the same constructors, but subterms which can only contain types are left out (because they would be erased anyway). Furthermore, $\lambda_{\square}$ has an additional constructor $\square$ denoting computationally meaningless content which was erased. Technically, the code shares the same syntax as that for PCUIC, but inside a different module. To avoid confusion and the additional complexity of considering modules, we have taken the liberty to prefix every term with `E.` in the definition.

The weak call-by-value (big-step) evaluation relation for $\lambda_{\square}$ is defined like for PCUIC (see §5.6), with three amendments:<fnref n="29" />

$$ (1) \text{ If } \Sigma \vdash a \Downarrow \square \text{ then } \Sigma \vdash E.tApp a t \Downarrow \square. $$

<footnote n="29">²⁹We present only the changes for big-step evaluation.</footnote>
Peter Dybjer and Anton Setzer. 2003. Induction-recursion and initial algebras. *Annals of Pure and Applied Logic* 124, 1-3 (2003), 1-47. https://doi.org/10.1016/S0168-0072(02)00096-9

Yannick Forster and Fabian Kunze. 2019. A certifying extraction with time bounds from Coq to call-by-value λ-calculus. In *Tenth International Conference on Interactive Theorem Proving*. Springer.

Herman Geuvers. 2007. Inconsistency of classical logic in type theory. *Unpublished notes* (2007). http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional Proof-Irrelevance without K. In *46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) (POPL)*. Lisbon, Portugal. https://hal.inria.fr/hal-01859964

Carlos Eduardo Giménez. 1996. *Un calcul de constructions infinies et son application à la vérification de systèmes communicants*. Ph. D. Dissertation. Ecole Normale Supérieure de Lyon. ftp://ftp.inria.fr/INRIA/LogiCal/Eduardo.Gimenez/thesis.ps.gz

J.-Y. Girard. 1972. *Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur*. Ph. D. Dissertation. Université Paris 7.

Stéphane Glondu. 2012. *Vers une certification de l'extraction de Coq*. Ph. D. Dissertation. Université Paris Diderot.

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. 2019. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In *ITP 2019 - 10th Conference on Interactive Theorem Proving*. Portland, United States. https://hal.inria.fr/hal-02167236

Robert Harper and Robert Pollack. 1991. Type Checking with Universes. *Theor. Comput. Sci.* 89, 1 (1991), 107-136.

Gérard Huet. 1988. Extending the Calculus of Constructions with Type:Type. (1988). http://pauillac.inria.fr/~huet/PUBLIC/tytyp.pdf

Lars Hupel and Tobias Nipkow. 2018. A verified compiler from Isabelle/HOL to CakeML. In *European Symposium on Programming*. Springer, 999-1026.

Antonius J. C. Hurkens. 1995. A simplification of Girard's paradox. In *Typed Lambda Calculi and Applications*, Mariangiola Dezani-Ciancaglini and Gordon Plotkin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 266-278.

Meven Lennon-Bertrand. 2021. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In *12th International Conference on Interactive Theorem Proving (ITP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193)*, Liron Cohen and Cezary Kaliszyk (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ITP.2021.24

Meven Lennon-Bertrand. 2022. *Bidirectional Typing for the Calculus of Inductive Constructions*. PhD Thesis.

Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In *33rd symposium Principles of Programming Languages*. ACM Press, 42-54. http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf

Pierre Letouzey. 2002. A New Extraction for Coq. In *TYPES'02 (Lecture Notes in Computer Science, Vol. 2646)*, Herman Geuvers and Freek Wiedijk (Eds.). Springer, 200-219.

Pierre Letouzey. 2004. *Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq*. Thèse de Doctorat. Université Paris-Sud. http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.pdf

Per Martin-Löf. 1984. *Intuitionistic type theory*. Studies in Proof Theory, Vol. 1. Bibliopolis. iv+91 pages.

Per Martin-Löf. 1998. An intuitionistic theory of types. In *Twenty-five years of constructive type theory (Venice, 1995)*, Giovanni Sambin and Jan M. Smith (Eds.). Oxford Logic Guides, Vol. 36. Oxford University Press, 127-172.

Conor McBride and James McKinna. 2004. The view from the left. *J. Funct. Program*. 14, 1 (2004), 69-111.

Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman. 2018. (Euf: minimizing the Coq extraction TCB. In *Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018*, June Andronick and Amy P. Felty (Eds.). ACM, 172-185. https://doi.org/10.1145/3167089

Magnus O Myreen and Scott Owens. 2014. Proof-producing translation of higher-order logic into pure and stateful ML. *Journal of Functional Programming* 24, 2-3 (2014), 284-315.

Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. 2023. Formalising Decentralised Exchanges in Coq. In *Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs*. 290-302.

Kristian Knudsen Olesen. 2021. Extracting certified Futhark code from Coq. (2021).

Lawrence C Paulson. 1986. Constructing Recursion operators in Intuitionistic Type Theory. *Journal of Symbolic Computation* 2, 4 (1986), 325-355. https://www.sciencedirect.com/science/article/pii/S0747717186800025/pdf?md5=4df038c66455b64762734b09ad0ea894&isDTMRedir=Y&pid=1-s2.0-S0747717186800025-main.pdf&valck=1

Pierre-Marie Pédrot and Nicolas Tabareau. 2017. An effectful way to eliminate addiction to dependence. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*. IEEE Computer Society, 1-12. https://doi.org/10.1109/LICS.2017.8005113

Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. *ACM Transactions on Programming Languages and Systems* 22, 1 (Jan. 2000), 1-44. http://doi.acm.org/10.1145/345099.345100
Equations $\mathcal{E} \Gamma (Ht : \forall \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \text{welltyped } \Sigma \Gamma t) : \mathbf{E}.\text{term} := \mathcal{E} \Gamma H\Gamma t \text{ with } (\mathbf{is}\_\text{erasable} \times \Gamma t Ht) :=$
$\begin{aligned}
& \{ \text{left } \mathbf{is}\_\text{er} \coloneqq \square; \\
& \text{right } \mathbf{not}\_\mathbf{is}\_\text{er} \text{ with } t \coloneqq \{ \\
& \qquad t\text{Rel } i \coloneqq \mathbf{E}.\text{tRel } i \\
& \qquad t\text{Const } k \text{ u } \coloneqq \mathbf{E}.\text{tConst } k\text{ \\
& \qquad t\text{Lambda } na \text{ b } b' \coloneqq \mathbf{E}.\text{tLambda } na.(\text{binder\_name}) (\mathcal{E} (\Gamma, na : b) b') \\
& \qquad t\text{App } f u \coloneqq \mathbf{E}.\text{tApp} (\mathcal{E} \Gamma f \_) (\mathcal{E} \Gamma u \_) \\
& \qquad (* \dots *) \}}
\end{aligned}$

<caption>Fig. 17. Erasure function (excerpt)</caption>

(2) If $\Sigma \vdash a \Downarrow \square$ and $\Sigma \vdash t \Downarrow \dots \Downarrow \square \Downarrow v$ then $\Sigma \vdash \mathbf{E}.\mathbf{tCase} (i, p) a [(n,t)] \Downarrow v$.
$n$ times

(3) The E.tFix rule is similarly extended to also apply if the principal argument evaluates to $\square$. Intuitively, the first rule corresponds to the fact that applying a type or a proof to an argument will be a type or proof. The second rule corresponds to the fact that if a case analysis is not erased to $\square$, this is because it returns something computational, and consequently the case analysis on the proof which was erased to $\square$ has to come from a subsingleton elimination (§3.6.3). Due to this, the rule actually covers all possible eliminations from tProp to produce a computational value. This will be explicit in the proof of correctness of erasure (§7.3). The third rule allows the unfolding of fixpoints computing a value by recursion on proofs.

## 7.2 Definition of an Erasure Function

In the remainder of the section, we assume an abstract environment $\mathcal{X}$. Parametrized by this abstract environment, a type and proof erasure function $\mathcal{E}$ can be defined from terms of PCUIC to terms of $\lambda_{\square}$.

Its implementation is based on a decision procedure `is_erasableb` which checks whether a well-typed term is *erasable*. The implementation relies on the retyping function which correctly reconstructs the type of merely well-typed terms, along with *weak-head reduction* to inspect types. We leave out the implementation of `is_erasableb` as we only need that it reflects the property `isErasable`, specifying that a term $t$ is erasable when it is typeable with some type $\Gamma$ which is either an arity (an $n$-ary dependent function type ending with a sort) – so when $t$ is a type – or typeable itself with sort `tProp` – so when $t$ is a proof.

Definition `isErasable` $\Sigma \Gamma t := \{ \Gamma \& \Sigma ; \Gamma \vdash t : T \times (\mathit{isArity} T + \Sigma ; \Gamma \vdash T : tProp) \}$.

This boolean reflection proof in particular involves proving that if `isErasable` $\Sigma \Gamma T \rightarrow \bot$ then `is_eraseableb` returns false. This requires meta-theoretic properties beyond those proved already for the system, as it focuses on proof terms specifically (those whose sort is `tProp`) and essentially quantifies over all possible types for $T$. In particular, it is necessary to show that if a term is typeable by a type which can have sort `tProp`, then for all other terms that are syntactically smaller or equal to it up to universes and are typeable, they must also have sort `tProp`. This is a generalization of principality that is particularly tricky to prove in presence of cumulative inductive types, as for example `nil@{i} N` and `nil@{j} N` are in this relation but can have unrelated sorts `nil@{i} N: list@{i} N`: `Type@{i}` and `nil@{j} N: list@{j} N`: `Type@{j}`. To solve this issue, we devise an alternative, coarser version of the cumulativity relation (in PCUIC: `CumulProp`), named sort quality equivalence, that identifies all `Type@{\_}` sorts, becoming symmetric. Cumulativity is hence a subrelation of sort quality
Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. 2014. F-ing modules. *J. Funct. Program.* 24, 5 (2014), 529–607.
https://doi.org/10.1017/S0956796814000264

Steven Schäfer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Brujin Terms and Parallel Substitutions. In *Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9236)*, Christian Urban and Xingyuan Zhang (Eds.). Springer, 359–374. https://doi.org/10.1007/978-3-319-22102-1_24

Vincent Siles and Hugo Herbelin. 2012. Pure Type System conversion is always typable. *J. Funct. Program.* 22, 2 (2012), 153–180. https://doi.org/10.1017/S0956796812000044

Gert Smolka. 2015. Confluence and Normalization in Reduction Systems. (2015). https://www.ps.uni-saarland.de/courses/sem-ws15/ars.pdf Lecture Notes.

Matthieu Sozeau. 2008. *Un environnement pour la programmation avec types dépendants*. Ph. D. Dissertation. Université Paris 11, Orsay, France.

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2019a. The MetaCoq Project. (June 2019). https://hal.inria.fr/hal-02167423 (submitted).

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2019b. Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. *Proceedings of the ACM on Programming Languages* 4, POPL (2019), 1–28. https://doi.org/10.1145/3371076

Matthieu Sozeau and Cyprien Mangin. 2019. Equations Reloaded. *PACMPL* 3, ICFP (August 2019), 86–115. https://doi.org/10.1145/3341690

Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In *Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8558)*, Gerwin Klein and Ruben Gamboa (Eds.). Springer, 499–514. https://doi.org/10.1007/978-3-319-08970-6_32

Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, and Juan Chen. 2012. Self-certification: Bootstrapping certified typecheckers in F* with Coq. In *39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'12*. Philadelphia, United States. https://hal.inria.fr/inria-00628775

Masako Takahashi. 1989. Parallel reductions in $\lambda$-calculus. *Journal of Symbolic Computation* 7, 2 (1989), 113–123.

Enrico Tassi. 2018. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi $\lambda$Prolog dialect). (Jan. 2018). https://hal.inria.fr/hal-01637063 working paper or preprint.

The Coq Development Team. 2016. The Coq Proof Assistant, version 8.5. https://coq.inria.fr/distrib/V8.5pl3/refman/

The Coq Development Team. 2022. *The Coq Proof Assistant, version 8.16*. https://doi.org/10.5281/zenodo.7313584

Amin Timany and Matthieu Sozeau. 2017. *Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)*. Research Report RR-9105. KU Leuven, Belgium ; Inria Paris. 30 pages. https://hal.inria.fr/hal-01615123

Amin Timany and Matthieu Sozeau. 2018. Cumulative Inductive Types In Coq. In *3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK (LIPIcs, Vol. 108)*, Hélène Kirchner (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 29:1–29:16. https://doi.org/10.4230/LIPIcs.FSCD.2018.29

Philip Wadler. 1985. Views. A Way for elegant definitions and efficient representations to coexist. Oxford University. http://homepages.inf.ed.ac.uk/wadler/papers/view/view.ps
<figure><img src="image_6.png" /><figcaption>Fig. 18. Erasure relation (excerpt)</figcaption></figure>

equivalence. We can then prove a theorem that essentially says that two typeable terms that are in the syntactical inequality up to universes relation have sort quality equivalent types. From this, it follows that if one has sort tProp, then the other must have it too, establishing a unique sort quality principle.

An excerpt of the definition of the erasure function is depicted in Fig. 17. It starts by looking at the result of `is_erasableb`. When the decision procedure says that the term is erasable, it simply returns `□`. When the term is not erasable, it proceeds by induction on the syntax of the term, coarsely by simply applying the erasure functions on sub-arguments and removing some type information (such as the universe instance `u` in the `tConst` case). Note the use of `EQUATIONS` to defer the definition of complex arguments such as the proof that a sub-term is well-typed using underscores.

## 7.3 Correctness of Erasure

Ideally, we would like to prove that if $\Sigma \vdash t \Downarrow v$, then we have $\mathcal{E} \Sigma \vdash \mathcal{E} [] t \Downarrow \mathcal{E} [] v$ for a suitable extension of $\mathcal{E}$ to global environments. However, this already fails on simple counter-examples: the Coq term (`fun X : Type` $\Rightarrow$ `(1, fun x : X \Rightarrow x)`) `Type` has type $\mathbb{N}^* (Type \rightarrow Type)$ and evaluates to the value `(1, fun x : Type \Rightarrow x)`. Erasing the term yields (`fun X \Rightarrow (1, fun x \Rightarrow x)`) `□`, with value `(1, fun x \Rightarrow x)`. Erasing the value however yields `(1, □)`, because `fun x : Type \Rightarrow x` is a type former of type `Type \rightarrow Type`, which is an arity and thus erased to `□`. This means intuitively that the erasure function can erase more parts of the term after it has been reduced.

Following Letouzey [2004], we get around this problem by considering a relation $\Sigma; \Gamma \vdash t \rightsquigarrow \mathcal{E} t'$, as depicted in Fig. 18, extending the erasure function, which will be closed under weak call-by-value evaluation. For normal terms of first-order inductive types like $\mathbb{N}$ or $\mathbb{N} \times \mathbb{N}$, the relation and the function agree, and we can still get the strongest result described above on such first-order types.

Essentially, the relation extends the erasure function by nondeterministic rules allowing not to erase a certain part of a term which could be erased. The only exception here is the `tCase` rule. If the `tCase` matches on a proof of a proposition which is not a `Subsingleton` (i.e., there is more
## EXAMPLE OF SUBJECT REDUCTION FAILURE IN COQ 8.14

This example showcases the incompleteness of Coq's kernel, as described in §3.4. This incompleteness manifests as a subject reduction failure: while the reduct is typeable in PCUIC, the kernel does not find this typing derivation, and wrongly rejects the reduct as ill typed.

Universe u.
(* Constraint Set < u. *)
Polymorphic Cumulative Record pack@{u} := Pack { pack_type : Type@{u} }.
(* u is covariant *)

Polymorphic Definition pack_id@{u} (p : pack@{u}) : pack@{u} :=
match p with
| Pack T ⇒ Pack T
end.

Definition packid_N (p : pack@{Set}) := pack_id@{u} p.
(* No constraints: Set ≤ u *)

Fail Definition sr_breaks := Eval compute in packid_N.

## COMPLETE SPECIFICATION OF CUMULATIVITY AND TYPING

Fig. 19 and Fig. 20 provide the complete specification of cumulativity in PCUIC while Fig. 21 provides all the typing rules of PCUIC.
than one branch in the case analysis), the whole case analysis has to be erased. This is necessary because erased discriminetes do not contain any information about which branch to use during evaluation. For subsingleton propositions, there is at most one branch where all arguments are proofs and thus can be erased, they can thus be still evaluated (by picking the one available branch, if any). We can prove global weakening, weakening and substitutivity of the erasure relation.

The erasure relation contains (the graph of) the erasure function:

Lemma erases_erase Γ t (wt : ∀ Σ, X ~ext Σ → welltyped Σ Γ t) :

$$ \forall \Sigma, X \sim_{\text{ext}} \Sigma \rightarrow \Sigma; \Gamma \vdash t \rightsquigarrow \mathcal{E} \rightarrow \Gamma \text{ wt.} $$

To state the correctness lemma, we need to extend erasure to global environments $Σ$. We write $Σ \rightsquigarrow \mathcal{E} Σ'$ for this relation. It can be defined in a straightforward way by pointwise extension of the erasure relation. Concretely, we however use an alternative definition which drops unneeded dependencies in $Σ'$ (e.g., type definitions), we discuss this in detail in § 7.4.

Contrarily to the erasure function, the erasure relation satisfies a general correctness lemma.

Lemma simple_erases correct : ∀ Σ t t' v Σ', wf Σ → welltyped Σ t →

$$ \Sigma \vdash t \Downarrow v \rightarrow \Sigma; [] \vdash t \rightsquigarrow \mathcal{E} t' \rightarrow \Sigma \rightsquigarrow \mathcal{E} \Sigma' \rightarrow $$

$$ \exists v', \Sigma; [] \vdash v \rightsquigarrow \mathcal{E} v' \wedge \| \Sigma' \vdash t' \Downarrow v' \|. $$

Note that this lemma is not proven in our development as we directly prove the more complex optimized one instead (§ 7.4).

To instantiate the erasure correctness theorem to the erasure function, we introduce the notion of first-order inductive types. An inductive i is first-order in a global context $Σ$, written firstorder_ind $Σ$ i, if all its parameters, indices, and constructor arguments have a type which is syntactically of the shape mkApps (tInd i u) args where i' is again first-order.

The crucial property is that values of first-order types are just nested constructor applications where neither proofs nor types can occur. Thus, on those terms, the erasure relation and the erasure function coincide, because they both just erase the type information to get an E.term.

Lemma firstorder_erases deterministic : ∀ v v' i u args

$$ (wf : ∀ Σ, X \sim_{\text{ext}} Σ \rightarrow \text{welltyped } Σ [] v) Σ, X \sim_{\text{ext}} Σ \rightarrow $$

$$ \text{firstorder\_ind } \Sigma i \rightarrow \Sigma; [] \vdash v : \text{mkApps} (\text{tInd } i \text{ u}) \text{ args} \rightarrow $$

$$ \Sigma \vdash v \Downarrow v \rightarrow \Sigma; [] \vdash v \rightsquigarrow \mathcal{E} v' \rightarrow $$

$$ v' = \mathcal{E} [] v \text{ wv.} $$

This brings us to the correctness of the erasure function. Because the proof of correctness is based on progress (§ 5.6), its statement has to be restricted to axiom free global environments.

Lemma erase correct firstorder : ∀ t v i u args Σ, X ~ext Σ → axiom_free Σ →

$$ \text{firstorder\_ind } \Sigma i \rightarrow $$

$$ \Sigma; [] \vdash t : \text{mkApps} (\text{tInd } i \text{ u}) \text{ args} \rightarrow $$

$$ \Sigma; [] \vdash t \rightsquigarrow^* v \rightarrow \neg \{v' \& \Sigma; [] \vdash v \rightsquigarrow v'\} \rightarrow $$

$$ \exists wv', \| \mathcal{E} \Sigma \vdash \mathcal{E} [] t \text{ wt} \Downarrow \mathcal{E} [] v wv' \|. $$

That is, if a closed term $t$ of first-order inductive type reduces to a value $v$, using the non-deterministic reduction $\rightsquigarrow^*$ defined in § 4.2, then the erasure of $t$ evaluates to the erasure of that value.

In particular, this observation entails that our type and proof erasure function supports separate compilation: Let $Σ; Γ \vdash \text{mkApps} f L : T$, where $T$ is a first-order type. Then the value of mkApps($\mathcal{E}f$)($\mathcal{E}L$) is the erasure of the value of mkApps $f L$.
Inductive "Σ ; Γ ⊢ _ ≤<sub>s</sub><sup>Rle</sup> _": term → term → Type :=

(* Ordering Rules *)

| cumul_Trans : ∀ t u v,
  is_closed_context Γ → is_open_term Γ u →
  Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Rle</sup> u →
  Σ ; Γ ⊢ u ≤<sub>s</sub><sup>Rle</sup> v →
  Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Rle</sup> v

| cumul_Sym : ∀ t u,
  Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Re</sup> u →
  Σ ; Γ ⊢ u ≤<sub>s</sub><sup>Rle</sup> t
| cumul_Refl : ∀ t,
  Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Rle</sup> t

(* Cumulativity Rules *)

| cumul_Ind : ∀ i u u' args args',
  cumul_Ind_univ Σ Re Rle i #|args| u u' →
  All2 (fun t u ⇒ Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Re</sup> u) args args' →
  Σ ; Γ ⊢ mkApps (tInd i u) args ≤<sub>s</sub><sup>Rle</sup> mkApps (tInd i u') args'
| cumulConstruct : ∀ i k u u' args args',
  cumulConstruct_univ Σ Re Rle i k #|args| u u' →
  All2 (fun t u ⇒ Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Re</sup> u) args args' →
  Σ ; Γ ⊢ mkApps (tConstruct i k u) args ≤<sub>s</sub><sup>Rle</sup> mkApps (tConstruct i k u') args'

| cumul_Sort : ∀ s s',
  Rle s s' →
  Σ ; Γ ⊢ tSort s ≤<sub>s</sub><sup>Rle</sup> tSort s'

(* Computation Rules *)

| cumul_beta : ∀ na t b a,
  Σ ; Γ ⊢ tApp (tLambda na t b) a ≤<sub>s</sub><sup>Rle</sup> b {0 := a}
| cumul_rel i body :
  option_map decl_body (nth_error Γ i) = Some (Some body) →
  Σ ; Γ ⊢ tRel i ≤<sub>s</sub><sup>Rle</sup> lift<sub>0</sub> (S i) body
| cumul_iota : ∀ ci c u args p brs br,
  nth_error brs c = Some br → #|args| = ci.(ci_npar) + context_assumptions br.(bcontext)) →
  Σ ; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ≤<sub>s</sub><sup>Rle</sup> iota_red ci p args br
| cumul_fix : ∀ mfix idx args narg fn,
  unfold_fix mfix idx = Some (narg, fn) → is
  Σ ; Γ ⊢ mkApps (tFix mfix idx) args ≤<sub>s</sub><sup>Rle</sup> mkApps fn args
| cumul_cofix_case : ∀ ip p mfix idx args narg fn brs,
  unfold_cofix mfix idx = Some (narg, fn) →
  Σ ; Γ ⊢ tCase ip p (mkApps (tCoFix mfix idx) args) brs ≤<sub>s</sub><sup>Rle</sup> tCase ip p (mkApps fn args) brs
| cumul_cofix proj : ∀ p mfix idx args narg fn,
  unfold_cofix mfix idx = Some (narg, fn) →
  Σ ; Γ ⊢ tProj p (mkApps (tCoFix mfix idx) args) ≤<sub>s</sub><sup>Rle</sup> tProj p (mkApps fn args)
| cumul_delta : ∀ c decl body (isdecl : declared
  decl.(cst_body) = Some body →
  Σ ; Γ ⊢ tConst c u ≤<sub>s</sub><sup>Rle</sup> body@[u]
| cumulproj : ∀ i pars narg args u arg,
  nth_error args (pars + narg) = Some arg →
  Σ ; Γ ⊢ tProj (i, pars, narg) (mkApps (tConstruct i 0 u) args) ≤<sub>s</sub><sup>Rle</sup> arg

<caption>Fig. 19. Cumulativity (Part I)</caption>
## 7.4 Optimizations

The erasure function defined in Letouzey’s PhD thesis [Letouzey 2004] and the definition described by Sozeau et al. [2019b] immediately inline an optimization on case analysis: if the case analysis is on a propositional inductive type, then the case analysis is immediately replaced by the first branch, where an appropriate amount of □ is inserted for all arguments of the branch. This is necessary for extraction, because □, which would witness this erasable inductive value, cannot be extracted to a constructor application as it must obey rule (1) from Page 62, thus a case analysis on it will fail or get stuck in most target languages.

Thus, the evaluation relation on $\lambda_\square$ could have been defined without rule (2) as described on Page 62. However, this direct expansion of cases considerably complicates the correctness proof of erasure, as it relies on typing invariants and inversion principles. We decide not to include it into the erasure function, and instead define it as a second pass. This second pass is done by defining a function `optimize` that is essentially the identity function but for `E.tCase` where it performs the optimization discussed above:

```
optimize Σ (E.tCase ind c brs) := let brs' := map (on_snd (optimize Σ)) brs in
    if isprop_ind Σ ind then
        match brs' with
            | [(a, b)] ⇒ substl (repeat □ #|a|) b
            | _ ⇒ E.tCase ind (optimize Σ c) brs'
    end
    else E.tCase ind (optimize Σ c) brs'
```

The function `isprop_ind` checks whether an inductive definition lives in `Prop`, in which case, when there is only one (optimized) branch, it directly returns that branch where every argument is substituted by □ (using the function `substl`).

In order to express that rule (2) is not needed anymore after this pass, we parametrize the evaluation relation over a record of flags:

```
Class WcbvFlags := {withProp_case : B; (* other flags not described in this paper *)}.
```

If `withProp_case = true`, then the rule is enabled, otherwise it is disabled. The correctness theorem for the propositional case expansion pass states that it does not change the evaluation of a term, where `eval` is the weak call-by-value evaluation predicate of $\lambda_\square$, for which we use no notation to be able to make the flags explicit.

```
Definition disableProp_cases fl := {withProp_case := false; (* ... *)}.
```

```
Lemma optimize correct Σ tv : WF Σ → closed t →
    eval fl Σ tv →
    eval (disableProp_cases fl) (optimize_env Σ) (optimize Σ t) (optimize Σ v).
```

Note that technically, we also need to extend `optimize` on environments because we need to optimize the body of definitions. The proof is direct as it just inlines the reduction rule (2).

In the same spirit, we plan on including other passes in the future, e.g., optimization passes removing parameters from inductives. If efficiency becomes a concern, we can always inline these passes again in a new erasure function and prove that it yields the same result as first running the erasure function as defined in this paper and then the propagation pass.

Another source of optimization is in the management of the global context. Indeed, the erasure process as explained here is too inefficient to be executed on realistic examples. The reason is that applying the erasure function pointwise to the global environment will perform retyping and yield numerous constants that are erased to □ but not used everywhere. This is because dependency on
(* Congruence Rules *)

| cumul_Lambda : ∀ na na' ty' t t',
  Σ ; Γ ⊢ ty ≤<sub>s</sub><sup>Re</sup> ty' → Σ ; Γ , na : ty ⊢ t ≤<sub>s</sub><sup>Rle</sup> t' →
  Σ ; Γ ⊢ tLambda na ty t ≤<sub>s</sub><sup>Rle</sup> tLambda na' ty' t'

| cumul_Prod : ∀ na na' a' b b',
  Σ ; Γ ⊢ a ≤<sub>s</sub><sup>Re</sup> a' → Σ ; Γ , na : a ⊢ b ≤<sub>s</sub><sup>Rle</sup> b' →
  Σ ; Γ ⊢ tProd na a b ≤<sub>s</sub><sup>Rle</sup> tProd na' a' b'

| cumul_LetIn : ∀ na na' t t' ty' u u',
  Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Re</sup> t' → Σ ; Γ ⊢ ty ≤<sub>s</sub><sup>Re</sup> ty' → Σ ; Γ , na := t : ty ⊢ u ≤<sub>s</sub><sup>Rle</sup> u' →
  Σ ; Γ ⊢ tLetIn na t ty u ≤<sub>s</sub><sup>Rle</sup> tLetIn na' t' ty' u'

| cumul_Case indn : ∀ p p' c c' brs brs',
  cumul predicate (fun Γ t u ⇒ Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Re</sup> u) Γ Re p p' → Σ ; Γ ⊢ c ≤<sub>s</sub><sup>Re</sup> c' →
  All2 (fun br br' ⇒ eq_context_gen eq eq (bcontext br) (bcontext br') ×
  Σ ; Γ ++ inst_caseahan context p br bbody br ≤<sub>s</sub><sup>Re</sup> bbody br') brs brs' →
  Σ ; Γ ⊢ tCase indn p c brs ≤<sub>s</sub><sup>Rle</sup> tCase indn p' c' brs'

| cumul_Proj : ∀ p c c',
  Σ ; Γ ⊢ c ≤<sub>s</sub><sup>Re</sup> c' → Σ ; Γ ⊢ tProj p c ≤<sub>s</sub><sup>Rle</sup> tProj p c'

| cumul_Fix : ∀ mfix mfix' idx,
  All2 (fun x y ⇒ Σ ; Γ ⊢ x.(dtype) ≤<sub>s</sub><sup>Re</sup> y.(dtype) ×
        Σ ; Γ ++ fix_ctx mfix x.(dbody) ≤<sub>s</sub><sup>Re</sup> y.(dbody) ×
        (x.(rarg) = y.(rarg))) mfix mfix' →
  Σ ; Γ ⊢ tFix mfix idx ≤<sub>s</sub><sup>Rle</sup> tFix mfix' idx

| cumul_CoFix : ∀ mfix mfix' idx,
  All2 (fun x y ⇒ Σ ; Γ ⊢ x.(dtype) ≤<sub>s</sub><sup>Re</sup> y.(dtype) ×
        Σ ; Γ ++ fix_ctx mfix x.(dbody) ≤<sub>s</sub><sup>Re</sup> y.(dbody) ×
        (x.(rarg) = y.(rarg))) mfix mfix' →
  Σ ; Γ ⊢ tCoFix mfix idx ≤<sub>s</sub><sup>Rle</sup> tCoFix mfix' idx.

| cumul_App : ∀ t t' u u',
  Σ ; Γ ⊢ t ≤<sub>s</sub><sup>Rle</sup> t' → Σ ; Γ ⊢ u ≤<sub>s</sub><sup>Re</sup> u' →
  Σ ; Γ ⊢ tApp t u ≤<sub>s</sub><sup>Rle</sup> tApp t' u'

| cumul_Const : ∀ c u u',
  R_universe_instance Re u u' →
  Σ ; Γ ⊢ tConst c u ≤<sub>s</sub><sup>Rle</sup> tConst c u'

<caption>Fig. 20. Cumulativity (Part II)</caption>
proofs disappears, as all proof are erased, but also because in practice a term usually only depends on a small subset of the global environment it is defined in. The full erasure theorem then reads as follows:

$$ \begin{array}{l} \textbf{Lemma} \ \text{erases\_correct} \ \Sigma \ t' \ v \ \Sigma' : \text{wf} \ \Sigma \to \text{welltyped} \ \Sigma \ t \to \\ \Sigma \vdash t \Downarrow v \to \Sigma; \ [ ] \vdash t \rightsquigarrow \varepsilon \ t' \to \text{erases\_deps} \ \Sigma \ \Sigma' \ t' \to \\ \exists v', \Sigma; \ [ ] \vdash v \rightsquigarrow \varepsilon \ v' \land \ || \ \Sigma' \vdash t' \Downarrow v' \ ||. \end{array} $$

In order not to produce a large environment polluted by irrelevant constants, we use an inductive predicate erases_deps $\Sigma \Sigma' t'$ stating that the global environment $\Sigma'$ is obtained from applying erasure recursively and selectively to $\Sigma$ by considering only the dependencies of the erased term $t'$, in a bottom-up fashion. Note that this is where we need the `abs_pop_decls` primitive that removes a declaration from the global context. This models the Recursive Extraction <term> command of Coq. The correctness proof requires fairly involved reasoning with an accumulator to account for these dependencies. It also requires particular inversion lemmas which have to be set up very carefully, accounting for the non-determinism of the erasure relation. We refer the reader to the Coq formalization for details.

# 8 RELATED WORK

Mechanized meta-theory and certified type checkers. Barras [1996] proposed the first substantial work in the area of formal correctness of proof assistants by proving subject reduction and strong normalization of a subset of Coq (namely CoC, the Calculus of Constructions) in Coq, together with the correctness of a type checker for this subset, which can then be extracted to Caml Light. Our work is a spiritual successor to this one, but is more focused on verification of an implementation than on proving strong normalization of the system. Furthermore, we deal with a subset of Coq that is almost feature complete, compared to the rather small fragment considered by Barras [1996], which for instance does not contain any inductive types. This work was the inspiration of other metatheoretical studies of extensions to CoC [Sozeau 2008] and general Pure Type Systems [Siles and Herbelin 2012] in Coq, similarly focusing on idealized, small languages.

Abel et al. [2018] present an algorithm for deciding definitional equality of an idealized dependent type theory with only one universe and natural numbers, verified in Agda, implemented using a stronger type theory with inductive-recursive types [Dybjer and Setzer 2003]. Extending that work, Adjedj et al. [2024] provide a certified type checker for a dependent type theory with $\Pi$ and $\Sigma$ types, one universe, natural numbers and an equality type, this time using Coq. While their logical relation is close to Abel et al.'s, they avoid using induction recursion. Their approach deals with $\eta$-laws by comparing $\beta$-normal $\eta$-long forms, which we do not handle. However, their algorithm is rather naive, as it systematically reduces terms to deep normal form. On the contrary, our implementation does not necessarily compute deep normal forms, which is crucial for practical performance. Moreover, we pay great attention to obtaining an executable and reasonably efficient implementation using erasure.

Strub et al. [2012] provide a methodology to build a self-certifying type checker for a large subset of $F^*$, whose metatheory is formalized in Coq. Our work is complementary in the sense that it reduces the trusted code base involved in that methodology to the specification of PCUIC, and no longer to its ML kernel implementation. Furthermore, they only tackle soundness of the type checker, while we also prove completeness.

Anand and Rahli [2014] formalize the meta-theory of the Nuprl proof assistant in Coq and prove its consistency, but do not verify a type checker for it.
<figure><img src="image_8.png" /><figcaption>Fig. 21. Typing rules</figcaption></figure>
Œuf [Mullen et al. 2018] formalizes a simply typed subset of Coq with predetermined base types and the corresponding eliminators and provides a verified compiler from this language to assembly code. As such our work is on a much larger scale as it deals with almost all of Coq.

In part inspired by META COQ, similar self-formalization projects exist for AGDA [Cockx [n. d.]] and LEAN [Carneiro 2024], but both of them are currently much less mature.

*Certified erasure and extraction.* Hupel and Nipkow [2018] implement a verified extraction from Isabelle/HOL into CakeML. The first phase of their compiler consists of a proof-producing translation implemented in Standard ML, translating terms of Isabelle/HOL into a deeply embedded term language. The second part of their compiler is a verified translation from the deeply embedded language into CakeML.

Myreen and Owens [2014] implement a certifying extraction from HOL Light code to CakeML. Their approach can translate programs in a state-and-exception monad into stateful ML code and was used by Abrahamsson et al. [2022] to extract a verified HOL Light compiler to CakeML.

Forster and Kunze [2019] report on a certifying translation from a subset of Coq to the weak call-by-value λ-calculus. Their extraction is implemented in the META COQ framework as well, but they produce correctness proofs for their extract in Coq's tactic language LTac.

Barras and Bernardo [2008] propose the Implicit Calculus of Constructions as an alternative way to specify computationally irrelevant content, whose pen-and-paper metatheory extends that of CIC [Bernardo 2015] and with a complex type inference decidability proof. It could be studied in the present framework.

Glondu [2012] verifies the syntactic proof given by Letouzey [2004] in Coq. He formalizes a correctness proof w.r.t. arbitrary small-step reduction, but works in a slightly idealized calculus with no exploitable correspondence to the actual implementation of Coq. This work does not consider a verified type checker or the verification of an executable type and proof erasure function.

*Work building on META COQ.* Annenkov et al. [2021] build on META COQ's verified erasure to extend the extraction capabilities of Coq in a verified way to more programming languages such as the web functional language Elm, the Liquidity and CameLIGO smart contract languages, or even Rust as part of the ConCert project [Annenkov et al. 2022; Nielsen et al. 2023]. Olesen [2021] goes further and extends ConCert to obtain certified extraction to the Futhark language.

The CERTI COQ project [Anand et al. 2017] is a work-in-progress verified compiler from Coq to C (as specified in COMP CERT). Before entering a complex compilation chain with various intermediate languages and optimizations, CERTI COQ uses the type and proof erasure procedure described in this paper. Consequently, an end-to-end correctness theorem for CERTI COQ would be composed of an end-to-end theorem connecting the weak call-by-value evaluation relation of λ⊥ to the operational semantics of the compiled C program and our correctness theorem for the erasure function.

Finally, Forster et al. [2024] build on the certified erasure described in this article to certify extraction from Coq to OCAML.

# 9 CONCLUSION AND FUTURE WORK

The whole development we presented includes the certified type-preserving translation from Coq's syntax to PCUIC's syntax, specification of typing, metatheory, verified checker and conversion and erasure phase. All this is done assuming the existence of a guard condition on fixpoints and cofixpoints that endows the system with strong normalization. From these specifications and implementations, a number of applications are possible. Certified translations and plugins were surveyed by Sozeau et al. [2019a], we focus here on what our contributions bring in addition.

With respect to Coq's currently implemented type theory, we depart by not considering η-equalities for functions and primitive record types in our specification of definitional equality.
We leave these extensions to future work. We also leave out the module system: thankfully, it is orthogonal to the term language and it is unclear if we should not rather explain them through an elaboration, in the style of Rossberg et al. [2014] rather than bake them in the core calculus.

In the future, we want to extend PCUIC and erasure to also handle the sort SProp [Gilbert et al. 2019], implemented since Coq 8.10. Since SProp is a proof-irrelevant analogue to Prop, adapting erasure is almost trivial: SProp can be erased like Prop and eliminations need no special care.

We also want to extend our account of erasure to other evaluation orders (most notably call-by-name evaluation to be able to target lazy languages). Currently, we support axioms which do not block call-by-value evaluation—which is rarely the case. Letouzey [2004] introduces a semantic account of erasure correctness, which would allow the treatment of axioms. We want to verify such a semantic correctness theorem.

Another exciting endeavor is to refine the specification to fit into the standard models of dependent type theory, beginning with the set theoretic model developed by Barras [1999]. A first step towards this goal will be to tackle the difficult guard and productivity conditions.

## ACKNOWLEDGMENTS

The work described in this paper received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101024493.

This work was also supported in part by a European Research Council (ERC) Consolidator Grant for the project "TypeFoundry", funded under the European Union's Horizon 2020 Framework Programme (grant agreement no. 101002277).

## REFERENCES

* Martin Abadi, Luca Cardelli, P-L Curien, and J-J Lévy. 1991. Explicit substitutions. *Journal of functional programming* 1, 4 (1991), 375–416.

* Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2004. Representing Nested Inductive Types Using W-Types. In *Automata, Languages and Programming*, Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 59–71.

* Andreas Abel, Joakim Øhman, and Andrea Vezzosi. 2018. Decidability of conversion for type theory in type theory. *PACMPL 2*, POPL (2018), 23:1–23:29. https://doi.org/10.1145/3158111

* Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: programming infinite structures by observations. In *The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013*, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 27–38. https://doi.org/10.1145/2429069.2429075

* Oskar Abrahamsson, Magnus O Myreen, Ramana Kumar, and Thomas Sewell. 2022. Candle: A Verified Implementation of HOL Light. In *13th International Conference on Interactive Theorem Proving (ITP 2022)*. Schloss Dagstuhl-Leibniz-Zentrum für Informatik.

* Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. 2024. Martin-Löf à la Coq. In *Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs* (London, UK) (CPP 2024). Association for Computing Machinery, New York, NY, USA, 230–245. https://doi.org/10.1145/3636501.3636951

* Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In *CoqPL. Paris, France. http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq*

* Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. In *ITP 2018 (Lecture Notes in Computer Science, Vol. 10895)*, Jeremy Avigad and Assia Mahboubi (Eds.). Springer, 20–39. https://doi.org/10.1007/978-3-319-94821-8_2

* Abhishek Anand and Vincent Rahli. 2014. Towards a Formally Verified Proof Assistant. In *Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8558)*, Gerwin Klein and Ruben Gamboa (Eds.). Springer, 27–44. https://doi.org/10.1007/978-3-319-08970-6_3

* Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2021. Extracting smart contracts tested and verified in Coq. In *Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs*. 105–121.
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2022. Extracting functional programs from Coq, in Coq. *Journal of Functional Programming* 32 (2022), e11.

ANSSI. 2021. *Requirements on the Use of Coq in the Context of Common Criteria Evaluations*. v1.1. French National Cybersecurity Agency. https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf.

Bruno Barras. 1996. *Coq en Coq*. Rapport de Recherche 3026. INRIA.

Bruno Barras. 1999. *Auto-validation d'un système de preuves avec familles inductives*. Thèse de Doctorat. Université Paris 7. http://pauillac.inria.fr/~barras/publi/these_barras.ps.gz

Bruno Barras. 2012. *Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families*. Habilitation Thesis.

Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In *FoSSaCS (Lecture Notes in Computer Science, Vol. 4962)*, Roberto M. Amadio (Ed.). Springer, 365–379.

Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, and Robert E. Tarjan. 2015. A New Approach to Incremental Cycle Detection and Related Problems. *ACM Trans. Algorithms* 12, 2, Article 14 (Dec. 2015), 22 pages. https://doi.org/10.1145/2756553

Bruno Bernardo. 2015. *Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable. (An implicit Calculus of Constructions with dependent sums and decidable type inference)*. Ph. D. Dissertation. École Polytechnique, Palaiseau, France. https://tel.archives-ouvertes.fr/tel-01197380

Marc Bezem and Thierry Coquand. 2022. Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. *Theoretical Computer Science* 913 (2022), 1–7. https://doi.org/10.1016/j.tcs.2022.01.017

Mario Carneiro. 2024. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. (March 2024). https://doi.org/10.48550/ARXIV.2403.14064 arXiv:2403.14064 [cs.PL]

Jesper Cockx. [n. d.]. Agda Core: The Dream and the Reality. ([n. d.]). https://jesper.cx/files/IFIP28-2024.html

T. Coquand. 1989. *Metamathematical investigations of a calculus of constructions*. Ph. D. Dissertation. https://hal.inria.fr/inria-00075471

Thierry Coquand and Gérard Huet. 1988. The Calculus of Constructions. *Information and Computation* 76, 2–3 (February/March 1988), 95–120.

Thierry Coquand and Christine Paulin. 1990. Inductively defined types. In *COLOG-88*, Per Martin-Löf and Grigori Mints (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 50–66.

Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. *Comput. Surveys* 54, 5, Article 98 (2021), 38 pages. https://doi.org/10.1145/3450952

Peter Dybjer and Anton Setzer. 2003. Induction-recursion and initial algebras. *Annals of Pure and Applied Logic* 124, 1-3 (2003), 1–47. https://doi.org/10.1016/S0168-0072(02)00096-9

Yannick Forster and Fabian Kunze. 2019. A certifying extraction with time bounds from Coq to call-by-value λ-calculus. In *Tenth International Conference on Interactive Theorem Proving*. Springer.

Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. 2024. Verified Extraction from Coq to OCaml. *Proc. ACM Program. Lang.* 8, PLDI, Article 149 (June 2024), 24 pages. https://doi.org/10.1145/3656379

Herman Geuvers. 2007. Inconsistency of classical logic in type theory. *Unpublished notes* (2007). http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional Proof-Irrelevance without K. *Proceedings of the ACM on Programming Languages* (Jan. 2019), 1–28. https://doi.org/10.1145/3290316.1145/3290316

Gaëtan Gilbert, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. 2023. From Lost to the River: Embracing Sort Proliferation. In *29th International Conference on Types for Proofs and Programs*.

Carlos Eduardo Giménez. 1996. *Un calcul de constructions infinies et son application à la vérification de systèmes communicants*. Ph. D. Dissertation. Ecole Normale Supérieure de Lyon. ftp://ftp.inria.fr/INRIA/LogiCal/Eduardo.Gimenez/thesis.ps.gz

J.-Y. Girard. 1972. *Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur*. Ph. D. Dissertation. Université Paris 7.

Stéphane Glondu. 2012. *Vers une certification de l'extraction de Coq*. Ph. D. Dissertation. Université Paris Diderot.

Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. 2019. Implementing a Modal Dependent Type Theory. *Proc. ACM Program. Lang.* 3, ICFP, Article 107 (July 2019), 29 pages. https://doi.org/10.1145/3341711

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. 2019. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In *ITP 2019 - 10th Conference on Interactive Theorem Proving*. Portland, United States. https://hal.inria.fr/hal-02167236

Robert Harper and Frank Pfenning. 2005. On equivalence and canonical forms in the LF type theory. *ACM Trans. Comput. Logic* 6, 1 (jan 2005), 61–101. https://doi.org/10.1145/1042038.1042041

Robert Harper and Robert Pollack. 1991. Type Checking with Universes. *Theor. Comput. Sci.* 89, 1 (1991), 107–136.
Gérard Huet. 1988. Extending the Calculus of Constructions with Type:Type. (1988). http://pauillac.inria.fr/~huet/PUBLIC/tytyp.pdf

Lars Hupel and Tobias Nipkow. 2018. A verified compiler from Isabelle/HOL to CakeML. In *European Symposium on Programming*. Springer, 999–1026.

Antonius J. C. Hurkens. 1995. A simplification of Girard's paradox. In *Typed Lambda Calculi and Applications*, Mariangiola Dezani-Ciancaglini and Gordon Plotkin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 266–278.

Gyesik Lee and Benjamin Werner. 2011. Proof-irrelevant model of CC with predicative induction and judgmental equality. *Logical Methods in Computer Science* 7, 4 (2011).

Meven Lennon-Bertrand. 2021. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In *12th International Conference on Interactive Theorem Proving (ITP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193)*, Liron Cohen and Cezary Kaliszyk (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ITP.2021.24

Meven Lennon-Bertrand. 2022. *Bidirectional Typing for the Calculus of Inductive Constructions*. PhD Thesis.

Yann Leray. 2022. *Formalisation et implémentation des propositions strictes dans MetaCoq*. Technical Report. Inria Rennes - Bretagne Atlantique ; LS2N-Nantes Université. 17 pages. https://inria.hal.science/hal-04433492

Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In *33rd symposium Principles of Programming Languages*. ACM Press, 42–54. http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf

Pierre Letouzey. 2002. A New Extraction for Coq. In *TYPES'02 (Lecture Notes in Computer Science, Vol. 2646)*, Herman Geuvers and Freek Wiedijk (Eds.). Springer, 200–219.

Pierre Letouzey. 2004. *Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq*. Thèse de Doctorat. Université Paris-Sud. http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.pdf

Per Martin-Löf. 1984. *Intuitionistic type theory*. Studies in Proof Theory, Vol. 1. Bibliopolis. iv+91 pages.

Per Martin-Löf. 1998. An intuitionistic theory of types. In *Twenty-five years of constructive type theory (Venice, 1995)*, Giovanni Sambin and Jan M. Smith (Eds.). Oxford Logic Guides, Vol. 36. Oxford University Press, 127–172.

Conor McBride. 2009. Grins from my Ripley Cupboard. (2009).

Conor McBride. 2018. Basics of Bidirectionalism. (Aug. 2018). https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/ Blog post.

Conor McBride and James McKinna. 2004. The view from the left. *J. Funct. Program*. 14, 1 (2004), 69–111.

Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman. 2018. (Euf: minimizing the Coq extraction TCB. In *Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018*, June Andronick and Amy P. Felty (Eds.). ACM, 172–185. https://doi.org/10.1145/3167089

Magnus O Myreen and Scott Owens. 2014. Proof-producing translation of higher-order logic into pure and stateful ML. *Journal of Functional Programming* 24, 2-3 (2014), 284–315.

Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. 2023. Formalising Decentralised Exchanges in Coq. In *Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs*. 290–302.

Fredrik Nordvall Forsberg. 2013. *Inductive-inductive definitions*. Ph. D. Dissertation. Swansea University.

Ulf Norell. 2007. *Towards a practical programming language based on dependent type theory*. Ph. D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden. http://www.cs.chalmers.se/~ulfn/papers/thesis.html

Kristian Knudsen Olesen. 2021. Extracting certified Futhark code from Coq. (2021).

Lawrence C Paulson. 1986. Constructing Recursion operators in Intuitionistic Type Theory. *Journal of Symbolic Computation* 2, 4 (1986), 325–355. https://www.sciencedirect.com/science/article/pii/S0747717186800025/pdf?md5=4df038c66455b64726734b09ad0ea894&isDTMRedir=Y&pid=1-s2.0-S0747717186800025-main.pdf&valck=1

Pierre-Marie Pédrot and Nicolas Tabareau. 2017. An effectful way to eliminate addiction to dependence. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*. IEEE Computer Society, 1–12. https://doi.org/10.1109/LICS.2017.8005113

Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. *ACM Transactions on Programming Languages and Systems* 22, 1 (Jan. 2000), 1–44. http://doi.acm.org/10.1145/345099.345100

Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. 2014. F-ing modules. *J. Funct. Program*. 24, 5 (2014), 529–607. https://doi.org/10.1017/S0956796814000264

Steven Schäfer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Brujin Terms and Parallel Substitutions. In *Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9236)*, Christian Urban and Xingyuan Zhang (Eds.). Springer, 359–374. https://doi.org/10.1007/978-3-319-22102-1_24
Vincent Siles and Hugo Herbelin. 2012. Pure Type System conversion is always typable. *J. Funct. Program.* 22, 2 (2012), 153–180. https://doi.org/10.1017/S0956796812000044

Gert Smolka. 2015. Confluence and Normalization in Reduction Systems. (2015). https://www.ps.uni-saarland.de/courses/sem-ws15/ars.pdf Lecture Notes.

Elie Soubiran. 2010. *Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq*. Theses. Ecole Polytechnique X. https://theses.hal.science/tel-00679201

Matthieu Sozeau. 2008. *Un environnement pour la programmation avec types dépendants*. Ph. D. Dissertation. Université Paris 11, Orsay, France.

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2019a. The MetaCoq Project. (June 2019). https://hal.inria.fr/hal-02167423 (submitted).

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2019b. Coq Coq correct! Verification of type checking and erasure for Coq, in *Coq. Proceedings of the ACM on Programming Languages* 4, POPL (2019), 1–28. https://doi.org/10.1145/3371076

Matthieu Sozeau and Cyprien Mangin. 2019. Equations Reloaded. *PACMPL* 3, ICFP (August 2019), 86–115. https://doi.org/10.1145/3341690

Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In *Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8558)*, Gerwin Klein and Ruben Gamboa (Eds.). Springer, 499–514. https://doi.org/10.1007/978-3-319-08970-6_32

Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, and Juan Chen. 2012. Self-certification: Bootstrapping certified typecheckers in F* with Coq. In *39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'12*. Philadelphia, United States. https://hal.inria.fr/inria-00628775

Masako Takahashi. 1989. Parallel reductions in $\lambda$-calculus. *Journal of Symbolic Computation* 7, 2 (1989), 113–123.

Enrico Tassi. 2018. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi $\lambda$Prolog dialect). (Jan. 2018). https://hal.inria.fr/hal-01637063 working paper or preprint.

Enrico Tassi. 2019. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In *10th International Conference on Interactive Theorem Proving, ITP 2019 (LIPIcs, Vol. 141)*, John Harrison, John O'Leary, and Andrew Tolmach (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 29:1–29:18. https://doi.org/10.4230/LIPICS.ITP.2019.29

The Coq Development Team. 2016. The Coq Proof Assistant, version 8.5. https://coq.inria.fr/distrib/V8.5pl3/refman/

The Coq Development Team. 2022. *The Coq Proof Assistant, version 8.16*. https://doi.org/10.5281/zenodo.7313584

Amin Timany and Matthieu Sozeau. 2017. *Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)*. Research Report RR-9105. KU Leuven, Belgium ; Inria Paris. 30 pages. https://hal.inria.fr/hal-01615123

Amin Timany and Matthieu Sozeau. 2018. Cumulative Inductive Types In Coq. In *3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK (LIPIcs, Vol. 108)*, Hélène Kirchner (Ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 29:1–29:16. https://doi.org/10.4230/LIPICS.FSCD.2018.29

Philip Wadler. 1985. Views. A Way for elegant definitions and efficient representations to coexist. Oxford University. http://homepages.inf.ed.ac.uk/wadler/papers/view/view.ps
## EXAMPLE OF SUBJECT REDUCTION FAILURE IN COQ 8.14

This example showcases the incompleteness of Coq's kernel, as described in §4.4. This incompleteness manifests as a subject reduction failure: while the reduct is typeable in PCUIC, the kernel does not find this typing derivation, and wrongly rejects the reduct as ill typed.

Universe u.
(* Constraint Set < u. *)
Polymorphic Cumulative Record pack@{u} := Pack { pack_type : Type@{u} }.
(* u is covariant *)

Polymorphic Definition pack_id@{u} (p : pack@{u}) : pack@{u} :=
match p with
| Pack T ⇒ Pack T
end.
Definition packid_N (p : pack@{Set}) := pack_id@{u} p.
(* No constraints: Set ≤ u *)

Fail Definition sr_breaks := Eval compute in packid_N.

## COMPLETE SPECIFICATION OF CUMULATIVITY AND TYPING

Fig. 19 and Fig. 20 provide the complete specification of cumulativity in PCUIC while Fig. 21 provides all the typing rules of PCUIC.
Inductive "Σ ; Γ ⊢ _ ≤_s Rle _": term → term → Type :=

(* Ordering Rules *)

| cumul_Trans : ∀ t u v,
  is_closed_context Γ → is_open_term Γ u →
  Σ ; Γ ⊢ t ≤_s Rle u →
  Σ ; Γ ⊢ u ≤_s Rle v →
  Σ ; Γ ⊢ t ≤_s Rle v

| cumul_Sym : ∀ t u,
  Σ ; Γ ⊢ t ≤_s Re u →
  Σ ; Γ ⊢ u ≤_s Rle t
| cumul_Refl : ∀ t,
  Σ ; Γ ⊢ t ≤_s Rle t

(* Cumulativity Rules *)

| cumul_Ind : ∀ i u u' args args',
  cumul_Ind_univ Σ Re Rle i #|args| u u' →
  All2 (fun t u ⇒ Σ ; Γ ⊢ t ≤_s Re u) args args' →
  Σ ; Γ ⊢ mkApps (tInd i u) args ≤_s Rle mkApps (tInd i u') args'
| cumul_Construct : ∀ i k u u' args args',
  cumul_Construct_univ Σ Re Rle i k #|args| u u' →
  All2 (fun t u ⇒ Σ ; Γ ⊢ t ≤_s Re u) args args' →
  Σ ; Γ ⊢ mkApps (tConstruct i k u) args ≤_s Rle mkApps (tConstruct i k u') args'

| cumul_Sort : ∀ s s',
  Rle s s' →
  Σ ; Γ ⊢ tSort s ≤_s Rle tSort s'

(* Computation Rules *)

| cumul_beta : ∀ na t b a,
  Σ ; Γ ⊢ tApp (tLambda na t b) a ≤_s Rle b {0 := a} | cumul_zeta : ∀ na b t b',
  Σ ; Γ ⊢ tLetIn na b t b' ≤_s Rle b' {0 := b}
| cumul_rel i body :
  option_map decl_body (nth_error Γ i) = Some (Some body) →
  Σ ; Γ ⊢ tRel i ≤_s Rle lift0 (S i) body
| cumul_iota : ∀ ci c u args p brs br,
  nth_error brs c = Some br → #|args| = ci.(ci_npar) + context_assumptions br.(bcontext)) →
  Σ ; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ≤_s Rle iota_red ci p args br
| cumul_fix : ∀ mfix idx args narg fn,
  unfold_fix mfix idx = Some (narg, fn) → is
  Σ ; Γ ⊢ mkApps (tFix mfix idx) args ≤_s Rle mkApps fn args
| cumul_cofix_case : ∀ ip p mfix idx args narg fn brs,
  unfold_cofix mfix idx = Some (narg, fn) →
  Σ ; Γ ⊢ tCase ip p (mkApps (tCoFix mfix idx) args) brs ≤_s Rle tCase ip p (mkApps fn args) brs
| cumul_cofix proj : ∀ p mfix idx args narg fn,
  unfold_cofix mfix idx = Some (narg, fn) →
  Σ ; Γ ⊢ tProj p (mkApps (tCoFix mfix idx) args) ≤_s Rle tProj p (mkApps fn args)
| cumul_delta : ∀ c decl body (isdecl : declared
  decl.(cst_body) = Some body →
  Σ ; Γ ⊢ tConst c u ≤_s Rle body@[u]
| cumul proj : ∀ i pars narg args u arg,
  nth_error args (pars + narg) = Some arg →
  Σ ; Γ ⊢ tProj (i, pars, narg) (mkApps (tConstruct i 0 u) args) ≤_s Rle arg

<caption>Fig. 19. Cumulativity (Part I)</caption>
(* Congruence Rules *)

| cumul_Lambda : ∀ na na' ty t' t',
  Σ ; Γ ⊢ ty ≲<sub>s</sub><sup>Re</sup> ty' → Σ ; Γ , na : ty ⊢ t ≲<sub>s</sub><sup>Rle</sup> t' →
  Σ ; Γ ⊢ tLambda na ty t ≲<sub>s</sub><sup>Rle</sup> tLambda na' ty' t'

| cumul_Prod : ∀ na na' a' b b',
  Σ ; Γ ⊢ a ≲<sub>s</sub><sup>Re</sup> a' → Σ ; Γ , na : a ⊢ b ≲<sub>s</sub><sup>Rle</sup> b' →
  Σ ; Γ ⊢ tProd na a b ≲<sub>s</sub><sup>Rle</sup> tProd na' a' b'

| cumul_LetIn : ∀ na na' t t' ty ty' u u',
  Σ ; Γ ⊢ t ≲<sub>s</sub><sup>Re</sup> t' → Σ ; Γ ⊢ ty ≲<sub>s</sub><sup>Re</sup> ty' → Σ ; Γ , na := t : ty ⊢ u ≲<sub>s</sub><sup>Rle</sup> u' →
  Σ ; Γ ⊢ tLetIn na t ty u ≲<sub>s</sub><sup>Rle</sup> tLetIn na' t' ty' u'

| cumul_Case indn : ∀ p p' c c' brs brs',
  cumul predicate (fun Γ t u ⇒ Σ ; Γ ⊢ t ≲<sub>s</sub><sup>Re</sup> u) Γ Re p p' → Σ ; Γ ⊢ c ≲<sub>s</sub><sup>Re</sup> c' →
  All2 (fun br br' ⇒ eq_context_gen eq eq (bcontext br) (bcontext br') ×
        Σ ; Γ ++ inst_caseahan context p br + bbody br ≲<sub>s</sub><sup>Re</sup> bbody br') brs brs' →
  Σ ; Γ ⊢ tCase indn p c brs ≲<sub>s</sub><sup>Rle</sup> tCase indn p' c' brs'

| cumul_Proj : ∀ p c c',
  Σ ; Γ ⊢ c ≲<sub>s</sub><sup>Re</sup> c' → Σ ; Γ ⊢ tProj p c ≲<sub>s</sub><sup>Rle</sup> tProj p c'

| cumul_Fix : ∀ mfix mfix' idx,
  All2 (fun x y ⇒ Σ ; Γ ⊢ x.(dtype) ≲<sub>s</sub><sup>Re</sup> y.(dtype) ×
        Σ ; Γ ++ fix_ctx mfix ⊢ x.(dbody) ≲<sub>s</sub><sup>Re</sup> y.(dbody) ×
        (x.(rarg) = y.(rarg))) mfix mfix' →
  Σ ; Γ ⊢ tFix mfix idx ≲<sub>s</sub><sup>Rle</sup> tFix mfix' idx

| cumul_CoFix : ∀ mfix mfix' idx,
  All2 (fun x y ⇒ Σ ; Γ ⊢ x.(dtype) ≲<sub>s</sub><sup>Re</sup> y.(dtype) ×
        Σ ; Γ ++ fix_ctx mfix ⊢ x.(dbody) ≲<sub>s</sub><sup>Re</sup> y.(dbody) ×
        (x.(rarg) = y.(rarg))) mfix mfix' →
  Σ ; Γ ⊢ tCoFix mfix idx ≲<sub>s</sub><sup>Rle</sup> tCoFix mfix' idx.

| cumul_App : ∀ t t' u u',
  Σ ; Γ ⊢ t ≲<sub>s</sub><sup>Rle</sup> t' → Σ ; Γ ⊢ u ≲<sub>s</sub><sup>Re</sup> u' →
  Σ ; Γ ⊢ tApp t u ≲<sub>s</sub><sup>Rle</sup> tApp t' u'

| cumul_Const : ∀ c u u',
  R_universe_instance Re u u' →
  Σ ; Γ ⊢ tConst c u ≲<sub>s</sub><sup>Rle</sup> tConst c u'

<caption>Fig. 20. Cumulativity (Part II)</caption>