La 2024 Coq

Arthur Adjedj
email: arthur.adjedj@gmail.com

Meven Lennon-Bertrand

Kenji Maillard
email: kenji.maillard@inria.fr

Pierre-Marie Pédrot
email: pierre-marie.pedrot@inria.fr

Loïc Pujet

Martin-Löf

Hal-04214008v2 Martin-Löf

Keywords: CCS Concepts:, Theory of computation → Type theory, Type structures, • Software and its engineering → Data types and structures Dependent type systems, Bidirectional typing, Logical relations

Introduction

Self-certification of proof assistants is a long-standing and very enticing goal. Since proof assistant kernels are by construction relatively small, have a precise specification, and are part of the trusted computing base of any software certified using them, they offer a natural target for certification. Yet, full certification of a realistic kernel based on dependent type theory remains a challenging goal.

The reasons are twofold. First, dependent type theory is very expressive, allowing one to formulate mathematical statements with small amounts of encoding. Consequently, even a minimalistic kernel has to be rather complex. Second, and more critically, dependent type theory intertwines types and computations, forcing us to prove results about computations in order to fully certify a type checker. The usual approach is to establish a normalization result to derive the decidability of the conversion relation, which is used to compare types during type checking. Normalization, however, is generally difficult to prove, as it typically implies soundness of the type system seen as a logic. Accordingly, an important part of the work needed to fully certify a type checker is spent on establishing metatheoretic properties, which are necessary to ensure termination of the type checker but have little to do with its concrete implementation.

Acknowledging this tension leads to radically different approaches. On the one hand, one can simply postulate normalization, to concentrate on the difficulties faced when certifying a realistic type-checker. The most ambitious project to date following this approach is MetaCoq [START_REF] Sozeau | The MetaCoq Project[END_REF][START_REF] Sozeau | Correct and Complete Type Checking and Certified Erasure for Coq[END_REF], which formalizes a nearly complete fragment of Coq's type system and provides a certified type checker aimed at execution in a realistic context, after extraction. On the other hand, one can concentrate on normalization and decidability of conversion, the most difficult theoretical problems. The most advanced formalizations on that end are Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF] and Wieczorek and Biernacki [START_REF] Wieczorek | A coq formalization of normalization by evaluation for martin-löf type theory[END_REF]. The first one, in Agda, shows decidability of conversion, but does not provide an executable conversion checker. The second, in Coq, certifies a conversion checker designed for execution after extraction, but supports a type theory that is less powerful than the former, e.g. it does not feature large elimination of inductive types. Neither formalization provide a type checker.

Contributions. We aim to bring together and improve on this state of the art on proof assistant certification. More precisely, we:

• formalize a full-fledged version of Martin-Löf type theory (MLTT) that features dependent function (Π) and pair (Σ) types with 𝜂-laws, natural numbers 𝐍 and intensional equality 𝐈𝐝 types with large elimination, and one predicative universe; • show decidability of conversion and type checking, refining the logical relation of Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF]; • provide a naïve but certified and executable implementation of the type checker; • define our logical relation in MLTT with indexed inductive types (i.e. without either induction-recursion or impredicativity), providing a narrow upper bound on the logical strength needed to show normalization; • design our development in a modular way that accommodates extensions of the type theory. The ongoing development is freely accessible on Github [START_REF] Adjedj | Logical Relation for MLTT in Coq[END_REF], and the version referenced in this article is available on Zenodo [11]. Our formalization spans around 30k lines of code, and we refer to it in the text with links in blue. To help navigate it, a (file-level) dependency graph is given in Fig. 2.

Plan of the paper. Section 2 sets the context of this work, giving a high-level tour of the theory and the metatheoretical properties we formalize. We provide a detailed comparison with prior work in Section 3. Section 4 presents the logical relation technique and Section 5 details some challenges of our formalization to encode logical relations for MLTT and establishes a bound on the complexity of the normalization proof. Section 6 explains the algorithmic aspects of typing and conversion, culminating with decidability. Section 7 details engineering aspects of the formalization, while Section 8 explore the future opportunities created by this work. Contribution statement. A. Adjedj started the first prototype of this project during an internship advised by L. Pujet and Nicolas Tabareau, focusing on defining a logical relation by small IR. M. Lennon-Bertrand laid down the main structure of the formalisation, particularly its bidirectional aspects and the certified checker. K. Maillard, P.-M. Pédrot and L. Pujet contributed to the logical relation proofs.

MLTT and its Metatheory

We take Martin-Löf type theory [START_REF] Martin | Number 1 in Studies in Proof Theory[END_REF]-or rather the Martin-Löf logical framework, which encompasses a whole family of type systems-as an ideal version of the actual type system implemented by proof assistants based on dependent types, such as Agda, Coq or Lean. MLTT is presented in terms of judgements for well-formed contexts and types, written ⊢ Γ and Γ ⊢ 𝑇 , well-typed terms Γ ⊢ 𝑡 : 𝑇 , but also conversion judgements for types Γ ⊢ 𝑇 ≅ 𝑇 ′ , and terms Γ ⊢ 𝑡 ≅ 𝑡 ′ : 𝑇 which assert that the two sides are definitionally equal, and can be used interchangeably. Importantly, conversion is typed: it only makes sense to compare terms at a given type. Judgements are derived according to typing rules that we leave out to the formalization, see Declar-ativeTyping. In our development, we implement in this logical framework the following type formers:

• the dependent function types Π 𝑥: 𝐴.𝐵 (with a definitional 𝜂-rule); • the dependent pair types Σ 𝑥: 𝐴.𝐵 (eliminated via projections, with a definitional 𝜂-rule); • a universe of small types, noted Type;

• the inductive datatype of natural numbers 𝐍, with an induction principle that supports large elimination; • the Martin-Löf identity type 𝐈𝐝 𝐴 𝑥 𝑦, and the J eliminator that supports large elimination; • the empty type 𝟎 and its eliminator. Our goal is to give a formal proof of the metatheoretical properties that make Martin-Löf type theory a well-behaved foundation for proof assistants: consistency, canonicity and decidability. Consistency states that there is no inhabitant of the empty type in the empty context, i.e. that the logic is sound. Canonicity asserts that every inhabitant of 𝐍 in an empty context is convertible to a numeral, i.e. a succession of successors applied to 0. Finally, typing and conversion should be decidable, more precisely it should be decidable whether any typing or conversion judgement is derivable.

Establishing these properties, however, is challenging. In particular, large elimination, i.e. the possibility to construct a type by induction, deeply intertwines the term and type levels. This fundamental feature of inductive types in MLTT sets this type theory apart, giving it its expressivity but complexifying its metatheory. In Section 4, we present a logical relation based on reduction to tackle this problem.

Indeed, conversion can be presented as the symmetric, reflexive, transitive, congruence closure of a reduction relation, modulo additional rules such as 𝜂-laws. Our formalization uses weak-head reduction , a deterministic1 reduction strategy that only reduces redexes at the top of a term but not in subterms. The normal forms for this reduction strategy, called weak-head normal forms, can be characterized inductively as either a canonical introduction form for a type (e.g. 𝜆𝑥: 𝐴.𝑡 for Π, 0 or 𝑆 𝑛 for 𝐍), or a neutral term, that is a stack of elimination forms (e.g. application 𝑛 𝑡 for Π, or induction ind 𝐍 (𝑛; 𝑃 ; 𝑡) for 𝐍 for neutrals 𝑛) ultimately stuck on a variable. The logical relation will be used to prove two key properties: first, weak-head normalization, which asserts that all well-typed terms reduce to a weak-head normal form; second, subject reduction, which stipulates that types are invariant by reduction (if 𝑥 : 𝐴 and 𝑥 𝑦 then 𝑦 : 𝐴).

From these, consistency of the system can be directly derived. The algorithmic presentations of typing and conversion from Section 6 also heavily rely on these properties to prove canonicity and decidability.

Related Work

