Meven Lennon-Bertrand

Ls2n

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Keywords: 2012 ACM Subject Classification Theory of computation → Type theory Bidirectional Typing, Calculus of Inductive Constructions, Coq, Proof Assistants Digital Object Identifier 10.4230/LIPIcs.CVIT.2016.23

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). It introduces a new judgement intermediate between the usual inference and checking, dubbed constrained inference, to handle the presence of computation in types. The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.

Introduction

In logical programming, an important characteristic of judgements is the mode of the objects involved, i.e., which ones are considered inputs or outputs. When examining this distinction for a typing judgement Γ ⊢ t : T , both the term t under inspection and the context Γ of this inspection are usually known, they are thus inputs (although some depart from this, see [START_REF] Jim | What are principal typings and what are they good for?[END_REF]). The mode of the type T , however, may vary: should it be inferred based upon Γ and t, or do we merely want to check whether t conforms to a given T ? Both are sensible approaches, and in fact typing algorithms for complex type systems usually alternate between them during the inspection of a single term/program. The bidirectional approach makes this difference between modes explicit, by decomposing undirected1 typing Γ ⊢ t : T into two separate judgments Γ ⊢ t ▷ T (inference) and Γ ⊢ t ◁ T (checking) 2 , that differ only by modes. This decomposition allows theoretical work on practical typing algorithms, but also gives a finer grained structure to typing derivations, which can be of purely theoretical interest even without any algorithm in sight. Although this seems appealing, and despite advocacy by McBride [START_REF] Mcbride | Basics of bidirectionalism[END_REF][START_REF] Mcbride | Check the box! In 25[END_REF] to adopt this approach when designing type systems, most of the theoretical work on dependent typing to this day remains undirected. Others have described on paper bidirectional algorithms for dependent types, starting with Coquand [START_REF] Coquand | An algorithm for type-checking dependent types[END_REF] and continuing with Norell [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF] or Abel [START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF]. However, all of these consider unannotated λ-abstractions, and use bidirectional typing as a way to remedy this lack of annotations. This is sensible when looking for lightness of the input syntax, but poses an inherent completeness problem, as a term like (λ x.x) 0 does not type-check against type N in those systems. Very few have considered the case of annotated abstractions, apart from Asperti and the Matita team [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF], who however concentrate on specific problems pertaining to unification and implementation of the Matita elaborator, without giving a general bidirectional framework. They also do not consider the problem of completeness with respect to a given undirected system, as it would fail in their setting due to the undecidability of higher order unification.

Thus, we wish to fill a gap in the literature, by describing a bidirectional type system that is complete with respect to the (undirected) Calculus of Inductive Constructions (CIC). By completeness, we mean that any term that is typable in the undirected system should also infer a type in the bidirectional one. This feature is very desirable when implementing kernels for proof assistants, whose algorithms should correspond to their undirected specification, never missing any typable term. The bidirectional systems we describe thus form intermediate steps between actual algorithms and undirected type systems. This step has proven useful in an ongoing completeness proof of MetaCoq's [START_REF] Sozeau | The MetaCoq Project[END_REF] type-checking algorithm3 : rather than proving the algorithm complete directly, the idea is to prove it equivalent to the bidirectional type system, separating the implementation problems from the ones regarding the bidirectional structure.

But the interest of having a bidirectional type system equivalent to the undirected one is not limited to the link with algorithms, it is also purely theoretical. First, the structure of a bidirectional derivation is more constrained than that of an undirected one, especially regarding the uses of computation. This finer structure can make proofs easier, while the equivalence ensures that they can be transported to the undirected world. For instance, in a setting with cumulativity/subtyping, the inferred type for a term t should by construction be smaller than any other types against which t checks. This provides an easy proof of the existence of principal types in the undirected system. The bidirectional structure also provides a better base for new type systems. This was actually the starting point for this investigation: in [START_REF] Lennon-Bertrand | Gradualizing the calculus of inductive constructions[END_REF], we quickly describe a bidirectional variant of CIC, as the usual undirected CIC is unfit for the gradual extension we envision due to the too high flexibility of a free-standing conversion rule. This is the system we wish to thoroughly describe and investigate here.

Outline We start by giving in Section 2 a general roadmap in the simple setting of pure type systems, including the introduction of a constrained inference judgement that had not been clearly singled out in previous works. With the ideas set clear, we go on to the real thing: a bidirectional type system proven equivalent to the Predicative Calculus of Cumulative Inductive Constructions -PCUIC, the extension of CIC nowadays at the heart of Coq. This equivalence has been formalised on top of MetaCoq [START_REF] Sozeau | Coq Coq Correct! Verification of Type Checking and Erasure for Coq[END_REF] 4 We next turn back to less technical considerations, as we believe that the bidirectional structure is of general theoretical interest. Section 4 thus describes the value of basing type systems on the bidirectional system directly rather than on the equivalent undirected one. Finally Section 5 investigates related work, and in particular tries and identify the implicit presence of constrained inference in various earlier articles, showing how making it explicit clarifies those.

2

Warming up with CCω

Undirected CCω

As a starting point, let us consider the system CCω. It is the backbone of CIC, and we can already illustrate most of our methodology on it. CCω belongs to the wider class of pure type systems (PTS), that has been thoroughly studied and described, see for instance [START_REF] Barendregt | Lambda calculi with types[END_REF]. Since there are many presentational variations, let us first give a precise account of our conventions. Terms in CCω are given by the grammar

t ::= x | □ i | Π x : t.t | λ x : t.t | t t
where the letter x denotes a variable (so will letters y and z), and the letter i is an integer (we will also use letters j, k and l for those). All other Latin letters will be used for terms, with the upper-case ones used to suggest the corresponding terms should be though of as types -although this is not a syntactical separation. We abbreviate Π x : A.B by A → B when B does not depend on x, as is customary. On those terms, reduction ⇝ is defined as the least congruence such that (λ x :

T.t) u ⇝ t[x := u],
where t[x := u] denotes substitution. Conversion ≡ is the symmetric, reflexive, transitive closure of reduction. Finally, contexts are lists of variable declarations x : t and are denoted using capital Greek letters. We write • for the empty list, Γ, x : T for concatenation, and (x : T ) ∈ Γ if (x : T ) appears in Γ. Combining those, we can define typing Γ ⊢ t : T as in Figure 1, where i ∨ j denotes the maximum of i and j. We say a context Γ is well-formed if ⊢ Γ, a type T is well-formed in a context Γ if there exists i such that Γ ⊢ T : □ i , and a term is well-formed in a context Γ if there exists T such that Γ ⊢ t : T . We also use well-typed for the latter, and leave the context implicit for the last two when it is clear from context. These rules differ from more usual PTS presentations such as [START_REF] Barendregt | Lambda calculi with types[END_REF] on the Var and Sort rules so as to avoid general weakening (which is however admissible) and single out the context well-formedness judgment. Premises are not minimal in order to provide more generous inductive hypotheses when doing proofs by induction on derivations. However, this presentation can easily be seen to be equivalent to that of [START_REF] Barendregt | Lambda calculi with types[END_REF].

As any PTS, CCω has many desirable properties. We summarize the ones we rely on here. Detailed proofs in the context of PTS can be found in [START_REF] Barendregt | Lambda calculi with types[END_REF], and formalisation of the corresponding properties for PCUIC are an important part of MetaCoq.