In response to the challenge of establishing metatheoretical properties for MLTT, the literature can be divided into two trends. On the one hand, there is a natural incentive to leverage the power of proof assistants to keep track of much of the nitty-gritty details and even automate them away. On the other hand, there is a growing interest in sophisticated frameworks that abstract away from these details in order to give synthetic, although mathematically challenging proofs.

Towards certified proof-assistants. The MetaCoq project [START_REF] Sozeau | The MetaCoq Project[END_REF][START_REF] Sozeau | Correct and Complete Type Checking and Certified Erasure for Coq[END_REF] provides a certified type checker for a type system very close to the one underlying Coq, assuming normalization of the formalized type theory. It is based on an untyped presentation of conversion, which facilitates parts of the metatheoretical work, but makes it much more difficult to handle extensionality rules, e.g. the 𝜂 rules for functions and primitive records, which are currently not supported.

Much earlier, Barras and Werner [START_REF] Barras | Coq in coq[END_REF] provide a fully certified proof assistant for the Calculus of Constructions, even featuring a small REPL on top of the certified kernel.

Outside dependently typed proof assistants, very advanced certification efforts have been achieved for the HOL family with the Candle project [START_REF] Oskar Abrahamsson | Candle: A Verified Implementation of HOL Light[END_REF].

Formalized metatheory of dependent type systems.

In the late '90s, Barras and Werner [START_REF] Barras | Coq in coq[END_REF] fully certified a proof assistant for the Calculus of Constructions (CC). They proved the normalization and decidability of type checking for CC in Coq using reducibility candidates [START_REF] Girard | Proofs and Types[END_REF]. Their type theory supports an impredicative universe, but no inductive types. This allows Barras et al. to erase dependency from the types in their normalization proof, and thereby solve the interdependency puzzle without too much difficulty. In his PhD thesis, Barras [START_REF] Barras | Auto-validation d'un système de preuves avec familles inductives[END_REF] adds inductive types and a hierarchy of predicative universes, and shows decidability of type checking assuming normalization, but to the best of our knowledge this part of his work was never formalized. In later unpublished work, Barras [START_REF] Barras | Semantical investigations in intuitionistic set theory and type theories with inductive families[END_REF] shows normalization of CC extended with natural numbers and large elimination, as well as consistency of the Extended Calculus of Constructions, adding a countable hierarchy of predicative universes to CC, together with W-types. His formal proof relies on realizability models built on top of an embedding of IZF in Coq, and has been applied to establish the metatheory of CoqMT [START_REF] Wang | Semantics of intensional type theory extended with decidable equational theories[END_REF].

More recently, Wieczorek and Biernacki [START_REF] Wieczorek | A coq formalization of normalization by evaluation for martin-löf type theory[END_REF] formally prove the correctness of a normalization by evaluation (NbE) algorithm in Coq, following pen-and-paper proofs by Abel and co-authors [START_REF] Abel | Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements[END_REF][START_REF] Abel | Normalization by evaluation for Martin-Löf type theory with one universe[END_REF][START_REF] Abel | A modular type-checking algorithm for type theory with singleton types and proof irrelevance[END_REF][START_REF] Abel | Towards normalization by evaluation for the 𝛽𝜂-calculus of constructions[END_REF]. Compared to the work of Barras et al., their development covers some primitive datatypes, namely natural numbers, and the empty and unit types. However, it does not tackle large elimination, the main difficulty presented by inductive types in this setting. For their normalization proof, Wieczorek et al. model types as proof-irrelevant partial equivalence relations (PERs). Since the pen-and-paper definition uses induction-recursion, which is not available in Coq, the authors replace it with impredicative encodings, creating an important gap in logical power between the object theory and their metatheory. They provide a conversion checker designed to be run after extraction (which erases the complex termination argument), but not a type checker, which they leave as future work.

In parallel, Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF] attack a similar problem in Agda. Rather than proving correctness of normalization by evaluation in a semantic domain, they rely on a reduction-based approach, although they nevertheless use a typed notion of conversion which supports 𝜂 laws. Moreover, they give a proper treatment of large elimination for the inductive type of natural numbers and its induction principle. The definition of their logical relation is also based on the work of Abel [START_REF] Abel | Towards normalization by evaluation for the 𝛽𝜂-calculus of constructions[END_REF] etc., but it relies on induction-recursion instead of impredicativity. Similarly to Wieczorek et al., they stop after decidability of conversion, and their decider is moreover not geared toward execution, neither in Agda nor after extraction.

This work has since been extended to justify multiple additions to MLTT [START_REF] Gilbert | Definitional proof-irrelevance without k. Proceedings of the ACM on Programming Languages[END_REF][START_REF] Pujet | Observational equality: now for good[END_REF][START_REF] Pujet | Impredicative observational equality[END_REF][START_REF] Abel | A graded modal dependent type theory with a universe and erasure, formalized[END_REF]. Of particular interest is Pujet and Tabareau [START_REF] Pujet | Impredicative observational equality[END_REF], which lowers the logical power needed for the proof by removing induction-recursion with an encoding similar to ours. Yet, this proof still relies on Agda's first-class universe levels, whose metatheory has been relatively unexplored, but for Kovács [START_REF] Kovács | Generalized universe hierarchies and firstclass universe levels[END_REF].

In his lecture at the Collège de France, Leroy [START_REF] Leroy | Coq en coq[END_REF] reviews these recent approaches to the certification of proof assistants, in particular for Coq and Agda. He highlights the difficulty for a proof assistant to certify its own correctness, e.g. Gödel's incompleteness theorems inform us that a proof of consistency requires a logic that is strictly more powerful than the logic of the proof assistant. Nevertheless, Leroy conjectures that only a marginal increase in power is required to show the consistency of Coq, for instance a mere difference in the number of available universes between the object theory and the metatheory. We approach a similar result for our fragment of MLTT, by avoiding the use of impredicativity or induction-recursion. More broadly, the two POPLMark challenges [START_REF] Aydemir | Mechanized metatheory for the masses: the poplmark challenge[END_REF][START_REF] Abel | Poplmark reloaded: mechanizing proofs by logical relations[END_REF], which aim at enhancing the general work on formalized metatheory of type systems, are also relevant to this work. Indeed, the AutoSubst plugin for Coq [START_REF] Stark | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions[END_REF], which has been developed in this setting, has been directly useful to us, and further developments on modular mechanization of metatheory [START_REF] Jin | Extensible metatheory mechanization via family polymorphism[END_REF][START_REF] Delaware | Meta-theory à la carte[END_REF][START_REF] Forster | Coq à la carte: a practical approach to modular syntax with binders[END_REF] would likely make developments such as ours much easier.

Frameworks for the metatheory of dependent types.

In recent years, the community has shown a renewed interest in higher-level proofs that pack tedious details into convenient abstractions, and make more room for the big picture. Such proofs have been formulated in the categorical language of gluing [START_REF] Coquand | Canonicity and normalisation for dependent type theory[END_REF][START_REF] Bocquet | For the metatheory of type theory, internal sconing is enough[END_REF], as well as more sophisticated frameworks such as synthetic Tait computability [START_REF] Sterling | First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory[END_REF][START_REF] Gratzer | Implementing a modal dependent type theory[END_REF]. Abstraction aside, the features that set these apart from more traditional proofs are the use of proof-relevant logical relations on the one hand, and the replacement of partial equivalence relations with actual quotients on the other hand. Note that the inductive equality type of intensional type theory supports neither quotient types nor function extensionality, which is essential for manipulating the higherorder types involved in proofs of normalization by gluing. Accordingly, these proofs have a very extensional flavor, and as such are less amenable to implementation in a proof assistant based on intensional type theory. Moreover, the more sophisticated iterations rely on (multi)modal type theories as internal languages for feature-rich categories, for which mechanization is still in its infancy. Finally, if the goal is to obtain a certified implementation, the connection between these abstract proofs and an executable algorithm has yet to be explicited.

Partiality and general recursion in type theory.