▶ Proposition 1 (Properties of CCω

Turning CCω Bidirectional

McBride's discipline To design our bidirectional type system, we follow a discipline exposed by McBride [START_REF] Mcbride | Basics of bidirectionalism[END_REF][START_REF] Mcbride | Check the box! In 25[END_REF]. The central point is to distinguish in a judgment between the subject, C V I T 2 0 1 6

23:4

Complete Bidirectional Typing for the Calculus of Inductive Constructions whose well-formedness is under scrutiny, from inputs, whose well-formedness is a condition for the judgment to behave well, and outputs, whose well-formedness is a consequence of the judgment. For instance, in inference Γ ⊢ t ▷ T , the subject is t, Γ is an input and T is an output. This means that one should consider whether Γ ⊢ t ▷ T only in cases where ⊢ Γ is already known, and if the judgment is derivable it should be possible to conclude that both t and T are well-formed. All inference rules are to preserve this invariant. This means that inputs to a premise should be well-formed whenever the inputs to the conclusion and outputs and subjects of previous premises are. Similarly the outputs of the conclusion should be well-formed if the inputs of the conclusion and the subjects and outputs of the premises are assumed to be so. This distinction also applies to the computation-related judgments, although those have no subject. For conversion T ≡ T ′ both T and T ′ are inputs, and thus should be known to be well-formed beforehand. For reduction T ⇝ * T ′ , T is an input and T ′ is an output, so only T needs to be well-formed, with the subject reduction property of the system ensuring that the output T ′ is also well-formed.

⊢ Γ ⊢ • Empty ⊢ Γ Γ ⊢ A : □ i ⊢ Γ, x : A Ext Γ ⊢ t : T ⊢ Γ Γ ⊢ □ i : □ i+1 Sort ⊢ Γ (x : A ∈ Γ) Γ ⊢ x : A Var Γ ⊢ A : □ i Γ, x : A ⊢ B : □ j Γ ⊢ Π x : A.B : □ i∨j Prod Γ ⊢ Π x : A.B : □ i Γ, x : A ⊢ t : B Γ ⊢ λ x : A.t : Π x : A.B Abs Γ ⊢ t : Π x : A.B Γ ⊢ u : A Γ ⊢ t u : B[x := u] App Γ ⊢ t : A Γ ⊢ B : □ i A ≡ B Γ ⊢ t : B Conv
Constrained inference Beyond the already described inference and checking judgements another one appears in the bidirectional typing rules of Figure 2: constrained inference, written Γ ⊢ t ▷ h T , where h is either Π or □ -and will be extended once we introduce more type formers. Constrained inference is a judgement -or, rather, a family of judgements indexed by h -with the exact same modes as inference, but where the type output is not completely free. Rather, as the name suggests, a constraint is imposed on it, namely that its head constructor can only be the corresponding element of h. This is needed to handle the behaviour absent in simple types that some terms might not have a desired type "on the nose", as exemplified by the first premise Γ ⊢ t ▷ Π Π x : A.B of the App rule for t u. Indeed, it would be too much to ask t to directly infer a Π-type, as some reduction might be needed on T to uncover this Π. Checking also cannot be used, because the domain and codomain of the tentative Π-type are not known at that point: they are to be inferred from t.

Γ ⊢ t ▷ □ □ i Sort-Inf Γ ⊢ t ▷ T T ⇝ * Π x : A.B Γ ⊢ t ▷ Π Π x : A.B Prod-Inf

Structural rules

To transform the rules of Figure 1 to those of Figure 2, we start by recalling that we wish to obtain a complete bidirectional type system. Therefore any term should infer a type, and thus all structural rules (i.e. all rules where the subject of the conclusion starts with a term constructor) should give rise to an inference rule. It thus remains to choose the judgements for the premises, which amounts to determining their modes. If a term in a premise appears as input in the conclusion or output of a previous premise, then it can be considered an input, otherwise it must be an output. Moreover, if a type output is unconstrained, then inference can be used, otherwise we must resort to constrained inference. This applies straightforwardly to most rules but the PTS-style Abs. Indeed, neither Γ ⊢ Π x : A.B : □ i nor Γ, x : A ⊢ t : B can be taken as the first bidirectional premise: the first one because B is not known from inputs to the conclusion, and the second because context Γ, x : A is not known to be well-formed from the conclusion. For general PTS, this is quite problematic, as demonstrated by Pollack [START_REF] Pollack | Typechecking in Pure Type Systems[END_REF]. For CCω, however, the solution is simple. Replacing Γ ⊢ Π x : A.B : □ i by the equivalent Γ ⊢ A : □ j and Γ, x : A ⊢ B : □ j ′ , the former can become the first premise, ensuring that type inference for t is done in a well-formed context, and the latter can be dropped based upon the invariant that outputs -here the type B inferred for t -are well-formed.

Similarly, as the context is always supposed to be well-formed as an input to the conclusion, it is not useful to re-check it, and thus the premise of Sort and Var can be safely dropped. This is in line with implementations, where the context is not re-checked at leaves of a derivation tree, with performance issues in mind. The well-formedness invariants then ensure that any derivation starting with the (well-formed) empty context will only handle well-formed contexts.

Computation rules

We are now left with the non-structural conversion rule. As we observed, there are two possible modes for computation: if both sides are inputs, conversion can be C V I T 2 0 1 6

23:6

Complete Bidirectional Typing for the Calculus of Inductive Constructions used, but if only one is known one must resort to reduction, and the other side becomes an output instead. Rule Check corresponds to the first case, while rules Prod-Inf and Sort-Inf both are in the second case. This difference in turn introduces the need to separate between checking, that calls for the first rule, and constrained inference, that requires the others.

The need to split the conversion rule into a (weak-head) reduction and conversion subroutine depending on the mode is known to the implementors of proof assistants [START_REF] Abel | A partial type checking algorithm for type:type[END_REF]. However, we wish to de-emphasize the role devoted specifically to reduction in the description of those algorithms, instead putting constrained inference forward. Indeed, reduction is only a means to determine whether a certain term fits into a certain category of types. In the setting of CCω, there is mainly one way to do so, which is to reduce its type until its head constructor is exposed. However, as soon as conversion is extended, for instance with unification [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF], coercions [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF][START_REF] Sozeau | Subset coercions in coq[END_REF] or graduality [START_REF] Lennon-Bertrand | Gradualizing the calculus of inductive constructions[END_REF], reduction is not enough any more. Singling out constrained inference then makes the required modification to the typing rules clearer. We come back to this more in length in Section 5.1.

Properties

Let us now state the two main properties relating the bidirectional system to the undirected one: it is both correct (terms typable in the bidirectional system are typable in the undirected system) and complete (all terms typable in the undirected system are also typable in the bidirectional system).

Correctness

A bidirectional derivation can be seen as a refinement of an undirected derivation. Indeed, the bidirectional structure can be erased -replacing each bidirectional rule with the corresponding undirected rule -to obtain an undirected derivation, but for missing sub-derivations, which can be retrieved using the invariants on well-formedness of inputs and outputs. Thus, we get the following correctness theorem -note how McBride's discipline manifests as well-formedness hypothesis on inputs.

▶ Theorem 2 (Correctness of bidirectional typing for CCω). If Γ is well-formed and

Γ ⊢ t ▷ T or Γ ⊢ t ▷ h T then Γ ⊢ t : T . If Γ and T are well-formed and Γ ⊢ t ◁ T then Γ ⊢ t : T .
Proof. The proof is by mutual induction on the bidirectional typing derivation.

Each rule of the bidirectional system can be replaced by the corresponding rule of the undirected system, with all three Check, Prod-Inf and Sort-Inf replaced by Conv, Abs using an extra Prod rule. In all cases, the induction hypothesis can be used on sub-derivations of the bidirectional judgment because the context extensions and checking are done with types that are known to be well-formed by induction hypothesis on previous premises and validity. Some sub-derivations of the undirected rules that have no counterpart in the bidirectional ones are however missing. In rules Sort and Var the hypothesis that ⊢ Γ is enough to get the required premise. For rule Check, the well-formedness hypothesis on the type is needed to get the second premise of rule Conv. As for Prod-Inf and Sort-Inf, that second premise is obtained using the induction hypothesis, validity and subject reduction. Finally, the missing premise on the codomain of the product type in rule Abs is obtained by validity.

Uses of validity could alternatively be handled by strengthening the theorem to incorporate the well-formedness of types when they are outputs. ◀

Completeness

Let us now state the most important property of our bidirectional system: it does not miss any undirected derivation.

▶ Theorem 3 (Completeness of bidirectional typing for CCω). If Γ ⊢ t : T then there exists T ′ such that Γ ⊢ t ▷ T ′ and T ′ ≡ T .

Proof. The proof is by induction on the undirected typing derivation. Rules Sort and Var are base cases, and can be replaced by the corresponding rules in the bidirectional world. Rule Conv is a direct consequence of the induction hypothesis on its first premise, together with transitivity of conversion.

For rule Prod, we need the intermediate lemma that if T is a term such that T ≡ □ i , then also T ⇝ * □ i . This is a consequence of confluence of reduction. In turn, it implies that if Γ ⊢ t ▷ T and T ≡ □ i then Γ ⊢ t ▷ □ □ i , and is enough to conclude for that rule.

In rule Abs, the induction hypothesis gives Γ ⊢ Π x : A.B ▷ T for some T , and an inversion on this gives Γ ⊢ A ▷ □ □ i for some i. Combined with the second induction hypothesis, we get Γ ⊢ λ x : A.t ▷ Π x : A.B ′ for some B ′ such that B ≡ B ′ , and thus Π x : A.B ≡ Π x : A.B ′ as desired.

We are finally left with the App rule. We know that Γ ⊢ t ▷ T with T ≡ Π x :

A.B. Confluence then implies that T ⇝ * Π x : A ′ .B ′ for some A ′ and B ′ such that A ≡ A ′ and B ≡ B ′ . Thus Γ ⊢ t ▷ Π Π x : A ′ .B ′ .
But by induction hypothesis we also know that Γ ⊢ u ▷ A ′′ with A ′′ ≡ A and so by transitivity of conversion Γ ⊢ u ◁ A ′ . We can thus apply App to conclude. ◀ Contrarily to correctness, which kept a similar derivation structure, completeness is of a different nature. Because in bidirectional derivations the conversion rules are much less liberal than in undirected derivations, the crux of the proof is to ensure that conversions can be permuted with structural rules, in order to concentrate them in the places where they are authorized in the bidirectional derivation. In a way, composing completeness with conversion gives a kind of normalization procedure that produces a canonical undirected derivation by pushing all conversions down as much as possible.

Reduction strategies

The judgements of Figure 2 are syntax-directed, in the sense that there is always at most one rule that can be used to derive a certain typing judgements. But with the rules as given there is still some indeterminacy. Indeed when appealing to reduction no strategy is fixed, thus two different reducts give different uses of the rule, resulting in different inferred types -although those are still convertible. However, a reduction strategy can be imposed to completely eliminate indeterminacy in typing, leading to the following.

▶ Proposition 4 (Reduction strategy). If ⇝ * is replaced by weak-head reduction in rules

Sort-Inf and Prod-Inf, then given a well-formed context Γ and a term t there is at most one derivation of Γ ⊢ t ▷ T and Γ ⊢ t ▷ h T , and so in particular such a T is unique. Similarly, given well-formed Γ and T and a term t there is at most one derivation of Γ ⊢ t◁T . Moreover, the existence of those derivations is decidable.

The algorithm for deciding the existence of the derivations is straightforward from the bidirectional rules, it amounts to structural recursion on the subject. From CCω to PCUIC CCω is already a powerful system, but today's proof assistants rely on much more complex features. There are two main areas of differences between CCω and the Predicative Calculus of Cumulative Inductive Constructions (PCUIC), the type theory nowadays behind the Coq proof assistant. Adapting to those is a good stress test for the bidirectional approach: seamlessly doing so is a good sign that the general methodology we presented is robust. The first area of difference are the universes. While on paper those are simply integer, to handle typical ambiguity and polymorphic (co)-inductive types, PCUIC uses algebraic universes, containing level variables, algebraic ∨ and +1 operators, and a special level for the sort Prop. Moreover, those universes are cumulative, that is they behave as if smaller universes were included in larger ones. The precise handling of the algebraic universes is abstracted away in MetaCoq, and quite similar in the directed and undirected systems, so it did not prove too difficult to handle. Cumulativity, however, introduces some not-so-small differences with the previous presentation, so we spend some time on it in Section 3.1.

The second is the addition of new base type and term constructors. We describe the treatment of inductive types in Section 3.2. Co-inductive types and records behave very similarly to inductive types at the level of typing, so we do not dwell on them. The difference lies mainly at the level of reduction/conversion, but as our type system treats those as black boxes the differences have a negligible impact.

The interplay between those two areas is quite subtle, and we were able to uncover an incompleteness bug in the current kernel of Coq regarding pattern-matching of cumulative inductive types. This bug had gone unnoticed until our formalisation, but was causing subject reduction failures in some corner cases 5 . We try and give an intuition of the problem in Section 3.2.

Cumulativity

PCUIC incorporates a limited form of subtyping, corresponding to the intuition that smaller universes are included in larger ones. Conversion ≡ is therefore replaced by cumulativity ⪯, the main difference being that the constraint on universes is relaxed. For conversions □ i ≡ □ j only when i = j, but for cumulativity □ i ⪯ □ j whenever i ≤ j -and this extends by congruence through most constructors. The conversion rule is accordingly replaced by the following cumulativity rule

Γ ⊢ t : A Γ ⊢ B : □ i A ⪯ B Γ ⊢ t : B Cumul
This reflects the view that universes □ i should be included one in the next when going up in the hierarchy. In CCω, all types for a given term t in a fixed context Γ are equally good, as they are all convertible. This is not the case any more in presence of cumulativity, as we can have T ⪯ T ′ but not T ≡ T ′ . Of particular interest are principal types, defined as follows.

▶ Definition 5 (Principal type). The term T is called a principal type for term t in context Γ if it is a least type for t in Γ, that is if Γ ⊢ t : T and for any T ′ such that Γ ⊢ t :

T ′ we have T ⪯ T ′ .
The existence of such principal types is no so easy to prove directly but quite useful, as they are in a sense the best types for any terms. Indeed, if T is a principal type for t in Γ and T ′ is any other type for t, the Cumul rule can be used to deduce Γ ⊢ t : T ′ from Γ ⊢ t : T , which in general is not the case if T is not principal. Similarly, if T and T ′ are two types for a term t, then they are not directly related, but the existence of principal types ensures that there exists some T ′′ that is a type for t and such that T ⪯ T ′ and T ⪯ T ′′ , indirectly relating T ′ and T ′′ .

Reflecting this modification in the bidirectional system of course calls for an update to the computation rules. The change to the Check rule is direct: simply replace conversion with cumulativity.

Γ ⊢ t ▷ A A ⪯ B Γ ⊢ t ◁ B Cumul
As to the constrained inference rules, there is no need to modify them. Intuitively, this is because there is no reason to degrade a type to a larger one when it is not needed. We only resort to cumulativity when it is forced by a given input. In that setting, completeness becomes the following:

▶ Theorem 6 (Completeness with cumulativity). If Γ ⊢ t : T using rules of Figure 1 replacing Conv with Cumul, then Γ ⊢ t ▷ T ′ is derivable with rules of Figure 2 replacing Check with Cumul for some T ′ such that T ′ ⪯ T .

In that setting, even without fixing a reduction strategy as in Proposition 4, there is a weaker uniqueness property for inferred types.

▶ Proposition 7 (Uniqueness of inferred type). If Γ is well-formed, Γ ⊢ t ▷ T and Γ ⊢ t ▷ T ′ then T ≡ T ′ . Similarly if Γ is well-formed, Γ ⊢ t ▷ h T and Γ ⊢ t ▷ h T ′ then T ≡ T ′ .
Proof. Mutual induction on the first derivation. It is key that constrained inference rules only reduce a type, so that the type in the conclusion is convertible to the type in the premise, rather than merely related by cumulativity. ◀

In particular, combining those two properties with a correctness property akin to Theorem 2, we can prove that any inferred type is principal, and so that they both exist and are computable since the bidirectional judgement can still be turned into an algorithm in the spirit of Proposition 4.

▶ Proposition 8 (Principal types). If Γ is well-formed and Γ ⊢ t ▷ T then T is a principal type for t in Γ.

Proof. If Γ ⊢ t : T ′ , then by completeness there exists some T ′′ such that Γ ⊢ t ▷ T ′′ and moreover T ′′ ⪯ T ′ . But by uniqueness T ≡ T ′′ ⪯ T ′ and thus T ⪯ T ′ , and T is indeed a principal type for t in Γ. ◀

Reasoning on the bidirectional derivation thus makes proofs easier, while the correctness and completeness properties ensure they can be carried to the undirected system. Another way to understand this is that seeing completeness followed by correction as a normalization procedure on derivations, the produced canonical derivation is more structured and thus more amenable to proofs. Here for instance the uniqueness of the inferred type translates to the existence of principal types via correctness, and the normalization of the derivations optimizes it to derive a principal type.

C V I T 2 0 1 6

Γ ⊢ t ▷ h T Γ ⊢ t ▷ T T ⇝ * Σ x : A.B Γ ⊢ t ▷ Σ Σ x : A.B Σ-Inf

Inductive Types

Sum type Before we turn to the general case of inductive types of the formalisation, let us present a simple inductive type: dependent sums. The undirected rules are given in Figure 3, and are inspired from the theoretical presentation of such dependent sums, such at the one of the Homotopy Type Theory book [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF]. In particular, we use the same convention to write y.P when variable y is bound in P . Note however that contrarily to [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF], some typing information is kept on the pair constructor. Exactly as for the abstraction, this is to be able to infer a unique, most general type in the bidirectional system. Indeed, without that information a pair (a, b) could inhabit multiple types Σ x : A.B because there are potentially many incomparable types B such that B[x := a] is a type for b, as even if B[x := a] and B ′ [x := a] are convertible B and B ′ may be quite different, depending of which instances of a in B[x := a] are abstracted to x.

To obtain the bidirectional rules of Figure 4, first notice that all undirected rules are structural and must thus become inference rules if we want the resulting system to be complete, just as in Section 2. The question therefore is again to know which modes to

Γ ⊢ t ▷ N N Γ ⊢ t ▷ T T ⇝ * Id A a a ′ Γ ⊢ t ▷ Id Id A a a ′

Figure 5 Other bidirectional inductive types

This same approach can be readily extended to other usual inductive types, with recursion or indices posing no specific problems, see Figure 5. The choice to use ▷ □ rather than ◁ for types is guided by the intuition that the universe level of e.g. A in Id A a a ′ is free, similarly to what happens for sum types.

Polymorphic, Cumulative Inductive Types

The account of general inductive types in PCUIC is quite different from the one we just gave. The main addition is universe polymorphism [START_REF] Sozeau | Universe polymorphism in Coq[END_REF], which means that inductive types and constructors come with explicit universe levels. The Σ-type of the previous paragraph, for instance, would contain an explicit universe level i, and both A and B would be checked against □ i rather than having their level inferred. This makes the treatment of complex inductive types possible by using checking uniformlyrather than relying on constrained inference to infer universe levels -at the cost of possibly needless annotations, as here with Σ-types. To make that polymorphism more seamless, those polymorphic inductive types are also cumulative [START_REF] Timany | Cumulative Inductive Types In Coq[END_REF]: in much the same way as □ i ⪯ □ j if i ≤ j, also N @i ⪯ N @j , where N @i denotes the polymorphic inductive N at universe level i. This enables lifting from a lower universe to a higher one, so that for instance ⊢ 0 @i : N @j if i ≤ j. PCUIC as presented in MetaCoq also presents constructors and inductive types as functions, rather than requiring them to be fully applied, and it separates recursors into a pattern-matching and a fixpoint construct, the latter coming with a specific guard condition to keep the normalization property enjoyed by a system with recursors. A sketch of the bidirectional rules is given in Figure 6, for a generic inductive I. We use bold characters to denote lists -for instance a is a list of terms -and indexes to denote a specific element -so that a k is the k-th element of the previous. The considered inductive I has parameters of type X, indices of type Y and inhabits some universe □ l . Its constructors c k are of types Π(x : X)(y : Y k ), I x u, with u k terms possibly depending on both x and y. Since we are considering a polymorphic inductive type, all of those actually have to be instantiate with universe levels, an operation we denote with @i .

C V I T 2 0 1 6 23:12 Complete Bidirectional Typing for the Calculus of Inductive Constructions

Γ ⊢ t ▷ T Γ ⊢ I @i ▷ Π(x : X @i )(y : Y @i ), □ l @i Ind Γ ⊢ c @i k ▷ Π(x : X @i )(y : Y k @i ), I @i x u @i k Cons Γ ⊢ s ▷ I I @i ′ a b Γ ⊢ p k ◁ X k [x := p] Γ, y : Y @i [x := p], z : I @i p y ⊢ P ▷ □ □ j I @i ′ a b ⪯ I @i p b Γ, y : Y k @i [x := p] ⊢ t k ◁ P [z := c @i k p y][y := u k @i ] Γ ⊢ match s in(I, i, p) return P with[t] ▷ P [z := s][y := b] Match Γ ⊢ T ▷ □ □ i Γ, f : T ⊢ t ◁ T guard condition Γ ⊢ fix f : T := t ▷ T Fix Γ ⊢ t ▷ I T Γ ⊢ t ▷ T T ⇝ I a b Γ ⊢ t ▷ I I a b
The two rules Ind, Cons are similar to those for variables, with the types pulled out of a global environment -not represented in our rules -rather than of the context. In particular, this presentation completely fixes the universe levels of the arguments. In rule Fix, the type of the fixpoint is checked to be well-formed, and then the body is checked against it. The guard condition, although complex, does not vary between the directed and undirected systems, and we thus do not dwell on it. The formalised version of this rule is complicated by the need to consider mutual (co-)fixpoints, but follows the same pattern.

Last but not least, Match follows the same structure as in Figures 4 and5: first, the type of the scrutinee is inferred, then the predicate is verified to be a type and finally the branches are checked. An important point is how much information can be retrieved from the scrutinee s. Indeed, the universe levels i and the parameters p used to build the context in which the predicate P and branches t are typed are stored in the match constructor. For cumulative inductive types, this is crucial to retain equivalence between the undirected and bidirectional system, and wrongly building the context from the type inferred for the scrutinee led to the bug we discovered. The idea is that the match construction might need to be typed "higher" than the type of inferred for s to be able to type P and t. Subsequently, a cumulativity check not appearing in the examples above is needed to ensure that the scrutinee checks against the type constructed using i and p. In contrast with parameters, the inferred indices b can safely be used in the return type, but proving this is the most subtle part of the correctness proof.

The formalisation

Let us now go over the formalisation file by file.

BDEnvironmentTyping.v & BDTyping.v

The first file refines a few definitions on contexts from EnvironmentTyping.v in order to account for the difference between checking and constrained inference. We expect this to eventually replace the less precise definitions.

The second contains the definition of the bidirectional type system as a mutually defined inductive type whose main part is infering. The best way to understand this inductive is probably to compare it with typing, the inductive predicate for undirected typing.

We then go on to proving by hand a custom induction principle, by first introducing a notion of size of a derivation. This induction principle is not as strong as we might expect, as it does not provide the extra induction hypothesis on context and type that would go with McBride's discipline. We did not try to go and prove such a strong induction principle, as we did not need it. Instead, reflecting the discipline in the choice of the predicates proven by induction was enough. But the main reason was that proving such an induction principle effectively corresponds to an inline proof of validity, a property that required quite an important amount of work to get. We still conjecture that such a strong induction principle should be provable, by reproducing some of the lemmas on the undirected typing, with extra care taken to the size of the obtained typing derivations, so as to be able to use e.g. substitutivity of typing together with an induction hypothesis.

BDToPCUIC.v & BDFromPCUIC.v

The next two files prove the equivalence between both type system. Correctness (akin to Theorem 2) is infering_typing for inference and the following theorems for the other judgements. Completeness (akin to Theorem 6) is theorem typing_infering.

The bulk of both proofs is an induction on typing derivation whose most challenging part is the handling of the case constructor, especially the subtle issues around indices described in Section 3.2. Similarly to Section 2, correctness relies on the strong properties of validity and subject reduction to reconstruct missing premises, while completeness mostly requires transitivity of conversion and confluence of reduction.

BDUnique.v This last file contains the proofs of Proposition 7 -uniqueness_inferredand Proposition 8 -principal_type. Apart from some lemmas on conversion that were only proved for cumulativity in MetaCoq, the induction itself is quite straightforward thanks to the bidirectional structure.

4

Beyond PCUIC

The use of our bidirectional structure is not limited to CIC or PCUIC. On the contrary, we found it crucial to have such a bidirectional type system when designing a gradual extension to CIC [START_REF] Lennon-Bertrand | Gradualizing the calculus of inductive constructions[END_REF], for multiple reasons we try and detail below. But let us first give a bit of context about this extension. The aim was to adapt the ideas of gradual typing [START_REF] Siek | Refined criteria for gradual typing[END_REF] to CIC. Gradual typing aims at incorporating some level of dynamic typing into a static typing discipline. To do so, a new type constructor ? is introduced to represent dynamic type information. At typing time, this ? should be seen as a wildcard that represents "any type" that is to be treated optimistically. In particular, ? should be considered convertible to any type. Conversion is thus replaced by a new relation, called consistency, that corresponds to this intuition. In effect it behaves somewhat similarly to unification, with each ? corresponding to a unification variable. This means in particular that consistency is not transitive, as if it were it would be useless: since any type T is consistent with ?, if consistency were transitive any two types would be related.

Localized computation

The free-standing conversion rule Conv is powerful, but sometimes too much.

This was our first use for the bidirectional structure. Indeed, multiple uses of a consistency in a row would have allowed to change the type of a term to any other arbitrary type by going through ? using two conversion rules in a row. Thus, any term would have been typable! Being able to use the conversion rule unrestricted was too much. Instead, the bidirectional system enforces a more localized use of conversion: only once, at the interface between inference and checking. This restriction was enough to make the conversion rule meaningful again.

More generally, since the equivalence between the undirected and directed variants relies on the properties listed in Proposition 1, when one of these fails the equivalence is endangered. When one envisons a system where this would be the case, the bidirectional approach might be worth considering, as it could stay viable while its undirected counterpart might not.

Modes for the conversion rule

The observation made in Section 2.2 that the unique Conv rule serves two different roles, which is clarified by the separation between checking and constrained inference, is an important one when toying with computation. Indeed, those two different aspects must be accounted for if one wishes to modify conversion and/or reduction. In particular, modifying the definition of conversion without accounting for the specific role of reduction would make rules for checking and constrained inference come out of sync, bringing trouble down the road.

Taking again the example of [START_REF] Lennon-Bertrand | Gradualizing the calculus of inductive constructions[END_REF], the Check is modified by directly replacing conversion with the consistency relation usual in gradual typing. But this is not enough, because constrained inference must be handled as well. This is done by supplementing rule Sort-Inf by another rule to treat the case when the inferred type reduces to the wildcard ?, that can be used as a type -with some care taken. The same happens for all constrained inference rules.

Bidirectional elaboration

In works such as [START_REF] Saïbi | Typing algorithm in type theory with inheritance[END_REF][START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF][START_REF] Lennon-Bertrand | Gradualizing the calculus of inductive constructions[END_REF], the procedure described is not typing but rather elaboration: the subject of the derivation t is in a kind of source syntax and the aim is not only to inspect t, but also to output a corresponding t ′ in another target syntax. The term t ′ is a more precise account of term t, for instance with solved meta-variables, inserted coercions, and so on. The bidirectional structure readily adapts to those settings, with the extra term t ′ simply considered as an output of all judgements. As such, McBride's discipline as described in Section 2.2 demands that when, in a context Γ, the subject t elaborates to t ′ while inferring type T , we should have Γ ⊢ t ′ : T -and similarly for all other typing judgements. Having all rules locally preserve this invariant ensures that elaborated terms are always well-typed.

5

Related work

Constrained inference

Traces of constrained inference in diverse seemingly ad-hoc workarounds can be found in various works around typing for CIC, illustrating that this notion, although overlooked, is of interest.

In [START_REF] Pollack | Typechecking in Pure Type Systems[END_REF], Γ ⊢ t : T is used for what we write Γ ⊢ t ▷ T , but another judgment written Γ ⊢ t :≥ T and denoting type inference followed by reduction is used to effectively inline the two hypothesis of our constrained inference rules. Checking is similarly inlined.

Saïbi [START_REF] Saïbi | Typing algorithm in type theory with inheritance[END_REF] describes an elaboration mechanism inserting coercions between types. Those are inserted primarily in checking, when both types are known. However he acknowledges the presence of two special classes to handle the need to cast a term to a sort or a function type without more informations, exactly in the places where we resort to constrained inference rather than checking.

More recently, Sozeau [START_REF] Sozeau | Subset coercions in coq[END_REF] describes a system where conversion is augmented to handle coercion between subset types. Again, Γ ⊢ t : T is used for inference, and the other judgments are inlined. Of interest is the fact that reduction is not enough to perform constrained inference, because type head constructors can be hidden by the subset construction: a term of subset type such as {f : N → N | f 0 = 0} should be usable as a function of type N → N. An erasure procedure is therefore required on top of reduction to remove subset types in the places where we use constrained inference.

Abel and Coquand [START_REF] Abel | Verifying a semantic βη-conversion test for Martin-Löf type theory[END_REF] use a judgement written ∆ ⊢ V δ ⇑ Set ⇝ i, where a type V is checked to be well-formed, but with its exact level i free. This corresponds very closely to our use of ▷ □ .

Traces can also be found in the description of Matita's elaboration algorithm [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF]. Indeed, the presence of meta-variables on top of coercions makes it even clearer that specific treatment of what we identified as constrained inference is required. The authors introduce a special judgement they call type-level enforcing corresponding to our ▷ □ judgement. As for ▷ Π , they have two rules to apply a function, one where its inferred type reduces to a product, corresponding to Prod-Inf, and another one to handle the case when the inferred type instead reduces to a meta-variable. As Saïbi, they also need a special case for coercions of terms in function and type position. However, their solution is different. They rely on unification, which is available in their setting, to introduce new meta-variables for the domain and codomain of a product type whenever needed. For ▷ □ though this solution is not viable, as one would need a kind of universe meta-variable. Instead, they rely on backtracking to test multiple possible universe choices.

Finally, we have already mentioned [START_REF] Lennon-Bertrand | Gradualizing the calculus of inductive constructions[END_REF] in Section 4, where the bidirectional structure is crucial in describing a gradual extension to CIC. In particular, and similarly to what happens with meta-variables in [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF], all constrained inference rules are duplicated: there is one rule when the head constructor is the desired one, and a second one to handle the gradual wildcard.

Completeness

Quite a few articles tackle the problem of bidirectional typing in a setting with an untypedso called Curry-style -abstraction. This is the case of early work by Coquand [START_REF] Coquand | An algorithm for type-checking dependent types[END_REF], the type system of Agda as described in [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF], the systems considered by Abel in many of his papers [START_REF] Abel | Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs[END_REF][START_REF] Abel | Verifying a semantic βη-conversion test for Martin-Löf type theory[END_REF][START_REF] Abel | A partial type checking algorithm for type:type[END_REF][START_REF] Abel | Decidability of conversion for type theory in type theory[END_REF], and much of the work of McBride [START_REF] Mcbride | I got plenty o' nuttin[END_REF][START_REF] Mcbride | Basics of bidirectionalism[END_REF][START_REF] Mcbride | Check the box! In 25[END_REF] on the topic. In such systems, C V I T 2 0 1 6 23:16 Complete Bidirectional Typing for the Calculus of Inductive Constructions λ-abstractions can only be checked against a given type, but cannot infer one, so that only terms with no β-redexes are typable. Norell [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF] argues that such β-redexes are uncommon in real-life programs, so that being unable to type them is not a strong limitation in practice. To circumvent this problem, McBride also adds the possibility of typing annotations to retain the typability of a term during reduction.

While this approach is adapted to programming languages, where the emphasis is on lightweight syntax, it is not tenable for a proof assistant kernel, where all valid terms should be accepted. Indeed, debugging a proof that is rejected because the kernel fails to accept a perfectly well-typed term the user never wrote -as most proofs are generated rather than written directly -is simply not an option.

In a setting with typed -Church-style -abstraction, if one wishes to give the possibility for seemingly untyped abstraction, another mechanism has to be resorted to, typically meta-variables. This is what is done in Matita [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF], where the authors combine a rule similar to Abs -where the type of an abstraction is inferred -with another one, similar to the Curry-style one -where abstraction is checked -looking like this:

T ⇝ * Π x : A ′ .B Γ ⊢ A ▷ □ □ i A ≡ A ′ Γ, x : A ⊢ t ◁ B Γ ⊢ λ x : A.t ◁ T
While such a rule would make a simple system such as that of Section 2 "over-complete", it is a useful addition to enable information from checking to be propagated upwards in the derivation. This is crucial in systems where completeness is lost, such as Matita's elaboration. Similar rules are described in [START_REF] Asperti | A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions[END_REF] for let-bindings and constructors of inductive types.

Although only few authors consider the problem of a complete bidirectional algorithm for type-checking dependent types, we are not the first to attack it. Already Pollack [START_REF] Pollack | Typechecking in Pure Type Systems[END_REF] does, and the completeness proof for CCω of Section 2 is very close to one given in his article. Another proof of completeness for a more complex CIC-like system can be found in [START_REF] Sozeau | Subset coercions in coq[END_REF]. None of those however tackle as we do the whole complexity of PCUIC.

Inputs and outputs

We already credited the discipline we adopt on well-formedness of inputs and outputs to McBride [START_REF] Mcbride | Basics of bidirectionalism[END_REF][START_REF] Mcbride | Check the box! In 25[END_REF]. A similar idea has also appeared independently in [9]. Bauer and his co-authors introduce the notions of a (weakly) presuppositive type theory [9, Def. 5.6] and of well-presented premise-family and rule-boundary [9, Def. 6.16 and 6.17] to describe a discipline similar to ours, using what they call the boundary of a judgment as the equivalent of our inputs and outputs. Due to their setting being undirected, this is however more restrictive, because they are not able to distinguish inputs from outputs and thus cannot relax their condition to only demand inputs to be well-formed but not outputs.

Conclusion

We have described a judgmental presentation of the bidirectional structure of typing algorithms in the setting of dependent types. In particular, we identified a new family of judgements we called constrained inference. Those have no counterpart in the non-dependent setting, as they result from a choice of modes for the conversion rule, which is specific to the dependent setting. We proved our bidirectional presentation equivalent to an undirected one, both on paper on the simple case of CCω, and formally in the much more complex and realistic setting of PCUIC. Finally, we gave various arguments for the usefulness of our presentation as a way to ease proofs, an intermediate between undirected type-systems and typing algorithms, a solid basis to design new type systems, and a tool to re-interpret previous work on type systems in a clearer way.

Regarding future work, a type-checking algorithm is already part of MetaCoq, and we should be able to use our bidirectional type system to give a pleasant completeness proof by separating the concerns pertaining to bidirectionality from the algorithmic problems, such as implementation of an efficient conversion check or proof of termination. More broadly, bidirectional type systems should be an interesting tool in the feat of incorporating in proof assistants features that have been satisfactorily investigated on the theoretical level while keeping a complete and correct kernel, avoiding the pitfall of cumulative type's incomplete implementation in Coq. A first step would be to investigate the discrepancies between the two kinds of presentations of inductive types Section 3, and in particular if all informations currently stored in the match node are really needed or if a more concise presentation can be given. But we could go further and study how to handle cubical type theory [START_REF] Vezzosi | Cubical Agda: A dependently typed programming language with univalence and higher inductive types[END_REF], rewrite rules [START_REF] Cockx | The Taming of the Rew: A Type Theory with Computational Assumptions[END_REF], setoid type theory [START_REF] Altenkirch | Setoid type theory -a syntactic translation[END_REF], exceptional type theory [START_REF] Pédrot | Failure is not an option an exceptional type theory[END_REF], η-conversion. . . There might also be an interesting link to make with the current work on normalization by evaluation [START_REF] Abel | Towards normalization by evaluation for the βη-calculus of constructions[END_REF] as an alternative to weak-head reduction for constrained inference. Finally, we hope that our methodology will be adapted as a base for other theoretical investigations. As a way to ease this adoption, studying it in a general setting such as that of [9] might be a strong argument for adoption.

Figure 1

 1 Figure 1 Undirected typing for CCω

Figure 2

 2 Figure 2 Bidirectional typing for CCω

Figure 4

 4 Figure 4 Bidirectional sum type

Figure 6

 6 Figure 6 Bidirectional inductive type -PCUIC style

  ). The type system CCω as just described enjoys the following properties: Confluence Reduction ⇝ is confluent. As a direct consequence, two terms are convertible just when they have a common reduct: t ≡ u if and only if there exists t ′ such that t ⇝ * t ′ and u ⇝ * t ′ . Transitivity Conversion is transitive. Subject reduction If Γ ⊢ t : T and t ⇝ t ′ then Γ ⊢ t ′ : T . Validity If Γ ⊢ t : T then T is well-formed, e.g. there exists some i such that Γ ⊢ T : □ i .