Conversion checking algorithms are not structurally recursive in their inputs, and indeed their termination argument is highly complex, since it relies on normalization. Implementing a conversion checker in a type theory admitting only structural recursion, such as Coq's, is thus challenging. The more traditional approaches to non-structurally recursive functions either rely on well-foundedness, encoded as an inductive accessibility predicate; or on step-indexing, using an extra "fuel" parameter bounding the allowed number of recursive calls. The latter induces significant noise in the definition, while the former makes it impossible to separate the definition of a function from a proof of its termination/totality, and impedes computation by making it necessary to compute very large accessibility proofs. Alternatives include using co-inductive types [START_REF] Capretta | General Recursion via Coinductive Types[END_REF], and the Bove and Capretta [START_REF] Bove | Modelling general recursion in type theory[END_REF] approach, relying on an inductive characterization of the function's graph. A variant of the latter is the Braga method [START_REF] Larchey | PROOF AND COMPUTATION II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification[END_REF], which adds the extra goal of a wellbehaved extraction. All of these allow one to define partial functions, without the extra complexity of carrying a fuel parameter around. Termination (possibly only on a subset of the domain) can be established separately from the function definition.

Our approach, based on [START_REF] Mcbride | Turing-completeness totally free[END_REF], separates the description of a recursive function from its realization using a free monad to describe the calling graph. From this monadic object, the fuelled, coinductive or graph-based realization can all be easily recovered, depending on one's goals. As with the Bove-Capretta and Braga methods, this lets us define functions before arguing about their termination, but without foregoing the ease of execution of the fuelled variant. This part of our development relies on a library by Winterhalter [START_REF] Winterhalter | Composable partial functions in coq, totally for free[END_REF], which implements an enhanced version of McBride's ideas in Coq.

The Logical Relation(s)

We establish the metatheoretical properties from Section 2 through an equivalence between two different presentations of MLTT, a declarative presentation in the tradition of Martin-Löf's logical framework and an algorithmic one based on ideas from bidirectional typing (cf Section 6). The latter is used as an effective specification to prove the correction of the type checking algorithm. In this section, we give a high level tour of the logical relation techniques that we employ to relate both presentations. We roughly follow Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF], where a more detailed account can be found.

Metatheory Through Logical Relations

The point of the logical relation is to build a model of dependent type theory where types are interpreted as reducibility predicates, i.e. predicates on the untyped syntax that characterize well-behaved inhabitants. In order to model convertibility, these reducibility predicates are additionally equipped with a relation that we call reducible conversion, effectively turning them into PERs on untyped terms.

The first step in the construction of our model is thus the mutual definition of a reducibility predicate to characterize types (type-level reducibility), together with a reducibility predicate to characterize the inhabitants of every reducible type (term-level reducibility), and the associated reducible conversions. Then, we show that reducible conversions are equivalence relations (reflexive, symmetric, transitive), that reducibility implies weak-head normalization, is closed under weakening and anti-reduction, and is irrelevant, meaning that the term-level reducibility and reducible conversions associated to reducibly convertible types are equivalent. Next, in order to interpret the typing judgements in our model, we need to give a semantic interpretation of contexts and substitutions. To this end, we define the validity relations ⊩ 𝑣 by (freely) closing reducibility under substitutions of reducible terms. Finally, we prove the fundamental lemma by induction on the typing derivations, which states that any derivable declarative judgement is valid.

Theorem 4.1 (Fundamental lemma).

If Γ ⊢ 𝑡: 𝐴 then Γ ⊩ 𝑣 𝑡 : 𝐴 / 𝔙 Γ / 𝔙 𝐴 for 𝔙 Γ : ⊩ 𝑣 Γ and 𝔙 𝐴 : Γ ⊩ 𝑣 𝐴 / 𝔙 Γ .

Once the fundamental lemma is established, we obtain that any well-typed term has a weak-head normal form classified by (the weak-head normal form of) its type, from which we derive many metatheoretical properties: injectivity of type constructors (hence subject reduction), consistency and canonicity.

Three Logical Relations in One

The fundamental lemma is enough to establish the normalization properties but proving decidability of the conversion and of the type-checking requires more work. We first prove that the algorithmic presentation is complete with respect to derivability in the declarative system: any judgements derivable in the declarative system is also derivable in the algorithmic system. The completeness proof uses another logical relation defined in terms of the algorithmic system instead of the declarative one. In order to factor out the work, we reuse an idea of Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF] who parameterize the logical relation by an abstract conversion relation. We expand over this idea and parameterize the definition of the logical relation by a generic typing interface accommodating both declarative and algorithmic typing.

A first instantiation of the interface with declarative typing gives us among other (weak-head) normalisation and injectivity of type constructors. Two more instantiations, one with a mixed system combining declarative typing and algorithmic conversion, and one with a fully algorithmic system, let us relate the declarative and algorithmic judgements (see Section 6.4).

Design Choices for the Logical Relation

Our model relies on an untyped small-step reduction. That is, even though at times we bundle big-step reduction proofs with side-conditions that one or both sides are well-typed, we do not ask for typing proofs at the granularity of single reduction steps. As a result, subject reduction is a result that becomes available late, after the fundamental lemma has been proven.

Since this goes against the position explicitly advocated for in [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF], we believe that this design choice deserves some discussion. The first reason is purely rooted in engineering considerations. Basically, asking for a typed reduction duplicates the definition of typing derivations into a reduction variant. These inductive types are big, so they require a lot of boilerplate. It also makes experimenting with extensions to the type theory cumbersome, since one has to duplicate the additions in both inductive types. Given that typing itself is already quite redundant with conversion, this was deemed too unpractical.

Another more theoretical reason is that opting for typed reduction hardwires a specific kind of models, or equivalently a specific kind of generic typing interfaces. As typed reduction implies typing in the declarative system, and the logical relation implies reduction to a normal form, it is essentially asking that the resulting model is complete for declarative typing. Nonetheless, there are instances of typing interfaces that either cannot be proven complete early (i.e. before the fundamental lemma), or simply are not complete. A typical example of the latter is the instance used to prove untyped weak-head normalization of well-typed terms, which interprets all typing statements trivially.

Abstract Conversion of Neutrals

While reducible conversion finely characterizes the behaviour of canonical terms, it is essentially blind to the structure of neutral terms. Indeed, two neutrals are reducibly convertible simply if they are related by an abstract notion of neutral conversion, which is part of the generic typing interface. While we can recover properties of neutrals by a well-chosen instantiation of the interface, due to this structure neutral conversion cannot be defined mutually with reducibility, limiting its power. Hence, the declarative instance of the logical relation does not show that neutral destructors are injective (e.g. that if Γ ⊢ 𝑛 𝑢 ≅ 𝑛 ′ 𝑢 ′ : 𝑇 with 𝑛 and 𝑛 ′ neutral, then 𝑛 and 𝑢 are respectively convertible to 𝑛 ′ and 𝑢 ′ ). This is the core reason why we must instantiate the logical relation with algorithmic instances, to obtain properties of algorithmic neutral comparison which we cannot get more directly. The declarative instance also does not imply deep normalization, again because it does not go under neutrals. This is why the algorithm's proof of termination (Section 7.2) works directly on a conversion derivation.

Not-so-Small Induction-Recursion

The definitions of reducibility and validity that we outlined in Section 4.1 are challenging to express in type theory. In the case of reducibility, term-level reducibility is indexed over type-level reducibility, but type-level reducibility must depend on term-level reducibility in order to properly model dependent types that contain terms. Likewise, validity for contexts is mutually defined with validity for types and substitutions. In presence of inductive types with large elimination, these dependencies cannot be swept under the rug and must be taken into account in our model.

In their proof, Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF] solve this dependency puzzle by exploiting the powerful definition scheme of Agda, which allows them to mutually define an inductive type with a function defined by recursion on that very type. This feature is known as induction-recursion (IR for short) [START_REF] Dybjer | Induction-recursion and initial algebras[END_REF], and is commonly used to build models of dependent type theory. Thus, Abel et al. use IR to simultaneously define reducible types in context Γ, noted Γ ⊩⟨ℓ⟩ 𝐴, by induction, and associate an adequate reducibility predicate Γ ⊩⟨ℓ⟩ 𝑡 : 𝐴 / ℜ 𝐴 to every reducibility proof ℜ 𝐴 : Γ ⊩⟨ℓ⟩ 𝐴, by recursion on ℜ 𝐴 .

For instance, there is a constructor 𝔯𝔢𝔡 ℕ that, given any type 𝐴 and a proof 𝑟 : 𝐴 * 𝐍 that it weak-head reduces to 𝐍, induces a proof Γ ⊩⟨ℓ⟩ 𝐴. Correspondingly, the recursive case Γ ⊩⟨ℓ⟩ 𝑡 : 𝐴 / 𝔯𝔢𝔡 ℕ 𝐴 𝑟 is defined as reducibility at the type of natural numbers Γ ⊩ ℕ 𝑡. The latter asserts that the term 𝑡 is reducible if it weak-head reduces either to 0, to a successor S 𝑢 with Γ ⊩ ℕ 𝑢 reducible at 𝐍 too, or to a neutral term of type 𝐍 in context Γ. Note that the recursive definition of the reducibility predicates on terms is already needed in the simply typed setting to account for function types 𝐴 → 𝐵 that feature a negative occurrence of reducibility for terms in the domain.

Furthermore, reducibility is indexed by an integer ℓ that reflects the stratification of types into universe levels: the definition for ℓ = 0 only accounts for small types and their inhabitants (i.e. types that do not mention any universe), while the definition for ℓ = 1 accounts for all types, large or small. This way, we can declare that a term is a reducible inhabitant of the universe Γ ⊩⟨1⟩ 𝑡 : 𝐴 / 𝔯𝔢𝔡 U 𝐴 precisely when it is a reducible small type Γ ⊩⟨0⟩ 𝑡, without introducing any circularity.

In exchange for its elegance, IR introduces a serious gap between the metatheory and the object theory, which only supports a handful of inductive types. Even though exploring normalization proofs for IR is a valuable endeavour, we would rather go the other way and narrow this gap by recasting the definitions of Abel et al. to rely only on regular indexed inductive types. In fact, this restriction is enforced by our choice of proof assistant, since Coq does not support induction-recursion. In exchange, Coq supports impredicativity through its sort of propositions Prop, but we never rely on impredicativity in our development 2 .

Removing induction-recursion. Although IR is strictly stronger than plain indexed inductive types in general, it is possible to transform an inductive-recursive definition into an inductive type if the codomain of the recursive part is smaller than the universe of the inductive part-this is known as small induction-recursion [START_REF] Hancock | Small induction recursion[END_REF]. The transformation works as follows: we first define the codomain of the recursive part, here the reducibility predicates on term, and then define an inductive predicate carving out those elements of the codomain that arise from the evaluation of the putative inductive part of the induction-recursion instance. The inductive part is then recovered by packing together an element of the codomain together with an inductive proof that it is in the image of the inductive-recursive definition, while the recursive part just projects out the element of the codomain, forgetting the inductive proof.

Reducibility is not a priori an instance of small IR, as both the term-level and type-level reducibility are defined in the Definition RedRel@{i} := Con -> Term -> (Term -> Type@{i}) -> Type@{i+1}.

Inductive LR@{i} : ∀ (ℓ : TypeLevel), RedRel@{i} := | redU : Γ ⊩U A -> LR@{i+1} 1 Γ A (fun B => ∑ P, LR@{i} 0 Γ B P) | redℕ : Γ ⊩ℕ A -> LR@{i} ℓ Γ A Redℕ.

Notation "Γ ⊩⟨ℓ⟩ A" := (∑ P, LR ℓ Γ A P).

Notation "Γ ⊩⟨ℓ⟩ t : A / RA" := (fst RA t).

Figure 1. Simplified excerpt of reducibility via small induction-recursion in Coq

same universe to enable defining reducibility for inhabitants of the universe in terms of type-level reducibility. However, it turns out that it is possible to recast it as one, at the cost of some universe level juggling: we can define type-level reducibility for small types (the inductive part for ℓ = 0) in Type 1 , while term-level reducibility for small types lands in Type 0 . Then, type-level reducibility for large types is defined in Type 2 , and the term-level part in Type 1 . Proceeding in this fashion, we can define the reducibility predicate for the universe as the type-level reducibility of small types, while keeping the recursive part of the definition smaller than the inductive part.

The result is presented in Fig. 1 in a Coq-inspired syntax. Here, LR@{i} ℓ Γ A P encodes as a functional relation the fact that P : term -> Type@{i} is the reducibility predicate Γ ⊩⟨ℓ⟩ _ : 𝐴 / ℜ 𝐴 associated to the reducibility proof ℜ 𝐴 in the usual IR presentation. LR is heavily simplified compared to the development, serving as an illustration device to build up intuition. The first difference is that in addition to term reducibility we also have two additional predicates term -> Type@{i} and term -> term -> Type@{i}, for reducible conversion of types Γ ⊩⟨ℓ⟩ 𝐴 ≅ _ / ℜ 𝐴 and of terms Γ ⊩⟨ℓ⟩ _ ≅ _ : 𝐴 / ℜ 𝐴 , respectively.

Furthermore, observe that the universe level of the definition depends on the level ℓ, which is not possible in Coq since first-class universe levels are not available. Instead, we resort to what amounts to good old-fashioned code duplication, essentially defining reducibility once for small types, then once again for large types. Luckily, we sidestep inconvenient copy-pasting by a mix of universe polymorphism, a form of open recursion, and the definition of a custom induction principle (see Section 7.1 for details).

This stratification is unpleasant, but we cannot hope to eliminate it completely, because of Gödel's incompleteness theorem. Indeed, normalization implies consistency, and we cannot hope to prove consistency for MLTT with arbitrarily many universes in a metatheory that amounts to MLTTthus some code manipulation is necessary in order to extend the proof with one additional universe.

Abel et al. use induction-recursion a second time to define validity. The same strategy as the one we adopt for reducibility applies to validity as well, and lets us reformulate it as an indexed inductive type too. As a result, we completely remove induction-recursion, enabling a port of the proof to plain Coq.

The gap between the object and the meta. The metatheory for MLTT with 𝑛 universes should ideally be MLTT with 𝑛+1 universes, but unfortunately our proof requires at least one additional universe. Indeed, our definition of reducibility for 𝑛 universes requires 𝑛 + 2 universes in the metatheory, appearing as 𝑖 and 𝑖 + 1 in Fig. 1. 3 The definition of validity also fits within these 𝑛 + 2 universes, which means they should be sufficient for the proof to go through. In our development, for an object theory with a single universe, we should be using 3 universes from the metatheory to define reducibility and validity. This is the theory, but in practice we assume two additional universe levels that live below the universes used for reducibility. These are used in universe polymorphic definitions: since a definition must use the same number of universe variables for ℓ = 0 and ℓ = 1, we use these additional universes to instantiate the unneeded variables for the ℓ = 0 case. In the end, our development uses 𝑛 + 4 universes to show normalization for MLTT with 𝑛 universes.

An Algorithmic Presentation of MLTT

Although decidability of conversion is the main difficulty in a proof that type checking is decidable, the latter does not automatically follow from the former, except for heavily annotated systems -see e.g. Petković Komel [44, Proposition 10.3.5]. In fact, type checking for MLTT as defined by Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF] is undecidable for this very reason [START_REF] Dowek | The undecidability of typability in the lambdapi-calculus[END_REF][START_REF] Heine | Lectures on the Curry-Howard isomorphism[END_REF].

In our development, we cover this last mile and show decidability of typing with a full account of algorithmic type checking, presented in a bidirectional fashion [START_REF] Pierce | Local type inference[END_REF][START_REF] Dunfield | Bidirectional typing[END_REF]. The main idea of bidirectional typing is to refine typing into type inference, where the type of a term is an unknown to be found, and type checking, where the type is known, which are mutually defined, both as judgement and as functions. Following the strategy implemented e.g. by Coq, our terms contain enough annotations to ensure that inference is complete: every well-typed term infers a type. For instance, 𝜆abstractions are annotated with the type of the variable, i.e. Church-style. We do not investigate the common alternative in the bidirectional setting, which reduces the need for annotations by foregoing completeness of inference -some well-typed terms can only be type checked against a given type, because they do not contain enough type information by themselves.