We call anything related to the Γ ⊢ t : T judgement undirected by contrast with the bidirectional typing.

We chose ▷ and ◁ rather than the more usual ⇒ and ⇐ to avoid confusion with implication on paper, and with the Coq notation for functions in the development.

A completeness bug in that algorithm -also present in the Coq kernel -has already been found, see Section 3 for details.

A version frozen as described in this article is available in the following git branch: https://github. com/MevenBertrand/metacoq/tree/itp-artefact.

Inference: Γ ⊢ t ▷ T Γ ⊢ □ i ▷ □ i+1 Sort (x : T ) ∈ Γ Γ ⊢ x ▷ T Var Γ ⊢ A ▷ □ □ i Γ, x : A ⊢ B ▷ □ □ j Γ ⊢ Π x : A.B ▷ □ i∨j Prod Γ ⊢ A ▷ □ □ i Γ, x : A ⊢ t ▷ B Γ ⊢ λ x : A.t ▷ Π x : A.B Abs Γ ⊢ t ▷ Π Π x : A.B Γ ⊢ u ◁ A Γ ⊢ t u ▷ B[x := u] App Checking: Γ ⊢ t ◁ T Γ ⊢ t ▷ T ′ T ′ ≡ T Γ ⊢ t ◁ T Check Constrained inference: Γ ⊢ t ▷ h T Γ ⊢ t ▷ T T ⇝ * □ i