Of course, algorithmic type checking relies on an algorithmic conversion. Ours is strongly inspired by the one of Abel et al. [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF], but puts more emphasis on its implicit bidirectional character. Indeed, our definition of algorithmic conversion is also decomposed into two mutually defined relations: general conversion checking, which is "checking" in the sense that it takes a type as input in order to compare the two terms; and a special neutral comparison relation, which is "inferring", in the sense that a common type for the two compared terms is synthesized while comparing them.

Algorithmic/Bidirectional Typing

Bidirectional typing, as an inductive predicate, is defined in AlgorithmicTyping. We denote type inference as Γ ⊢ 𝑡 ▷ 𝑇 , and type checking as Γ ⊢ 𝑡 ◁ 𝑇 . Each declarative typing rule for a term constructor gives rise to a corresponding rule for type inference, which ensures completeness of inference. For instance, the algorithmic rule for application is

infApp Γ ⊢ 𝑓 ▷ h Π 𝑥: 𝐴.𝐵 Γ ⊢ 𝑎 ◁ 𝐴 Γ ⊢ 𝑓 𝑢 ▷ 𝐵[𝑢]
Since terms might infer a type that does not exactly meet the required constraints, two extra rules let us handle conversion. For instance, in rule infApp above, 𝑎 might not infer 𝐴, but some 𝐴 ′ convertible to 𝐴. This is exactly what the only rule to derive type checking lets us do:

checKConv Γ ⊢ 𝑡 ▷ 𝑇 Γ ⊢ 𝑇 ≅ 𝑇 ′ Γ ⊢ 𝑡 ◁ 𝑇 ′
However, it can happen that we have a constraint only on the head constructor of the inferred type: for instance, the type of first premise of infApp should be a Π type. In that case, we cannot use the conversion checker to compare the type inferred by 𝑓 with Π 𝑥: 𝐴.𝐵, as neither 𝐴 nor 𝐵 are specified. This typically happens for destructors like application, where the head type constructor of the destructed term is known, but no more. In this case, we use reduction on the inferred type to expose its head constructor, and check that it matches the expected one. This is exactly what reduced inference, written Γ ⊢ 𝑡 ▷ h 𝑇 , 4 does, corresponding to the following rule:

infRed Γ ⊢ 𝑡 ▷ 𝑇 𝑇 ⋆ 𝑇 ′ Γ ⊢ 𝑡 ▷ h 𝑇 ′
The choice of using inference, reduced inference or checking in a premise when turning a declarative rule into an algorithmic one is a rather mechanical one. If the type is fully known from earlier premises or the term under consideration, we can use checking. If the type is fully unknown, we must use inference. Finally, when the type is partly unknown but has a prescribed shape we use reduced inference, in order to uncover said shape. In essence, this follows what Dunfield and Krishnaswami [START_REF] Dunfield | Bidirectional typing[END_REF] call the "Pfenning recipe", with the extra complication that we rely on reduction to exhibit the shape of types.

Algorithmic Conversion is Bidirectional Too

The easiest way to implement conversion checking is to fully normalize terms to 𝜂-long deep normal forms, and compare these for pure syntactic equality. However, this approach is neither faithful to our logical relation, which proceeds by iterated weak-head normalization, nor to most implementations, which also follow this lazy, stepwise approach. So we instead implement our conversion checker and the inductive relation that presents it by an interleaving of weak-head reduction and structural comparison of head normal forms.

The entry point of algorithmic conversion, in rule checK-Conv, is conversion between types, which is fairly straightforward: the two types are reduced to weak-head normal form, and are deemed convertible if they share the same head constructor and all their subtypes/subterms are recursively convertible. However, since these weak-head normal forms might be neutral inhabitants of the universe, we must be able to compare arbitrary neutral terms for conversion.

Algorithmic conversion of terms is subtler than for types. Indeed, consider the declarative conversion rules for functions: congruence of application and the 𝜂 rule for functions. How should information propagate in these rules? On one hand, the type 𝐵 in TeRmAppCong can only be obtained from the first premise, as we cannot uniquely invert the substitution 𝐵[𝑎]. On the other hand we would like to use the information that conversion happens at a Π-type to trigger TeRmFunExt. Thus, type information is useful for typedirected rules such as TeRmFunExt, yet it is impossible to propagate type information bottom-up through TeRmApp-Cong. The way out is to split conversion checking in two: a general relation to compare arbitrary terms, which takes a type as input, and can use it to trigger type-directed rules; and a second relation to specifically compare neutral terms, which infers a type, propagating it upside-down rather than bottom-up. We write the former relation Γ ⊢ 𝑡 ≅ 𝑡 ′ ◁ 𝑇 , using the same symbol as for type checking to insist on the bidirectional intuition, and the latter as Γ ⊢ 𝑛 ∼ 𝑛 ′ ▷ 𝑇 . This approach is sensible since extensionality rules are useless on neutrals, intuitively because 𝜂-expanding neutrals is useless as it cannot trigger any further computation, but only add an extra stuck layer. Once this design decision is fixed, the rest of the definition follows straightforwardly. In the end, conversion checking operates roughly as follows:

1. the two terms to compare and their type are reduced to weak-head normal form, 2. if the type is one with an 𝜂-rule (Π or Σ), then this rule is applied, and the 𝜂-expanded terms are recursively compared, 3. otherwise, if the two terms start with the same canonical constructor, it is stripped and its subterms are recursively compared, 4. finally, if the two terms are neutrals, they are compared using neutral comparison. Neutral comparison structurally traverses the two neutrals to find the variable on which they are stuck, gets its type from the context, and then uses that type information to recursively compare the other subterms with general conversion. If the variable is not the same, or the neutrals do not have the same structure, they are not convertible.

This general structure is the one followed by actual implementations, such as Coq or Agda, although they are of course more efficient than our naïve checker, typically by using a more refined implementation of reduction, and by using fast-paths to avoid reducing terms when it is unnecessary. It should nonetheless be possible to show correctness of these local optimisation with respect to our naïve prototype, thanks to the common global structure.

Bundled Algorithmic Typing: Invariants as an Induction Principle

There is an important caveat to algorithmic typing as defined in AlgorithmicTyping: it is not, in general, equivalent to declarative typing. The reason is the way we treat "boundaries" of judgements (e.g. Γ and 𝑇 in Γ ⊢ 𝑡 : 𝑇 ). In declarative typing, whenever Γ ⊢ 𝑡 : 𝑇 holds, ⊢ Γ and Γ ⊢ 𝑇 do too. This is enforced at the leaves of derivation trees, with rules like the following one for variables:

wfVaR ⊢ Γ (𝑥: 𝑇 ∈ Γ) Γ ⊢ 𝑥 : 𝑇
While this is sensible for a specification, it would be algorithmically much too costly, as it would mean re-checking the whole context at every leaf of the derivation. Instead, implementations maintain context well-formation as an invariant, rather than enforcing it: contexts are only ever extended with types which are known to be well-formed, but never fully checked. More generally, algorithmic judgements have three kinds of arguments: inputs, outputs and a subject. From the algorithmic point of view, both inputs and the subject are arguments of the function. The difference lies in what we assume about them: inputs are assumed to be well-formed before calling the function, while it is the function's role to ensure the subject is valid. For instance, in type inference Γ ⊢ 𝑡 ▷ 𝑇 , Γ is an input, 𝑡 is the subject, and 𝑇 is an output. The invariant to maintain is twofold. First, when a function is called, its inputs must already be known to be wellformed. Second, when it returns positively, both its subject and output must also be well-formed. This idea, originally due to McBride [START_REF] Mcbride | Basics of bidirectionalism[END_REF], and later dubbed "McBride discipline" in Lennon-Bertrand [START_REF] Lennon-Bertrand | Complete Bidirectional Typing for the Calculus of Inductive Constructions[END_REF][START_REF] Lennon-Bertrand | Bidirectional Typing for the Calculus of Inductive Constructions[END_REF], imposes clear constraints on how to design sensible bidirectional typing rules.

Most properties of algorithmic judgements only hold if their inputs are well-formed, and thus the invariant preservation must appear in proofs. In Lennon-Bertrand [START_REF] Lennon-Bertrand | Complete Bidirectional Typing for the Calculus of Inductive Constructions[END_REF], only soundness is shown directly for bidirectional typing, all other properties are shown on the declarative side and then transported to the bidirectional one. Thus, the McBride discipline is treated in an ad-hoc way, by carefully crafting the induction predicate for soundness to bake well-formation invariants in. Here, however, we need to show multiple properties of our algorithmic judgements, each needing their induction. The approach of modifying induction predicates would thus be inconvenient, because we would have to show the same invariant preservation over and over again in each inductive proof. Instead, in BundledAlgorithmicTyping we introduce bundled algorithmic judgement, and custom induction principles that handle invariant preservation once and for all.

Bundled algorithmic judgements ⊢ bn pack together an algorithmic judgement together with its pre-condition, i.e. wellformation of its inputs. These are the ones shown to be equivalent to the declarative ones. Note that only the "main" judgement is expressed algorithmically, all other ones are only declarative. This is because at this stage we have very few properties of algorithmic judgements, and it would thus be too difficult to construct these fields if they were expressed algorithmically. For declarative judgements, on the contrary, we can already rely on the declarative instance of the logical relation to give us powerful theorems.

While these bundled judgements are not inductively defined, they satisfy induction principles (BundledConvInduction and BundledTypingInduction). These trade a weaker conclusion -with extra well-formation hypotheses -for induction steps which are easier to prove, by having access to extra hypotheses. Concretely, in the induction step corresponding to infApp, on top of the induction hypotheses, one also knows that Γ is well-typed (pre-condition to the conclusion), and that moreover Γ ⊢ 𝑓 : Π 𝑥: 𝐴.𝐵, Γ ⊢ Π 𝑥: 𝐴.𝐵 and Γ ⊢ 𝑎 : 𝐴 (post-conditions of the premises).

We show these induction principles by regular induction on the unbundled algorithmic judgements. This amounts to showing once and for all invariant preservation, i.e. that preconditions to recursive calls are always satisfied provided pre-conditions of the conclusion and post-conditions of previous recursive calls. As a nice side-product, since part of the post-condition of the algorithmic judgements is their undirected counterparts, we get soundness of the bundled algorithmic judgements, for free. Theorem 6.1 (Soundness of bidirectional typing). If Γ ⊢ bn 𝑡: 𝐴 then Γ ⊢ 𝑡: 𝐴.

Properties of Algorithmic Typing

Using bundled induction, we are able to show most properties of algorithmic conversion in AlgorithmicConvProperties. In particular, it is a partial equivalence relation, it is stable under conversion of the type (that is, if Γ ⊢ 𝑡 ≅ 𝑡 ′ ◁ 𝑇 and Γ ⊢ 𝑇 ≅ 𝑇 ′ , then Γ ⊢ 𝑡 ≅ 𝑡 ′ ◁ 𝑇 ′ ), and neutral comparison implies conversion, at any type.

Stability under conversion requires injectivity of type constructors: we must know that we can use the same rule for 𝑇 ′ that was used for 𝑇 , so if e.g. 𝑇 reduces to a Π type, then 𝑇 ′ should too, with recursively related domain and codomain to invoke induction hypotheses.

Inclusion of neutral comparison in conversion requires normalization. Indeed, if a type supports an 𝜂 rule, this rule is applied systematically. Hence, we can go from neutral to comparison only at types without extensionality rules. We thus need to know that this cannot go forever, i.e. that the type normalizes and so that it cannot produce Π or Σ type constructors forever.

Yet, we cannot prove at this stage that bundled judgements form an instance of generic typing. In order to do so, we would need a mixed form of transitivity: if Γ ⊢ 𝑇 ≅ 𝑇 ′ (algorithmically) and Γ ⊢ 𝑇 ′ ≅ 𝑇 ″ (declaratively), then Γ ⊢ 𝑇 ≅ 𝑇 ″ (algorithmically). The natural proof idea is that if the rule for algorithmic conversion is e.g. congruence of Π, then by injectivity also 𝑇 ″ must reduce to a Π-type since it is convertible to 𝑇 ′ , and so the same rule applies. However, when we reach the base case of neutral types, we are stuck: as explained in Section 4.4, the logical relation does not show that neutrals are injective! Instead, we first inhabit an "intermediate" instance of generic typing, where conversion is taken to be (bundled) algorithmic, but typing is declarative. For this instance we can show all the required properties at that stage. By the fundamental lemma, we obtain completeness of bundled algorithmic conversion. This is enough to establish properties of algorithmic typing (AlgorithmicTypingProperties) and inhabit a third, fully algorithmic instance, concluding that algorithmic typing is complete. Once we show that algorithmic typing is decidable (Section 7.2), we obtain that type checking is decidable for declarative typing.

Engineering Aspects

We detail in this section some aspects of our implementation strategy that could inform future formal developments: first, the technical challenges to encode small induction recursion in Coq; second, a report on our use of a recent library for manipulating partial functions; and third, the impact of tactics and automation on our development.

Encoding Small Induction-Recursion, in Practice

Section 5 explains the high-level strategy to implement a logical relation for MLTT using small induction-recursion.

Here, we explain some implementation details that one must tackle in order to effectively encode small induction-recursion.

Avoiding code duplication.

Compared to what is presented in Section 5, we generalize the type of LR to LR@{i} : forall (ℓ : TypeLevel),

(forall ℓ', ℓ' < ℓ -> RedRel@{i}) -> RedRel@{i+1}
where 𝑖 is quantified over by prenex universe polymorphism and the additional parameter is a form of open recursion call. Although in practice we only care about levels 0 and 1, we can define non-uniformly the logical relation for every closed numeral with a single inductive definition for LR.

This makes it possible to share the definition of the logical relation by packing our two definitions of reducibility into a universe polymorphic container, whose universe level does not depend on ℓ but can be instantiated to either level.

Using the logical relation. Once the logical relation is

suitably encoded, we should avoid the specificities and intricacies of the encoding when proving properties. In particular, the induction principle automatically derived by Coq is unsuitable. This is due to the wish to only ever manipulate the complete, packed presentation of the logical relation when proving properties, but also to nested inductive occurrences in the definition of the logical relation, for which Coq lacks support when deriving induction principles. Thus, we show by hand a custom induction principle, which hides our encoding: users should never directly deal with it, but only interact with the logical relation through its encapsulation in the induction principle. In particular, the induction principle allows us to prove our lemmas on reducibility for all levels at once by making them universe polymorphic. Tactics also adapt to this custom induction principle, providing a proving experience very similar to what one would have with an induction recursion scheme supported directly by the proof assistant.

Proving properties of the logical relation.

The properties of the logical relation presented in Section 4.1 need to be proved in a precise order visible in the dependency graph of the corresponding files Fig. 2. Some properties would a priori need a mutual definition at types and terms levels: for instance reflexivity of reducible conversion at type 𝐈𝐝 𝐴 𝑥 𝑦 requires reflexivity proofs of reducible conversion for the subterms 𝑥 and 𝑦. We cut these dependencies by throwing in additional data in the logical relation that turns out to be redundant once we proved all the properties. We need to be careful that this additional data preserves the irrelevance of the logical relation with respect to reducible conversion. Indeed, irrelevance turns out to be the most difficult property to establish. In particular, we generalize the statement of the irrelevance of the logical relation so that it also encompasses cumulativity with respect to universe levels, and symmetry and transitivity of type conversion.

An Executable Type Checker, in Coq