The precise issue in the kernel is described in this git issue: https://github.com/coq/coq/issues/ 13495.

Γ ⊢ A : □ i Γ, x : A ⊢ B : □ j Γ ⊢ Σ x : A.B : □ i∨j Σ-type Γ ⊢ A : □ i Γ, x : A ⊢ B : □ j Γ ⊢ a : A Γ ⊢ b : B[x := a] Γ ⊢ (a, b) A,x.B : Σ x : A.B Σ-cons Γ, z : Σ x : A.B ⊢ P : □ i Γ, x : A, y : B ⊢ b : P [z := (x, y)] Γ ⊢ s : Σ x : A.B Γ ⊢ rec Σ (z.P, x.y.p, s) : P [z := s] Σ-rec Figure 3 Undirected sum type Γ ⊢ t ▷ T Γ ⊢ A ▷ □ □ i Γ, x : A ⊢ B ▷ □ □ j Γ ⊢ Σ x : A.B ▷ □ i∨j Σ-type Γ ⊢ A ▷ □ □ i Γ, x : A ⊢ B ▷ □ □ j Γ ⊢ a ◁ A Γ ⊢ b ◁ B[x := a] Γ ⊢ (a, b) A,x.B ▷ Σ x : A.B Σ-cons Γ ⊢ s ▷ Σ Σ x : A.B Γ, z : Σ x : A.B ⊢ P ▷ □ □ i Γ, x : A, y : B ⊢ b ◁ P [z := (x, y)]Γ ⊢ rec Σ (z.P, x.y.b, s) ▷ P [z := s] Σ-rec

choose for the premises. For Σ-type and Σ-cons this is straightforward: when the type appears in the conclusion, use checking, otherwise (constrained) inference. The case of the destructors is somewhat more complex. Handling the subterms of the destructor in the order in which they usually appear (predicate, branches and finally scrutinee) is not possible, as the parameters of the inductive type are needed to construct the context in which the predicate is typed. However those parameters can be inferred from the scrutinee. Thus, a type for the scrutinee is first obtained using a new constrained inference judgment, forcing the inferred type to be a Σ-type, but leaving its parameters free. Next, the obtained arguments can be used to construct the context to type the predicate. Finally, once the predicate is known to be well-formed, it can be used to type-check the branch.Γ ⊢ t ▷ T Γ ⊢ N ▷ □ 0 Γ ⊢ 0 ▷ N Γ ⊢ n ◁ N Γ ⊢ S(n) ▷ N Γ ⊢ s ▷ N N Γ, z : N ⊢ P ▷ □ □ i Γ ⊢ b 0 ◁ P [z := 0] Γ, x : N, p : P [z := x] ⊢ b S ◁ P [z := S(x)] Γ ⊢ rec N (z.P, b 0 , x.p.b S , s) ▷ P [z := s] Γ ⊢ A ▷ □ □ i Γ ⊢ a ◁ A Γ ⊢ a ′ ◁ A Γ ⊢ Id A a a ′ ▷ □ i Γ ⊢ A ▷ □ □ i Γ ⊢ a ◁ A Γ ⊢ refl A a ▷ Id A a a Γ ⊢ s ▷ Id A a a ′ Γ, x : A, z : Id A a x ⊢ P ▷ □ □ i Γ ⊢b ◁ P [z := Id A a a][x := a] Γ ⊢ rec Id (x.z.P, b, s) ▷ P [z := s][x := a ′ ] Γ ⊢ t ▷ h T Γ ⊢ t ▷ T T ⇝ * N