Open recursion. The idea of our implementation, based on Winterhalter [START_REF] Winterhalter | Composable partial functions in coq, totally for free[END_REF], is to describe the calling graph of our algorithm, in the "open recursion" fashion. That way, we can use different approaches to execution, depending on our goals: a fuelled version can be efficiently run inside Coq, since it does not need to compute proofs; while a graphbased version leads to a certified total type checking function check, albeit one which should not be run without proof erasure. Moreover, this approach allows us to define functions before arguing about their termination, which means we can run a certified sound type checker returning valid type derivations without yet having proven its termination. 5Concretely, Winterhalter [START_REF] Winterhalter | Composable partial functions in coq, totally for free[END_REF] provides a parameterized type orec A B C of computations returning values of type C using open recursive call of type ∀ (x : A), B x. This type also supports undefined computations and calls to previously defined partial functions which is crucial to scale to a library consisting of multiple functions. As part of our development, we contributed a small extension to this calling mechanism that lower the required universe levels in the definition at the cost of making explicit the functions that can be called. The type ∇ x : A. B, which is defined as ∀ (x : A), orec A B (B x), represents open dependent partial functions from A to B.

Defining the partial functions. To define our partial functions in the most streamlined way, and to support effective reasoning about them, we rely on a wealth of techniques. The type orec A B describes the open recursion monad supporting the three generic operations rec, call and undefined. However, some of the functions we want to use also naturally involve an exception monad, for instance type inference should return either a type or an error. This means that to write proper monadic code, we must combine the exception and open recursion monad, and allow us to call a function using only one of the two monadic structure (reduction, which uses only open recursion monad but cannot error, or context access, which can error but is structurally recursive) inside the combined monad.

A nice aspect of the open recursion approach is its natural support for modularity. Because we do not close the recursion loop immediately, we are free to separately describe mutually defined functions. For instance, conversion checking corresponds to six mutually-defined routines, corresponding to the six conv_state tags. We can define separately the six corresponding functions (conv_ty, conv_ne, etc.), before finally combining them in the conv function. While we do this manually, encoding mutual recursion by non-mutual recursion with a tag, it might be interesting to explore the possibility to integrate such a mechanism directly into Winterhalter [START_REF] Winterhalter | Composable partial functions in coq, totally for free[END_REF]'s library.

The implementations themselves follow closely the algorithmic judgements. Only reduction is more complex: we implement a stack machine to be able to handle reduction under weak-head contexts. This machine is in essence a simplification of MetaCoq's. However, since we do not need to show its termination while defining it, we avoid the very complex dependent lexicographic order modulo a relation needed there [START_REF] Winterhalter | Formalisation and meta-theory of type theory[END_REF].

Reasoning on partial functions. We wish to establish three properties of our partial checking functions, namely

• soundness: if the function returns without raising an error, then the corresponding judgement is derivable; • completeness: if the corresponding judgement is derivable, then the function always returns a positive result; • termination: the function always returns a result (either a positive one or an error) when called on inputs satisfying its precondition. To prove Soundness, we use functional induction, induction principles tailored to the functions' calling graphs. A nice aspect of open recursion is that it makes it easy to perform this generically: a functional induction principle, which we can use out of the box, is part of Winterhalter [START_REF] Winterhalter | Composable partial functions in coq, totally for free[END_REF]. Since our functions directly follow the structure of the algorithmic judgements, establishing their soundness is straightforward, taking only a few lines of Ltac code -the difficult work is soundness of the algorithmic judgements with respect to the declarative ones. The only slightly subtle proof is for reduction, because of the stack machine used in the implementation.

Completeness is proven by bundled induction on algorithmic typing. Again, the main subtlety is in dealing with reduction. Indeed, because reduction cannot error, its completeness already encompasses termination, and we need to rely on a somewhat complex order, whose well-foundedness is established by normalization. Moreover, we need to show that whenever reduction throws an undefined error we are indeed in an unreachable branch. This means reasoning on the structure of well-typed stacks, to show that these branches correspond to ill-typed terms. Consequently, reduction is only complete when called on well-typed terms, and accordingly we need bundled induction to have this invariant available whenever reduction is called.

The last challenge is Termination of the conversion checking algorithm. We show that whenever Γ ⊢ 𝑡 ≅ 𝑢 ◁ 𝑇 , then conversion checking terminates on the inputs Γ, 𝑡, 𝑢 ′ and 𝑇 , for any well-typed 𝑢 ′ (unrelated with 𝑢). In essence, the structure of the proof of Γ ⊢ 𝑡 ≅ 𝑢 ◁ 𝑇 implicitly contains a derivation of deep normalization of 𝑡, including the relevant 𝜂-expansions, and we induct on that structure. Then, by reflexivity we know that any well-typed term 𝑡 is convertible to itself, which provides the derivation we need. Termination of type-checking is easy, since it is structural.

Executing partial functions.

From our functions, we can derive two implementations, with different purposes. The first is a fuelled implementation, which computes efficiently by induction on its extra natural number argument. Some examples are included in Execution, where we use the fuelled checker and its soundness to derive typing derivations by reflexion. Note how this only relies on soundness of the functions, but not on their completeness or termination. The second is the total implementation, which lets us derive a type checker with the type one expects for a proper decision procedure, in Decidability. This second implementation is not well-suited for direct execution inside Coq, because it computes proofs. Yet, it should be possible to use extraction [START_REF] Letouzey | Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq[END_REF][START_REF] Sozeau | Correct and Complete Type Checking and Certified Erasure for Coq[END_REF] to erase the proof certificates and obtain a certified implementation of the type checker in e.g. OCaml. We did not explore this path in depth yet, as the fuelled implementation in Coq was more useful to us, but this is definitely a direction to explore. While our implementation is relatively naïve and so not extremely efficient, it should still be able to type-check nontrivial examples without choking immediately, as it follows the general structure of the type checkers actually implemented in "real" kernels.

Automation and its Limitations

AutoSubst. We rely on the OCaml implementation of AutoSubst 2 [START_REF] Stark | Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions[END_REF][START_REF] Dapprich | Generating Infrastructural Code for Terms with Binders using MetaCoq and OCaml[END_REF] to deal with all the aspect of raw syntax, define untyped renamings and substitutions, generating boilerplate lemmas for these, and provide tactical support to discharge equational obligations. We heavily use the auto-generated lemmas indirectly via the asimpl tactic, a decision procedure for equations in the substitution calculus, which greatly alleviate the burden of these tedious goals. Still, there is room for improving AutoSubst and its use.

First, on top of raw renamings (functions nat -> term), we use an inductive notion of well-typed weakenings. Such a weakening can be turned into a renaming, but the cohabitation of the two notions makes the development cumbersome, and forces us to redefine AutoSubst's built-in asimpl to a tactic bsimpl which deals with this discrepancy. This problem partly stems from our formalization choices, rather than purely from AutoSubst, but it was unclear to us how to seamlessly combine inductive reasoning on weakenings with AutoSubst's renamings.

Second, the asimpl/bsimpl tactics, while providing useful decision procedures, have some practical limitations. They rely on setoid_rewrite, which quickly becomes slow, even on the not so large goals we have to handle, and become the performance bottleneck in a number of proof scripts. Moreover, they are only able to work on equations without existential variables (evars). This somewhat negates the otherwise powerful mechanism of evars, which lets one avoid giving a value upfront, rather refining it as one goes along with the proof.

Type-classes and tags.

As mentioned in Section 4.2, our logical relation is defined over a generic family of typing (and conversion, reduction, etc.) judgements. This is not only theoretically useful, but also doubles as a notational device, as we attach notations to the type classes for the generic judgements, in the Math Classes style [START_REF] Spitters | Type classes for mathematics in type theory[END_REF].

However, disambiguation between the various judgement families cannot be type-directed: all our typing judgements have the same type! Instead, we rely on a system of tags, inhabitants of a distinguished type tag with a single constructor mkTag. Each time we introduce a new family of judgements we also introduce an associated new opaque inhabitant of tag, and crucially keep the instances wrapped in a module. When working on this specific instance, this module can be imported, bringing the required instance in context. Similarly, when working generically, as usual with type classes, we introduce a hypothetical instance and tag. When there is only one specific or generic instance in context, it is safe to use the unqualified notation for typing Γ |-t : T, which will find the unique instance available. If, however, multiple instances are available (typically, when working with both the declarative and algorithmic systems), we use a different notation with an explicit tag Γ |-[de] t : T. This will find the only instance with the corresponding tag, here the declarative one. This strategy is similar to that used by Allamigeon et al. [START_REF] Xavier Allamigeon | Design patterns of hierarchies for order structures[END_REF], to solve a similar disambiguation problem in the context of canonical structures.