https://github.com/MevenBertrand/metacoq/


Precision Close-to-Carrier Phase Noise Simulation of BAW Oscillators

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

I. I

M  commercial electronic simulators are neces- sary tools for oscillator analysis [START_REF] Rhea | Oscillator Design and Computer Simulation[END_REF]. Such engineering tools, including Advanced Design System (ADS) from Agilent Technologies, Santa Clara, CA, cover the whole oscillator design procedure, including phase noise analysis. They can also clarify some intrinsic oscillator processes [START_REF] Quere | Low phase noise oscillator modeling in a system environment[END_REF]. Indeed, not all important oscillator parameters are available for direct measurements. For example, the true phase noise of the oscillator loop alone is difficult to measure and partially hidden by the output-amplifier noise. Thus, the influence of the different loop components, including the resonator itself, on the resulting noise spectrum is not clearly distinguishable. So, in dielectric resonator oscillators (10-100 GHz) the active component noise dominates the resonator noise. For oscillators using acoustic resonators [bulk acoustic wave (BAW) up to 100 MHz, surface acoustic wave (SAW), and film bulk acoustic resonators (FBAR) up to 10 GHz], resonator noise cannot be ignored, as is usually done. At best, it is added manually by the designer after simulation. For example, for BAW [START_REF] Sthal | About quartz crystal resonator noise: Recent study[END_REF], [START_REF] Rubiola | Flicker noise measurement of HF quartz resonators[END_REF] and FBAR [START_REF] Gribaldo | Experimental study of phase noise in FBAR resonators[END_REF], resonator-caused noises are measured, but not included in resonator simulations. Obviously, this simplification reduces the validity of the close-to-carrier simulation results. In this paper, the noise of ultra-stable RF quartz crystal oscillators is covered. The resonator noise model, ignoring the noise origins (which are still not clearly identified [START_REF] Kroupa | Theory of 1/f noise-A new approach[END_REF]), is developed in the first section. This is followed in the next section by the implementation of the resonator model in oscillator simulation to determine the impact on the oscillator noise spectrum.

II. Q R P N M

To get a realistic phase noise model of the resonator, recent precision phase noise measurements have been used [START_REF] Sthal | About quartz crystal resonator noise: Recent study[END_REF], [START_REF] Rubiola | Flicker noise measurement of HF quartz resonators[END_REF]. Measurements are made with an interferometric bench. For all resonators, a double-oven temperature control (having the same quality as that in oscillators) is implemented [START_REF] Sthal | Thermal characterization of crystal ovens used in phase noise measurement system[END_REF]. The typical phase noise spectrum of a quartz crystal resonator consists of the following four zones: 1) f -2 is a random-walk process caused by remaining temperature fluctuations. Even though it is not usually taken into account, it always exists [START_REF] Gagnepain | Excess noise in quartz crystal resonators[END_REF], [START_REF] Noguchi | 1/f frequency fluctuation of a quartz crystal oscillator and temperature fluctuation[END_REF] and can limit the phase noise performances at low frequencies. 2) f -1 is the intrinsic crystal noise within its bandwidth [START_REF] Shmaliy | The noise conversion method for oscillatory systems[END_REF]- [START_REF] Planat | 1/f noise in quartz crystal resonator in relation with losses and frequency dispersion[END_REF]; 3) f -3 is the intrinsic crystal noise outside the bandwidth; and 4) f 0 is the noise floor of the measurement bench. For an unambiguous description of the resonator noise, three spectrum parameters can be extracted: 1) f T is the corner frequency between f -2 and f -1 regions; 2) the phase noise level at 1 Hz; and 3) f L is the corner frequency between f -1 and f -3 regions.