Automation. We use tactics to provide for judgementindependent notions, e.g. we use a single irrelevance tactic to use lemmas stating that one of the logical relation judgement is irrelevant in some of its parameters, or a boundary tactic to obtain "boundary" conditions of judgement, for instance to deduce from Γ |-t : T that also Γ |-T. An important part of the work achieved by the definition of the logical relation consist in its generalization of typing contexts through Kripke-style quantifications over renamings and substitutions, and we use instantiation tactics to automatically apply lemmas to the relevant hypotheses. Finally, to handle goals easily solved by using properties of a generic typing judgements, we provide gen_typing tactic, which performs a crude proof search. While these tactics already go some way in making proof writing higher level and more robust, we feel like there is a lot of space for designing tactics which are more powerful, robust and predictable. A typical issue with gen_typing, for instance, is that it either succeeds quickly or fails excruciatingly slowly, resulting in brittleness in the face of proof changes.

8 Future Work

Extensions and Improvements

Universes. It should be possible to add more universes to obtain a hierarchy of arbitrary finite length, and we see no theoretical obstacle in doing so, although there might be some practical metaprogramming challenges in the definition of the logical relation. Going beyond this and tackling a full countable hierarchy requires a different approach. If we want to stay in axiom-free Coq and keep avoiding inductionrecursion, the natural candidate is to use impredicativity. However, in Coq the impredicative sort Prop comes with restrictions, and it is currently unclear to us whether these restrictions would break a naïve port of our development to a logical relation in Prop. Inductive types. Our current formalization only handles rather simple inductive types, namely 𝐍 and 𝐈𝐝. Although these already encompass the main difficulties posed by inductive types, a natural extension would be to add W types: together with 𝐈𝐝, Σ, Π and a few base types, these can encode all indexed inductive types [START_REF] Hugunin | Why not w? In 26[END_REF][START_REF] Awodey | Inductive types in homotopy type theory[END_REF], which would really narrow the gap between our object and metatheory to a difference in universes. A more ambitious step would be to consider a general inductive scheme, as used in virtually any realistic system, and in MetaCoq, instead of particular examples.

Less naïve algorithms.

Our current algorithm is a naïve one, closely following the logical relation. An interesting improvement would be to implement term-directed extensionality rules [START_REF] Abel | Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs[END_REF]. Lennon-Bertrand [START_REF] Lennon-Bertrand | Bidirectional Typing for the Calculus of Inductive Constructions[END_REF]Chapter 6] shows that once one has access to the metatheory of the unoptimized, algorithmic variant, the proof of equivalence is straightforward. On the bidirectional side, we mentioned in Section 6 the common pattern, used for instance in the kernel of Agda [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF], of trading lighter annotations against incomplete inference. Typically, unannotated 𝜆 abstractions do not infer types and can be only be checked. While this makes type inference in general incomplete, we could adapt our formalization to show that type checking remains decidable.

Automation. On the practical side, we feel like there is a lot of room to improve automation, taking inspiration from the rich Coq ecosystem. Indeed, the main difficulty for a proof by logical relations is in the setup of the relation, but most proof obligations are rather repetitive and unsurprising. While our tactics already relieve us from quite a bit of this tedious work, they are far from alleviating all the pain.

Integration in MetaCoq.

While there is no formal relation between the present work and MetaCoq, we hope that in the future we will be able to connect the two, showing that the normalization axiom of MetaCoq is provable at least for a subset of the language. This is challenging, because there is still a significant gap between the two systems: we use typed conversion while MetaCoq's is untyped, MetaCoq uses pattern-matching and (guarded) fixpoints instead of recursors. The techniques we deploy to implement our type checker in Section 7.2 should be useful in MetaCoq too, delimiting further the portion of the code that depends on normalization.

Applications

Although our development is centered on MLTT, its modularity makes it amenable to study other type theories.

Definitional functor laws.

An ongoing parallel project building on this work extends MLTT with definitional functor laws for the map operation on lists: map id l ≡ l and map (f o g) l ≡ map f (map g l). In particular, the proofs of normalization and decidability adapt with relatively little changes on the original formalization.

Strict propositions and TT obs . Pujet and Tabareau [START_REF] Pujet | Impredicative observational equality[END_REF] were the first to attempt removing induction-recursion from their normalization proof, in order to provide a conservativity result for their theory TT obs : every numeric function that is definable in it can also be defined in MLTT. Yet, they still rely on first-class universe levels, a feature of Agda with little theoretical investigation. Moreover, they cannot restrict Agda's positivity checker to only accept "standard" inductive definitions, and as a matter of fact we had to significantly amend their inductively defined logical relation to have it accepted by Coq. Thus, it would be natural to solidify the conservativity result of Pujet and Tabareau [START_REF] Pujet | Impredicative observational equality[END_REF] by porting their development of TT obs to our setting.

Variants of MLTT and the multiverse. An enticing potential application of this work, beyond the implementation of various extension, is the ability to explore the interactions of multiple extensions. This could take the shape of adding multiple universes in order to delimit potentially incompatible extensions, e.g. with uniqueness of identity proofs such as TT obs and univalence such as some variant of homotopy type theory or cubical type theories, and study which interactions are sound, in the sense that they preserve the metatheorems established in this formalization.

Lemma 4 . 2 (

 42 Weak-head Normalization). If Γ ⊢ 𝑡 : 𝐴 then 𝑡 * 𝑤 where 𝑤 is a weak head normal form.

Lemma 4 . 3

 43 (Π-injectivity). If Γ ⊢ Π𝑥: 𝐴.𝐵 ≅ Π𝑥: 𝐴 ′ .𝐵 ′ then Γ ⊢ 𝐴 ≅ 𝐴 ′ and Γ, 𝑥: 𝐴 ⊢ 𝐵 ≅ 𝐵 ′ .

  TeRmAppCong Γ ⊢ 𝑓 ≅ 𝑔 : Π 𝑥: 𝐴.𝐵 Γ ⊢ 𝑎 ≅ 𝑏 : 𝐴 Γ ⊢ 𝑓 𝑎 ≅ 𝑔 𝑏 : 𝐵[𝑎] TeRmFunExt Γ, 𝑥: 𝐴 ⊢ 𝑓 𝑥 ≅ 𝑔 𝑥 : 𝐵 Γ ⊢ 𝑓 ≅ 𝑔 : Π 𝑥: 𝐴.𝐵

Theorem 6 . 2 (

 62 Completeness of bidirectional typing). If Γ ⊢ 𝑡: 𝐴 then Γ ⊢ bn 𝑡: 𝐴.

Theorem 6 . 3 (

 63 Decidability of typechecking). If Γ ⊢ and Γ ⊢ 𝐴, whether Γ ⊢ 𝑡 : 𝐴 holds is decidable for any term 𝑡.

Figure 2 .

 2 Figure 2. Dependency graph of the library

For any 𝑡, there exists at most one 𝑡 ′ such that 𝑡 𝑡 ′ .

We cannot completely avoid Prop, due to its ubiquity in Coq's standard library, for instance via the identity type eq. But the proofs would work just as well with a Type-valued equality.

Since Coq does not support algebraic universes of the shape 𝑖 + 1 in surface syntax, we need to use two levels 𝑖 < 𝑗 in the formalization.

The "h" stands for (weak-)head reduction.

This is visible in the dependency graph in Fig.2, where Functions only depends on the AST of terms, and Soundness only depends on the definition of AlgorithmicTyping, but not on the logical relation.

Received 2023-09-19; accepted 2023-11-25

Acknowledgment

We are indebted to Yannick Forster for setting up our CI, Adrien Guatto for the title idea, and Nicolas Tabareau for advising A. Adjedj at the start of the project.