This type of measured spectrum has been implemented using the circuit shown in Fig. 1. The quartz crystal resonator is modeled with its conventional RLC branch (doubled here because a parasitic mode is close to the working mode for doubly-rotated crystal cuts) and its parallel parasitic capacitor, but including an additive current-controlled inductance, whose value depends on the current of two noise sources SRC1 and SRC2. Because the device resonance frequency depends not only on parameters of the motional branches but also on the variable inductor, the resulting system has a parametric noise with a spectral density proportional to the squared current of the noise sources. Thus, the first source with a power spectral density proportional to f -1/2 is used to represent f -1 and f -3 noises for medium and high Fourier frequencies. The second source, with a PSD proportional to f -1 , gives an f -2 slope for low frequencies. The parameters of the sources (I_Noise, which is the noise current magnitude per hertz 1/2 ) are adjusted to simulate the phase noise of real 10-MHz doubly-rotated BVA-type resonators measured at the FEMTO-ST Institute. Fig. 2 presents the simulation results, i.e., the phase noise PSDs of the signal at the node out (see Fig. 1), which reproduce the measurement data [START_REF] Sthal | About quartz crystal resonator noise: Recent study[END_REF], [START_REF] Rubiola | Flicker noise measurement of HF quartz resonators[END_REF]. Noise spectra of two different samples are shown to demonstrate that all resonator samples have different parameters and noise characteristics, even if they are of the same type and made by the same manufacturer. It is also important to note that the quality of the temperature controller influences the recorded noise in the f -2 region.

Moreover, as mentioned previously, the resonator model consists of two resonance branches that model both the desired and spurious crystal modes. For example, an LDcut quartz crystal resonator designed to work at 10 MHz

Precision Close-to-Carrier Phase Noise Simulation of BAW Oscillators

Maxim Goryachev and Serge Galliou

The authors are with the Time and Frequency department of the Franche-Comté Electronique, Mécanique, Thermique et Optique-Sciences et Technologies (FEMTO-ST) Institute, Besançon, France (e-mail: maxim.goryachev@femto-st.fr).

on its C-mode has a parasitic resonance at 10.7 MHz (Bmode). This means that the spurious mode is inside the usual analysis band (which is defined here as close-to-carrier: typically 1 MHz from the carrier at 10 MHz) of the working mode. The parasitic branch does not have a considerable effect on the close-to-carrier phase noise, but it is used in simulations to verify that the oscillator operates on the expected mode. In some cases, additional elements are required to cancel the parasitic effects (see Fig. 3).

It should be noted that using a current-controlled inductance combined with current noise sources is not the only method available to modulate noise at the resonator. For example, a voltage-controlled capacitance across Cx1, linked with voltage noise sources, is also relevant [START_REF] Howard | Simulate oscillator phase noise[END_REF]. In this case, the noise voltage magnitude per hertz 1/2 of the sources has to be adjusted accordingly.

III. O S

The described model has been implemented for simulation of an actual 10 MHz ultra-stable quartz crystal oscillator designed at FEMTO-ST (see Fig. 3). This unit has a one-transistor Colpitts-type oscillation loop (the sustaining amplifier + the resonator), and a common-collector stage followed by an output cascode amplifier (i.e., two buffer stages are used to isolate the loop from the load, to match impedances and to purify the output signal).

Fig. 4 shows the simulated phase noise PSD of the oscillator in different configurations with or without crystal noise, and before or after the buffer stages to determine the influence of the various oscillator parts. In addition to the resonator noise, thermal noise sources of all component and transistor flicker noise sources are enabled. From a practical point of view, the simulated curves correspond to actual measurements. The oscillator phase noise spectrum consists of f -4 , f -3 , f -1 , and f 0 noises [14]- [START_REF] Norton | Advanced technology oscillator for small spacecraft[END_REF], which can also easily be identified in a typical RF oscillator phase noise spectrum. The f -4 spectrum slope is due to the Leeson effect [START_REF] Leeson | A simple model of feed back oscillator noise spectrum[END_REF] of the f -2 resonator noise. f -3 corresponds to the transformed f -1 resonator noise. The flicker and white noises of curve (1) are dominated by the noise of the output buffers, though the flicker and white noises of curve (2) are only due to the sustaining amplifier and resonator phase noise.

The first observation from these results is that white and flicker noise of the buffers overlap these types of noises of the oscillating loop. This leads to a decrease of the corner frequency between f -1 and f -3 PSD slopes () , f c ′ which can be taken for the Leeson frequency by mistake [START_REF] Rubiola | On the 1/f frequency noise in ultrastable quartz oscillators[END_REF], [START_REF] Rubiola | Phase Noise and Frequency Stability in Oscillators[END_REF]. This error leads to an overly high estimate of the loaded quality factor. Actually, the Leeson effect takes place inside the oscillating loop, so the true Leeson frequency is the corner frequency between the f -1 and f -3 noises of the curve (2), or f c ′′, which is hidden by the buffer noise. In conclusion, f c ′ would give unjustified high values of the loaded quality factor. The Leeson frequency could also be found from curve [START_REF] Sthal | About quartz crystal resonator noise: Recent study[END_REF], as the intersection between f -2 and f 0 noise slopes, because the corner frequency of the sustaining amplifier is lower. Second, as can also be concluded by comparing curves (1) and ( 3), the phase noise close to the carrier (both f -3 Fig. 3. Advanced Design System schematics of the modeled Colpitts oscillator with two output buffers. Note that capacitor C3 and inductor L1 are used to suppress the spurious mode (i.e., the B mode here). Fig. 4. PSDs of oscillator phase noise representing an actual 10-MHz oscillator in different configurations: (1) the oscillator PSD after the buffers, i.e., the PSD measured in reality, (2) the PSD before the buffers (also marked as a black square), (3) the PSD before the buffers without the resonator noise. Three generalized noise sources are present: ψ 1 , resonator; ψ 2 , sustaining amplifier; ψ 3 , buffer phase noises. and f -4 ) is predominantly due to the resonator instability. Thus, for reliable ultra-stable oscillator noise simulation, the resonator phase noise model has to be included in the loop. The importance of the f -4 noise depends on the quality of the temperature control in the ovenized crystal oscillator as well as in the measurement bench of resonator noise. So, neglecting it (as is usually done both in measurements and modeling) leads to unrealistic simulation results close to the carrier. It should be noted that resonator aging can hide the effect of long-term temperature fluctuations, depending on their relative weights.

IV. C

The proposed resonator noise model is sufficient for presimulations of ultra-stable quartz oscillators. Simulations are in good agreement with both resonator and oscillator phase noise measurements. This model implements remaining quartz crystal parametric noise, both caused by temperature and intrinsic fluctuations. This approach provides reliable results of phase noise close to the carrier. Also, the implementation of the f -2 resonator noise is necessary, because it limits the system performances in many applications. Our simulations confirm that actual oscillator phase noise performance close to the carrier is a strong function of the quartz-crystal resonator noise. In addition, far from the carrier (f -1 and f 0 noises) the system stability is mainly limited by the buffer amplifying stages. The suggested approach may be very helpful for computer-aided ultra-stable crystal oscillator design.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Quartz resonator noise modeling circuit. Noise sources SRC1 and SRC2 have spectral noise densities proportional to f -1/2 and f -1 correspondingly.

A

The authors thank Prof. E. Rubiola (FEMTO-ST, Besançon, France), Prof. P. A. Rolland (IEMN, Lille, France), J. Chauvin (Oscilloquartz SA, Neuchâtel, Switzerland), P. Vincent (CEA-LETI, Grenoble, France) for their fruitful discussions as well as the anonymous reviewers for their pertinent comments. R