Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

Andreas Abel,^{1} Thierry Coquand,^{2} and Peter Dybjer^{2}^{⋆}

1 Department of Computer Science, Ludwig-Maximilians-University, Munich

                     abel@tcs.ifi.lmu.de

2 Department of Computer Science, Chalmers University of Technology

                coquand,peterd@cs.chalmers.se

Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of Coquand’s algorithm for checking the βη-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of contextual reification and strong semantic equality. The algorithm is part of a bi-directional type checking algorithm which checks whether a normal term has a certain semantic type, a technique used in the proof assistants Agda and Epigram. We work with an abstract notion of semantic domain in order to accommodate a variety of possible implementation techniques, such as normal forms, weak head normal forms, closures, and compiled code. Our aim is to get closer than previous work to verifying the type-checking algorithms which are actually used in practice.

1 Introduction

Proof assistants based on dependent type theory have now been around for about 25 years. The most prominent representative, Coq [INR07], has become a mature system. It can now be used for larger scale program development and verification, as Leroy’s ongoing implementation of a verified compiler shows [Ler06]. Functional programmers have also become more and more interested in using dependent types to ensure program and data structure invariants. New functional languages with dependent types such as Agda 2 [Nor07] and Epigram 2 [CAM07] enjoy increasing popularity.

Although many questions about properties of dependent type theories have been settled in the 1990s, some problems are still waiting for a satisfactory solution. One example is the treatment of equality in implementations of proof assistants. When we check that a dependently typed program is well-typed,

⋆ Research partially supported by the EU coordination action TYPES (510996) and the project TLCA of Vetenskapsrådet.

we may need to test whether two types are definitionally equal (convertible). Although it is of course impossible for a system to recognize all semantically equal types, a user will feel more comfortable if it can recognize as many as possible. Whenever it fails the user has to resort to proving manually that the types are equal. This has the additional drawback of introducing proof-objects for these equalities. In recent years there has therefore been a move from βequality (computational equality) to the stronger βη-equality (computational and extensional equality).

Recently, algorithms for testing βη-equality have been formulated and verified by the authors both for an untyped notion of conversion [AAD07] and for typed equality judgements [ACD07]. These algorithms use the technique of normalization by evaluation (NbE). However, the algorithms used by proof assistants such as Agda and Epigram [CAM07], use Coquand’s βη-conversion test for semantic ”values”, and do not employ the NbE-technique of the abovementioned papers. Moreover, there is a gap between algorithms on paper and their actual implementation. Proofs on paper are often informal about the treatment of variable names, and they tend to represent values as pieces of abstract syntax. Besides Pollack’s [Pol94], Coquand’s algorithm [Coq96] is a notable exception: values are represented as closures, and the algorithm explicitly deals with α-equivalence by replacing variables by numbers (de Bruijn levels).

We here continue the work of the second author and verify an implementation of the βη-conversion test close to the one used in practice. In particular:

– Equality is checked incrementally, and not by full normalization followed by a test for syntactical identity.

– The representation of values is abstract. We only require that they form a syntactical applicative structure. In this way, several possible implementations, such as normal forms, closures, and abstract machine code, are covered by our verification.

– The verification approach is extensible: Although we only spell out the proofs for a core of type theory with predicative universes, our development extends to richer languages. We can for example include a unit type, Σ types, proof irrelevance, and inductive types with large eliminations.

Overview. In Sec. 2 we present an abstract type and equality checking algorithm, which only assumes that the domain of values forms a syntactical applicative structure. In Sec. 3 inference rules for typing and type equality are given for a version of Martin-Löf type theory with explicit substitutions. An outline of the verification is given in Sec. 4 together with a definition of contextual reification, our main tool for verification. Using contextual reification, an alternative equality test can be formulated, which is shown complete in Sec. 5, by construction of a Kripke model, and proven sound in Sec. 6 via a Kripke logical relation. Completeness of the original algorithm then follows easily in Sec. 7. For soundness, we have to introduce a Kripke logical relation and the concept of strong semantic equality in Sec. 8. In Sec. 9 we discuss the problem of termination of the equality algorithm, which remains open. More proof details can be found in the accompanying technical report [ACD08].

2 Semantic Type and Equality Checking

We consider dependently typed programs p to be given as lists of the form

x_{0} : V_{0} = v_{0}
⋮
x_{n−1} : V_{n−1} = v_{n−1}

where x_{i} is a identifier, V_{i} its type, and v_{i} the definition of x_{i} for i < n. (Typically x_{i} will be a function identifier and v_{i} the function definition.) The identifiers are not defined simultaneously (which would correspond to mutual recursion), but one-after-another. Hence, V_{i} and v_{i} may only refer to previously defined identifiers x_{j} for j < i. A program is type correct if each V_{i} is a well-formed type and each v_{i} is a term of type V_{i}. To establish this, the type and definition of the previously defined identifiers may be used. It is reasonable to assume and easy to check that the global identifiers x_{i} are all distinct; global declarations should not be shadowed. However, local shadowing is allowed; the identifiers x_{i} may be reused in some of the v_{j} or V_{j}. Our type checking algorithm handles shadowing correctly without any informal use of α-conversion.

Dependent types need to be evaluated during type checking. Thus it is common to store them in evaluated form. Without going into further details now, let vρ (V ρ) denote the evaluation of term v (type V) in environment ρ. The environment maps already checked identifiers to their values. A typing context Δ maps already checked identifiers to their types (in evaluated form). Checking a program starts in an empty environment ρ_{0} and an empty typing context Δ_{0}. For i = 0, …, n − 1, we execute the following steps:

1. Check that V_{i} is a well-formed type in the current context Δ_{i}.

2. Evaluate V_{i} in the current environment: X_{i} = V_{i}ρ_{i}.

3. Check that v_{i} is of type X_{i} in the current context. This test is written Δ_{i} ⊢ v_{i} δ_{id} ⇑ X_{i}, where δ_{id} is the identity map on names.

4. Evaluate v_{i} and extend the current environment by binding x_{i} to the result: ρ_{i+1} = (ρ_{i}, x_{i} = v_{i}ρ_{i}).

5. Extend the current context: Δ_{i+1} = Δ, x_{i}:X_{i}.

The details of type checking depend on the language. We here show how to verify an algorithm for a core language with dependent function types and predicative universes. In the accompanying technical report [ACD08] we consider also natural numbers with primitive recursion. However, the algorithms and proofs in this work directly extend to dependent tuples (Σ and unit type).

2.1 Syntax

Expressions r, s, t are formed from variables x and constants c by application r s and function abstraction λxt. The types V_{i} and terms v_{i} of a program p ≡ (x_{i} :

V_{i} = v_{i})_{i} must be in normal form.

Var ∋ x, y, z  ::= …, x_{1}, x_{2}, …  variables
Const ∋ c  ::= Fun | Set_{i}  constants (i ∈ ℕ)
Exp ∋ r, s, t  ::= c | x | λxt | r s  expressions
Nf ∋ v, w, V, W ::= u | λxv | Fun V λxW | Set_{i} β-normal expressions
Ne ∋ u  ::= x | u v  neutral expressions

The set Var of variable identifiers contains, among others, the special variables x_{1}, x_{2}, … which are called de Bruijn levels. To aid the reader, we use the letters A, B, C, V, W for expressions which are to be understood as types and r, s, t, u, v, w for terms. Dependent function types, usually written Πx : A. B, are written Fun A λxB. When B does not depend on x we have a non-dependent function type and write A → B.

An expression like Fun A λxB is parsed as (Fun A) (λxB); application is leftassociative. To save on parentheses, we introduce the notation λx. t where the dot opens a parenthesis which closes as far to the right as syntactically possible. For instance λx. r s is short for λx (r s), whereas λxr s means (λxr) s.

The hello world program of dependent types, the polymorphic identity, becomes in our notation

id : Fun Set_{0} λA. A → A = λAλa a.

The predicative universes Set_{i} are types of types. A well-formed type V : Set_{i} lives in universe i and above. A universe Set_{i} lives in higher universes Set_{j}, j > i.

2.2 Values

In implementations of dependently typed languages, different representations of values have been chosen: Twelf [PS99] uses de Bruijn terms with explicit substitutions; Agda 2 [Nor07] de Bruijn terms in normal form; and Epigram 2 [CAM07] higher-order abstract syntax. Furthermore, the second author has suggested to use closures [Coq96]. In this article, we abstract over several possible representations, by considering a syntactical applicative structure with atoms.

Applicative structure with atoms. This is an applicative structure (D, · ) which includes all variables and constants as atoms (Var ∪ Const ⊆ D). Elements of D are denoted by d, e, f, X, Y, Z, E, F and called values or objects. Neutral values are given inductively by e, E ::= x | e · d. Neutral application is injective: If e · d = e′ · d′, then e = e′ and d = d′. Neutral values are distinct, for instance, x · d ≠ y · d′. We will sometimes write application as juxtaposition, especially in neutral and constructed values.

The constants Set_{i} are constructors of arity 0 and Fun is a constructor of arity 2. Constructors are injective, thus, Fun X F = Fun X′ F′ implies X = X′ and F = F′. Constructed values, i. e., of the form c d, are distinguished from each other and from neutral values. It is decidable whether an object is neutral, constructed, or neither. If an object is neutral, we can extract the head variable and the arguments, and similar for constructed objects.

Syntactical applicative structure with atoms. We enrich the applicative structure with an evaluation operation tρ ∈ D for expressions t ∈ Exp in an environment ρ : Var ⇀ D. Let ρ_{id} denote the identity environment. The following axioms must hold for evaluation.

eval-c  cρ = c
eval-var  xρ = ρ(x)
eval-fun-e (r s)ρ = rρ · sρ
app-fun (λxt)ρ · d = t(ρ, x=d)

An applicative structure which satisfies these equations is called a syntactical applicative structure (D, · , ). Barendregt [Bar84, 5.3.1.] adds a sanity condition that the evaluation of an expression may only depend on the valuations of its free variables, but we will not require it. All syntactical λ-models [BL84] [Bar84, 5.3.2.(ii)] are instances of syntactical applicative structures, yet they must additionally fulfill weak extensionality (ξ).

An instance: closures. There are applicative structures which are neither λmodels nor combinatory algebras, for example the representation of values by closures. Values are given by the grammar

\begin{aligned}D & ∋ & d & ::= & [λxt]ρ | e \\ & & e & ::= & c | x | e d \end{aligned}

where [λxt]ρ is a closure such that ρ provides a value for each free variable in λxt. Evaluation does not proceed under binders; it is given by the above axioms plus:

eval-fun-i (λxt)ρ = [λxt]ρ
app-ne  e · d = e d

Closures are a standard tool for building interpreters for λ-calculi; the second author has used them to implement a type checker [Coq96]. While for the soundness proof he requires weak extensionality in D, we will not; instead, extensionality of functions in Type Theory is proven via a Kripke model (Section 5).

2.3 Type Checking

In this section, we present a bidirectional type-checking algorithm [PT98] which checks a normal term against a type and infers the type of a normal expression. In the dependently typed setting, where types may contain computations, the principled approach is to keep types in evaluated form. During the course of type-checking we will have to evaluate terms (see rule inf-fun-e below). To avoid non-termination, it is crucial to only evaluate terms which have already been type checked.

We are ready to present the semantic type checking algorithm, where “semantic” refers to the fact that types are values in D and not type expressions. As usual we describe it using inference rules. These can be read as the clauses of logic programs and we specify the modes (input and output). Note that the modes are not part of the mathematical definition of the inductive judgements— they only describe how the judgements should be executed. Since the rules are deterministic, they also describe a functional implementation of type checking, which can be obtained mechanically from the rules.

In the following definitions δ ranges over special environments, renamings, which are finite maps from variables to de Bruijn levels. As before, tδ denotes the evaluation of t in environment δ.

Semantic (typing) contexts are given by the grammar Δ ::= ⋄ | Δ, x : X, where x ∉ dom(Δ). If (x: X) ∈ Δ then Δ(x) = X. We write x_{Δ} for the first de Bruijn level which is not used in Δ, x_{Δ+1} for the next one, etc.

Type checking algorithm. We define bidirectional type checking of normal terms and well-formedness checking of normal types by the following three judgements. Herein, Δ ∈ SemCxt, u ∈ Ne, v, V ∈ Nf, δ ∈ Var ⇀ Var, X ∈ D and i ∈ ℕ.

Δ ⊢ u δ ⇓ X  the type of neutral u is inferred as X
Δ ⊢ v δ ⇑ X  normal v checks against type X
Δ ⊢ V δ ⇑ Set ⇝ i  V is a well-formed type of inferred level i.

In all judgements we maintain the invariant that Δ assigns types to the free variables in X and Δ ∘ δ to the free variables in u, v, V.

Type inference Δ ⊢ u δ ⇓ X. (Inputs: Δ, u, δ. Output: type X of u or fail.)

inf-var \overline{Δ ⊢ x δ ⇓ Δ(xδ)}

inf-fun-e \frac{Δ ⊢ u δ ⇓ Fun XF  Δ ⊢ v δ ⇑ X}{Δ ⊢ (u v) δ ⇓ F · vδ}

The type of a variable x under renaming δ is just looked up in the context. When computing the type of an application u v from the type Fun XF of the function part we need to apply F to the evaluated argument part vδ (dependent function application). At this point, it is crucial that we have type-checked v already, otherwise the application F · vδ could diverge.

Type checking Δ ⊢ v δ ⇑ X. (Inputs: Δ, v, δ, X. Output: succeed or fail.)

chk-fun-i \frac{Δ, x_{Δ}:X ⊢ v (δ, x=x_{Δ}) ⇑ F · x_{Δ}}{Δ ⊢ (λxv) δ ⇑ Fun XF}

chk-set \frac{Δ ⊢ V δ ⇑ Set ⇝ i}{Δ ⊢ V δ ⇑ Set_{j}} i ≤ j

chk-inf \frac{Δ ⊢ u δ ⇓ X  Δ ⊢ X = X′ ⇑ Set ⇝ i}{Δ ⊢ u δ ⇑ X′}

When checking an abstraction λxv against a dependent function type value Fun XF, we rename x to the next free de Bruijn level x_{Δ} and check the abstraction body v against F · x_{Δ} in the extended context which binds the abstracted variable to the domain X. To check a neutral term u against X′, we infer the type X of u and compare X and X′. The implementation and verification of this comparison will occupy our attention for the remainder of this article.

Type well-formedness Δ ⊢ V δ ⇑ Set ⇝ i. (Inputs: Δ, V, δ. Output: universe level i of V or fail.)

chk-inf-f \frac{Δ ⊢ V δ ⇓ Set_{i}}{Δ ⊢ V δ ⇑ Set ⇝ i}  chk-set-f \overline{Δ ⊢ Set_{i} δ ⇑ Set ⇝ i + 1}

chk-fun-f \frac{Δ ⊢ V δ ⇑ Set ⇝ i  Δ, x_{Δ}:V δ ⊢ W (δ, y =x_{Δ}) ⇑ Set ⇝ j}{Δ ⊢ (Fun V λyW) δ ⇑ Set ⇝ max(i, j)}

This judgement checks that V is a well-formed type and additionally infers the lowest universe level i this type lives in. The type Set_{i} is well-formed and lives in level i + 1. A neutral type is well-formed if its type is computed as Set_{i} for some i. A function type is well-formed if both domain and codomain are, and it lives in any level both components live in.

Comparison to [Coq96]. The second author has presented a similar type checking algorithm before [Coq96] for unstratified universes Set : Set. The main difference is that in rule chk-inf he uses an untyped β-conversion check X ∼ X′ instead of typed βη-conversion Δ ⊢ X = X′ ⇑ Set ⇝ i which we will describe in the following section. A minor difference is that in Δ ⊢ v δ ⇑ X he uses Δ to assign types to the free variables of term v whereas we use Δ ∘ δ. Consequently, the free variables of X would live in context Δ ∘ δ^{−1} in his case, however, this is problematic in principle since δ may not be invertible, e. g., in case of shadowing. Since he uses untyped conversion, this is irrelevant, because he never needs to look at the types of free variables in X. In our case, it is crucial.

2.4 Checking Equality

Checking the type of a neutral expression against X′ while its type has been inferred as X requires testing the types X and X′ for equality. Since types depend on objects, we will also have to compare objects. The principal method to check η-equality is a type-directed algorithm. In the following we present such a type-directed algorithm for comparing values.

Analogously to type checking, we define three inductive judgements. Herein, d, d′, e, e′, X, X′ ∈ D, Δ ∈ SemCxt, and i ∈ ℕ.

Δ ⊢ e = e′ ⇓ X  neutral e and e′ are equal, inferring type X
Δ ⊢ d = d′ ⇑ X  d and d′ are equal, checked at type X
Δ ⊢ X = X′ ⇑ Set ⇝ i  X and X′ are equal types, inferring universe level i

Inference mode Δ ⊢ e = e′ ⇓ X (inputs: Δ,e,e′, output: X or fail). In inference mode, neutral values e, e′ are checked for equality, and their type is inferred.

aq-var \overline{Δ ⊢ x = x ⇓ Δ(x)}

aq-fun \frac{Δ ⊢ e = e′ ⇓ Fun XF  Δ ⊢ d = d′ ⇑ X}{Δ ⊢ e d = e′ d′ ⇓ F · d}

A variable is only equal to itself; its type is read from the context. A neutral application e d is only equal to another neutral application e′ d′ and the function parts must be equal, as well as the argument parts. The type of e must be a function type Fun XF, whose domain X is used to check d and d′ for equality.

The type of the application e d is computed as F ·d. We could equally well have chosen to return F · d′. That both choices amount to the same follows from the correctness of the equality check; yet we cannot rely on it before we have established correctness. This will be an issue in the correctness proof (Sec. 5); Harper and Pfenning [HP05] have avoided these complications by using simply-typed skeletons to direct the equality algorithm. Their method relies on dependency erasure which works for LF but not for type theories with large eliminations.

Checking mode Δ ⊢ d = d′ ⇑ X (inputs: Δ, d, d′, X, output: succeed or fail).

aq-ne-f \frac{Δ ⊢ e = e′ ⇓ E_{1}  Δ ⊢ E_{1} = E_{2} ⇓ Set_{i}}{Δ ⊢ e = e′ ⇑ E_{2}}

aq-ext \frac{Δ, x_{Δ}:X ⊢ f · x_{Δ} = f′ · x_{Δ} ⇑ F · x_{Δ}}{Δ ⊢ f = f′ ⇑ Fun XF}

aq-ty \frac{Δ ⊢ X = X′ ⇑ Set ⇝ i}{Δ ⊢ X = X′ ⇑ Set_{j}} i ≤ j

Neutral values e, e′ can only be of neutral type E_{i}, they are passed to inference mode. The check Δ ⊢ E_{1} = E_{2} ⇓ Set_{i} should actually not be necessary, because we already now that e and e′ are well-typed, and types are only present to guide the equality algorithm. However, currently we do not know how to show soundness without it. Such redundant checks are present in other works as well [HP05, p. 77].

Two values f, f′ of functional type are equal if applying them to a fresh variable x_{Δ} makes them equal. This is extensional equality, provided we can substitute arbitrary values for the variable. Had we formulated the algorithm on terms instead of values, this would be a standard substitution theorem. However, in our case it is more difficult. We deal with this issue in Sec. 8.

Values X, X′ of type Set_{j} must be types, we check their equality in the type mode. The inferred universe i must be at most j, otherwise X, X′ are not welltyped.

Type mode Δ ⊢ X = X′ ⇑ Set ⇝ i (inputs: Δ, X, X′, output: i or fail).

aq-ty-ne \frac{Δ ⊢ E = E′ ⇓ Set_{i}}{Δ ⊢ E = E′ ⇑ Set ⇝ i}

aq-ty-set

Δ ⊢ Set_{i} = Set_{i} ⇑ Set ⇝ i + 1
aq-ty-fun \frac{Δ ⊢ X = X′ ⇑ Set ⇝ i  Δ, x_{Δ}:X ⊢ F · x_{Δ} = F′ · x_{Δ} ⇑ Set ⇝ j}{Δ ⊢ Fun XF = Fun X′F′ ⇑ Set ⇝ max(i, j)}

A neutral type E can only be equal to another neutral type E′, we delegate the test to the inference mode. A universe Set_{i} is only equal to itself. Function types Fun XF and Fun X′F′ are equal if their domains and codomains coincide. For checking the codomains we introduce the fresh variable x_{Δ} of type X into the context. Again arbitrarily; we could have chosen X′ instead. This is another source of asymmetry which complicates the correctness proof; for LF, it can be avoided by considering simply-typed contexts [HP05].

This algorithm is called semantic since it compares values. It is part of the core of Agda and Epigram 2. Since it is of practical relevance, it is a worth-while effort to verify it. Correctness of type checking is then a consequence of the correctness of algorithmic equality.

3 Specification: Typing with Explicit Substitutions

We want to prove that our algorithmic equality is correct, so we should say in which sense and provide a specification. There are different ways to present type theory. We choose a formulation with explicit substitutions [ML92] because the typing and equality rules can then be validated directed in any (Kripke) PER model over any syntactical applicative structure (see Thm. 1). Altenkirch and Chapman [AC08] exploit this fact for their closure-based definition of values. A formulation with non-explicit (deep) substitution directly validates the inference rules only for PER models over syntactical applicative structures with extra properties, e. g., λ-algebras [AC07], or combinatory algebras [ACD07].

We extend the expression syntax by explicit substitutions and introduce syntactical typing contexts:

Exp ∋ r, s, t ::= ⋯ | tσ  expressions
Subst ∋ σ, τ ::= (σ, x=t) | σ_{id} | σ ∘ τ substitutions
Cxt ∋ Γ ::= ⋄ | Γ, x:A  typing contexts

We identify expressions up to α-conversion and adopt the convention that in contexts Γ all variables must be distinct. Hence, we can view Γ as a map from variables to types with finite domain dom(Γ) and let Γ (x) = A iff (x: A) ∈ Γ. In context extensions Γ, x : A we assume x ∉ dom(Γ). As usual FV(t) is the set of free variables of t. We let FV(t_{1}, …, t_{n}) = FV(t_{1}) ∪ ⋯ ∪ FV(t_{n}) and FV(Γ) = ⋃_{x∈dom(Γ)} FV(Γ (x)).

We have extended the language by explicit substitutions so we need to extend the notion of syntactical applicative structure, to ensure substitutions are evaluated reasonably:

eval-subst-id  σ_{id}ρ = ρ
eval-subst-comp (σ ∘ σ′)ρ = σ(σ′ρ)
eval-subst-ext (σ, x=s)ρ = (σρ, x=sρ)
eval-esubst  (tσ)ρ = t(σρ)

Herein, σρ is defined by x(σρ) = (xσ)ρ.

Judgements. Our type theory with explicit substitutions has the following forms of judgement:

Γ ⊢  Γ is a well-formed context
Γ ⊢ A  A is a well-formed type in Γ
Γ ⊢ t : A  t has type A in Γ
Γ ⊢ σ : Γ′  σ is a well-formed substitution in Γ
Γ ⊢ A = A′  A and A′ are equal types in Γ
Γ ⊢ t = t′ : A  t and t′ are equal terms of type A in Γ
Γ ⊢ σ = σ′ : Γ′ σ and σ′ are equal substitutions in Γ

For an arbitrary judgement, we write Γ ⊢ J, where J is a collection of syntactic entities (terms, contexts, substitutions) to the right of ⊢ in a judgement. FV(J) is the union of the free variable sets of all entities in J. Exceptions are FV(σ : Δ), which is defined as ⋃_{x∈dom(Δ)} FV(Δ(x), σ(x)), and FV(σ = σ′ : Δ) = ⋃_{x∈dom(Δ)} FV(Δ(x), σ(x), σ′(x)).

The judgements on types can be defined in terms of the judgement on terms.

Γ ⊢ A  ⟺ Γ ⊢ A : Set_{i}  for some i
Γ ⊢ A = A′ ⟺ Γ ⊢ A = A′ : Set_{i} for some i

The inference rules for the other judgements are given in figures 1, 2, 3, and 4. They are inspired by categorical presentations of type theory, in particular, categories with families [Dyb96], which have been inspired by Martin-Löf’s substitution calculus [ML92]. Rule const relies on an auxiliary judgement Σ ⊢ c : A meaning constant c can be assigned type A. Its only rule is:

set-f \overline{Σ ⊢ Set_{i} : Set_{i+1}}

In extensions of the core theory, the signature Σ provides the types of constructors of inductive types like the natural numbers.

The judgements enjoy some standard properties, like weakening, inversion of typing, and well-formedness of contexts, types and terms (syntactic validity).

Well-formed contexts Γ ⊢.

cxt-empty \overline{⋄ ⊢}  cxt-ext \frac{Γ ⊢ A}{Γ, x:A ⊢}

Well-typed terms Γ ⊢ t : A.

const \frac{Γ ⊢  Σ ⊢ c : A}{Γ ⊢ c : A}  hyp \frac{Γ ⊢  (x:A) ∈ Γ}{Γ ⊢ x : A}

conv \frac{Γ ⊢ t : A  Γ ⊢ A = A′}{Γ ⊢ t : A′}  sub \frac{Γ ⊢ A : Set_{i}}{Γ ⊢ A : Set_{j}} i ≤ j

fun-f \frac{Γ ⊢ A : Set_{i}  Γ, x:A ⊢ B : Set_{i}}{Γ ⊢ Fun A λxB : Set_{i}}

fun-i \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : Fun A λxB}  fun-e \frac{Γ ⊢ r : Fun A λxB  Γ ⊢ s : A}{Γ ⊢ r s : B(σ_{id}, x=s)}

esubst-f \frac{Γ ⊢ σ : Γ′  Γ′ ⊢ t : A}{Γ ⊢ tσ : Aσ}

Well-formed substitutions Γ ⊢ σ : Γ′.

subst-ext \frac{Γ ⊢ σ : Γ′  Γ′ ⊢ A  Γ ⊢ s : Aσ}{Γ ⊢ (σ, x=s) : (Γ′, x:A)}

subst-id \frac{Γ ⊢}{Γ ⊢ σ_{id} : Γ}  subst-comp \frac{Γ_{2} ⊢ σ : Γ_{3}  Γ_{1} ⊢ τ : Γ_{2}}{Γ_{1} ⊢ σ ∘ τ : Γ_{3}}

subst-weak \frac{Γ ⊢ σ : Γ′, x:A, Γ′′}{Γ ⊢ σ : Γ′, Γ′′}

Fig. 1. Rules for contexts, types, and terms.

Equality Γ ⊢ t = t′ : A. Equivalence, hypotheses, conversion.

eq-refl \frac{Γ ⊢ t : A}{Γ ⊢ t = t : A}  eq-sym \frac{Γ ⊢ t = t′ : A}{Γ ⊢ t′ = t : A}

eq-trans \frac{Γ ⊢ t = t′ : A  Γ ⊢ t′ = t′′ : A}{Γ ⊢ t = t′′ : A}

eq-const \frac{Γ ⊢  Σ ⊢ c : A}{Γ ⊢ c = c : A}  eq-hyp \frac{Γ ⊢  (x:A) ∈ Γ}{Γ ⊢ x = x : A}

eq-conv \frac{Γ ⊢ t = t′ : A  Γ ⊢ A = A′}{Γ ⊢ t = t′ : A′}  eq-sub \frac{Γ ⊢ A = A′ : Set_{i}}{Γ ⊢ A = A′ : Set_{j}} i ≤ j

Dependent functions.

eq-fun-f \frac{Γ ⊢ A = A′ : Set_{i}  Γ, x:A ⊢ B = B′ : Set_{i}}{Γ ⊢ Fun A λxB = Fun A′ λxB′ : Set_{i}}

eq-fun-i \frac{Γ, x:A ⊢ t = t′ : B}{Γ ⊢ λxt = λxt′ : Fun A λxB}

eq-fun-e \frac{Γ ⊢ r = r′ : Fun A λxB  Γ ⊢ s = s′ : A}{Γ ⊢ r s = r′ s′ : B(σ_{id}, x=s)}

eq-fun-β \frac{Γ, x:A ⊢ t : B  Γ ⊢ s : A}{Γ ⊢ (λxt) s = t(σ_{id}, x=s) : B(σ_{id}, x=s)}

eq-fun-η \frac{Γ ⊢ t : Fun A λxB}{Γ ⊢ (λx. t x) = t : Fun A λxB} x ∉ dom(Γ)

Fig. 2. Equality rules.

Equivalence rules and weakening.

eq-subst-refl \frac{Γ ⊢ σ : Γ′}{Γ ⊢ σ = σ : Γ′}  eq-subst-sym \frac{Γ ⊢ σ = σ′ : Γ′}{Γ ⊢ σ′ = σ : Γ′}

eq-subst-trans \frac{Γ_{1} ⊢ σ = σ′ : Γ_{2}  Γ_{2} ⊢ σ′ = σ′′ : Γ_{3}}{Γ_{1} ⊢ σ = σ′′ : Γ_{3}}

eq-subst-weak \frac{Γ ⊢ σ = σ′ : Γ′, x:A, Γ′′}{Γ ⊢ σ = σ′ : Γ′, Γ′′}

Rules of the category of contexts and substitutions.

eq-subst-id-l \frac{Γ ⊢ σ : Γ′}{Γ ⊢ σ_{id} ∘ σ = σ : Γ′}  eq-subst-id-r \frac{Γ ⊢ σ : Γ′}{Γ ⊢ σ ∘ σ_{id} = σ : Γ′}

eq-subst-assoc \frac{Γ_{3} ⊢ σ : Γ_{4}  Γ_{2} ⊢ σ′ : Γ_{3}  Γ_{1} ⊢ σ′′ : Γ_{2}}{Γ_{1} ⊢ (σ ∘ σ′) ∘ σ′′ = σ ∘ (σ′ ∘ σ′′) : Γ_{4}}

Rules for the empty substitution and substitution extension.

eq-subst-empty-η \frac{Γ ⊢ σ : ⋄  Γ ⊢ σ′ : ⋄}{Γ ⊢ σ = σ′ : ⋄}

eq-subst-ext-β \frac{Γ_{2} ⊢ σ : Γ_{3}  Γ_{3} ⊢ A  Γ_{2} ⊢ s : Aσ  Γ_{1} ⊢ τ : Γ_{2}}{Γ_{1} ⊢ (σ, x=s) ∘ τ = (σ ∘ τ, x=sτ) : Γ_{3}, x:A}

eq-subst-ext-η \frac{Γ, x:A ⊢}{Γ, x:A ⊢ (σ_{id}, x=x) = σ_{id} : Γ, x:A}

eq-subst-ext-weak \frac{Γ ⊢ σ : Γ′  Γ′, x:A ⊢  Γ ⊢ t : Aσ}{Γ ⊢ (σ, x=t) = σ : Γ′}

Congruence rules.

eq-subst-ext \frac{Γ ⊢ σ = σ′ : Γ′  Γ′ ⊢ A  Γ ⊢ s = s′ : Aσ}{Γ ⊢ (σ, x=s) = (σ′, x=s′) : (Γ′, x:A)}

eq-subst-comp \frac{Γ_{2} ⊢ σ = σ′ : Γ_{3}  Γ_{1} ⊢ τ = τ′ : Γ_{2}}{Γ_{1} ⊢ σ ∘ τ = σ′ ∘ τ′ : Γ_{3}}

Fig. 3. Equality rules for substitutions Γ ⊢ σ = σ′ : Δ.

eq-esubst-f \frac{Γ ⊢ σ = σ′ : Δ  Δ ⊢ t = t′ : A}{Γ ⊢ tσ = t′σ′ : Aσ}

eq-esubst-id \frac{Γ ⊢ t : A}{Γ ⊢ tσ_{id} = t : A}

eq-esubst-comp \frac{Γ ⊢ τ : Γ′  Γ′ ⊢ σ : Γ′′  Γ′′ ⊢ t : A}{Γ ⊢ t(σ ∘ τ) = (tσ)τ : A(σ ∘ τ)}

eq-esubst-c \frac{Γ ⊢ σ : Γ′  Σ ⊢ c : A}{Γ ⊢ cσ = c : A}

eq-esubst-var \frac{Γ ⊢ σ : Γ′  Γ′, x:A ⊢  Γ ⊢ t : Aσ}{Γ ⊢ x(σ, x=t) = t : Aσ}

eq-esubst-fun-f \frac{Γ ⊢ σ : Γ′  Γ′ ⊢ A : Set_{i}  Γ′, x:A ⊢ B : Set_{i}}{Γ ⊢ (Fun A λxB)σ = Fun (Aσ) (λxB)σ : Set_{i}} x ∉ dom(Γ)

eq-esubst-fun-i \frac{Γ ⊢ σ : Γ′ Γ′, x:A ⊢ t : B}{Γ ⊢ (λxt)σ = λx. t(σ, x=x) : (Fun A λxB)σ} x ∉ dom(Γ)

eq-esubst-fun-e \frac{Γ ⊢ σ : Γ′  Γ′ ⊢ r : Fun A λxB  Γ′ ⊢ s : A}{Γ ⊢ (r s)σ = rσ sσ : B(σ, x=sσ)}

Fig. 4. Equality rules for explicit substitutions.

4 Verification Plan and Contextual Reification

A standard method to show completeness of the algorithmic equality would be the following [HP05].

1. Define a Kripke logical relation Δ ⊢ d = d′ : X on a semantic context Δ and values d, d′ by induction on the type X. We will call this relation Kripke model. For base types X, let the relation coincide with algorithmic equality Δ ⊢ d = d′ ⇑ X, for function types do the usual functional construction: Δ ⊢ f = f′ : Fun XF iff Δ′ ⊢ d = d′ : X implies Δ′ ⊢ f · d = f′ · d′ : F · d for all d, d′ and all extensions Δ′ of Δ.

2. Show that if two values are related in the model, then the algorithm relates them as well. Following Schürmann and Sarnat [SS08] we call this the escape lemma, since it allows to “get out of the logical relation”.

3. Finally show validity of the inference rules w. r. t. the model, i.e., if two terms t, t′ are equal of type A, then for each well-formed environment ρ, we have tρ = t′ρ : Aρ in the model, which implies that the algorithm accepts t, t′ as equal.

In particular, the relation Δ ⊢ = : X needs to be a partial equivalence, in order to validate symmetry and transitivity rules. But due to the asymmetric nature of algorithmic equality (rules aq-fun and aq-ty-fun), this can only be shown if we have soundness, which at this point we cannot obtain.

Normalization-by-evaluation (NbE) [ML75,BS91,Coq94,Dan99] to the rescue! There already are equality algorithms for dependent types with large eliminations which are based on semantics [AAD07,ACD07]. Two semantic values are considered equal if they reify to the same expression. Reification at a type X converts a value to a term, η-expanding it on the fly according to type X. It turns out that we can verify the algorithmic equality by relating it to NbE.

We will verify algorithmic equality according to this plan:

1. Define normalization-by-evaluation for our setting. This amounts to defining contextual reification Δ ⊢ d ↘ v ⇑ X which converts value d of type X in context Δ to normal form v.

2. Show completeness of NbE (Sec. 5), meaning that if one takes two judgmentally equal terms t, t′, evaluates and reifies them, one arrives at the same normal form v (Cor. 1). To this end, we construct a Kripke model based on reification, meaning that two values are equal at base type if they reify to the same normal form.

3. Show soundness of NbE (Sec. 6), meaning that if we take a term t, evaluate and reify it, we arrive at a normal form v judgmentally equal to t (Cor. 2). The main tool is a Kripke logical relation between well-typed terms t and semantic objects d, which for base types states that d reifies to a normal form v which is judgmentally equal to t.

4. Show completeness of the algorithmic equality (Sec. 7). This is a corollary of completeness of NbE, since we will see that if two values reify to the same normal form, then the algorithm will accept them as equal (Lemma 7).

5. Show soundness of the algorithm (Sec. 8). The direct approach, showing that two algorithmically equal values reify to the same normal form, fails due to the asymmetry of the algorithm. We introduce the concept of strong semantic typing and equality (a super Kripke model, so to say) and prove that the algorithm is sound for strong semantic equality. By establishing that the inference rules are valid in the super Kripke model (Cor. 4), and that equality in the super Kripke model entails equality in the Kripke model, we finally show that well-typed terms whose values are algorithmically equal reify to the same normal form, thus, are judgmentally equal (Thm. 3).

What remains open is termination of algorithmic equality.

4.1 Contextual Reification

Reification [BS91] converts a semantic value to a syntactic term, η-expanding it on the fly. It is defined by recursion on the type of the value. In previous NbE approaches [BS91,ACD07] the semantics of base types has been defined as a set of η-long neutral terms, thus, reification at base type is simply the identity. In our approach, the semantics of base types is a set of neutral values, which are not η-expanded and need to be reified recursively. This can only happen if reification has access to the types of the free variables of a neutral value. For example, to reify x d d′ at base type we need to retrieve the type Fun X F of x, recursively reify d at type X, compute F · d = Fun X′ F′ and recursively reify d′ at type X′. For this task, we introduce a new form of reification which is parameterized by a semantic typing context Δ, hence the name contextual reification.

We simultaneously define three inductive judgements by the rules to follow. Herein, Δ ∈ SemCxt, d, e, X ∈ D, u ∈ Ne, v, V ∈ Nf and i ∈ ℕ.

Δ ⊢ e ↘ u ⇓ X  neutral value e reifies to u, inferring its type X
Δ ⊢ d ↘ v ⇑ X  value d reifies to normal form v at type X
Δ ⊢ X ↘ V ⇑ Set ⇝ i type value X reifies to V, inferring its level i.

Inference mode Δ ⊢ e ↘ u ⇓ X (inputs: Δ, e, outputs: u, X or fail).

reify-var \overline{Δ ⊢ x ↘ x ⇓ Δ(x)}

reify-fun-e \frac{Δ ⊢ e ↘ u ⇓ Fun XF  Δ ⊢ d ↘ v ⇑ X}{Δ ⊢ e d ↘ u v ⇓ F · d}

Variables reify to themselves and neutral applications to neutral applications. The type information flows out of the context Δ and is used in reify-fun-e to reify d of type X in checking mode.

Checking mode Δ ⊢ d ↘ v ⇑ X (inputs: Δ, d, X, output: v or fail).

reify-ne \frac{Δ ⊢ e ↘ u ⇓ E_{1}  Δ ⊢ E_{1} ↘ u′ ⇓ Set_{i}  Δ ⊢ E_{2} ↘ u′ ⇓ Set_{i}}{Δ ⊢ e ↘ u ⇑ E_{2}}

reify-ext \frac{Δ, x:X ⊢ f · x ↘ v ⇑ F · x}{Δ ⊢ f ↘ λxv ⇑ Fun XF}

reify-ty \frac{Δ ⊢ X ↘ V ⇑ Set ⇝ i}{Δ ⊢ X ↘ V ⇑ Set_{j}} i ≤ j

Any value f of functional type is reified by applying it to a fresh variable x. Note that this can trigger further evaluation, e. g., in the λ-model where functional values are just weak head normal forms or closures. The result of reifying a functional value is always a λ-abstraction, which means that reification returns η-long forms.

At neutral type E_{2}, objects e need to be neutral and are reified in inference mode. The inferred type E_{1} needs to be equal to E_{2}—this is checked by reifying both types, expecting the same normal form.

Type mode Δ ⊢ X ↘ V ⇑ Set ⇝ i (inputs: Δ, X, outputs: V, i or fail).

reify-ty-ne \frac{Δ ⊢ e ↘ u ⇓ Set_{i}}{Δ ⊢ e ↘ u ⇑ Set ⇝ i}

reify-ty-set

Δ ⊢ Set_{i} ↘ Set_{i} ⇑ Set ⇝ i + 1
reify-ty-fun \frac{Δ ⊢ X ↘ V ⇑ Set ⇝ i  Δ, x:X ⊢ F · x ↘ W ⇑ Set ⇝ j}{Δ ⊢ Fun XF ↘ Fun V λxW ⇑ Set ⇝ max(i, j)}

Function type values reify to function type expressions in long normal form, universes to universes and neutral type values to neutral type expressions.

We write Δ ⊢ e, e′ ↘ u ⇓ X for Δ ⊢ e ↘ u ⇓ X and Δ ⊢ e′ ↘ u ⇓ X. This gives a basic equality on neutral objects (which is used in rule reify-ne, for instance).

We say Δ′ extends Δ, written Δ′ ≤ Δ, if Δ′(x) = Δ(x) for all x ∈ dom(Δ). (The direction of ≤ is as in subtyping.) Reification is closed under weakening of contexts, i.e., reifying in an extended context produces an α-equivalent normal form. Reification provides us with a normalization function: given a closed term t : A, the normal form v is obtained by ⋄ ⊢ tρ_{id} ↘ v ⇑ Aρ_{id}.

5 Kripke Model and Completeness of NbE

Dependent types complicate the definition of a logical relation, because one cannot use structural induction on the type expression. Instead one needs to simultaneously define the “good” type values X by induction and their denotation, a relation on objects, by recursion [Dyb00]. We spell out this construction for our Kripke model in sections 5.1–5.3. In Section 5.4 we prove that it models our inference rules.

5.1 An induction measure

If X ⊆ D and F(d) ⊆ D for each d ∈ X, then the dependent function space

Π X F = {f | ∀d ∈ X . f · d ∈ F(d)}

is another subset of D. For i = 0, 1, … we define the sets T_{i} ⊆ D × P(D) inductively as follows:

\overline{(E, D) ∈ T_{i}} \overline{(Set_{j}, |T_{j}|) ∈ T_{i}} j < i

\frac{(X, X) ∈ T_{i} ∀d ∈ X . (F · d, F(d)) ∈ T_{i}}{(Fun XF, Π X F) ∈ T_{i}}

Herein, |T_{i}| = {X | ∃X . (X, X) ∈ T_{i}}. We define the relation : ⊆ D × D by

d : X ⟺ ∃X , i. (X, X) ∈ T_{i} and d ∈ X

As a special case, X : Set_{i} ⟺ X ∈ |T_{i}|. We will use the derivation of membership in T_{i} as induction measure, quoted as “induction on X : Set_{i}”.

5.2 Construction of the Kripke model

It is tempting to define Δ ⊢ d = d′ : X for base types directly as “Δ ⊢ d ↘ v ⇑ X and Δ ⊢ d′ ↘ v ⇑ X for some v”. However, then the proof of the escape lemma will fail, because during reification of function types, their domains flow into the context. Reifying two function types will soon take place in different contexts. We need to be more general and relate semantic objects at a priori different types in a priori different contexts. Thus, in the following we define a relation Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : X′ for the purpose of proving the escape lemma, and we obtain Δ ⊢ d = d′ : X as a special case in Sec. 5.3.

By lexicographic induction on i and X′ : Set_{i} we define the relations:

\begin{matrix}⊢ : Ⓢ ⊢ X′ : Set_{i} \\ ⊢ : Ⓢ ⊢ : X′ \end{matrix}

– Case E′ : Set_{i}.

Δ ⊢ X : Z Ⓢ Δ′ ⊢ E′ : Set_{i}

⟺ X = E neutral and Z = Set_{i} and

Δ ⊢ E ↘ U ⇓ Set_{j} and Δ′ ⊢ E′ ↘ U ⇓ Set_{j′} for some U and j, j′ ≤ i

Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : E′

⟺ X = E neutral and Δ ⊢ d ↘ u ⇓ Ê and Δ′ ⊢ d′ ↘ u ⇓ Ê′ and
Δ ⊢ E, Ê ↘ U ⇓ Set_{j} and Δ′ ⊢ E′, Ê′ ↘ U ⇓ Set_{j′}
for some E, Ê, Ê′, u, U, and j, j′ ≤ i

– Case Set_{j} : Set_{i} for j < i.

Δ ⊢ X : Z Ⓢ Δ′ ⊢ Set_{j} : Set_{i} ⟺ X = Set_{j} and Z = Set_{i}
Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : Set_{j} has already been defined

– Case Fun X′ F′ : Set_{i} where X′ : Set_{i} and F′ · d : Set_{i} for all d : X′.

Δ ⊢ Y : Z Ⓢ Δ′ ⊢ Fun X′F′ : Set_{i}

⟺ Y = Fun XF for some X, F and Z = Set_{i} and
Δ ⊢ X : Set_{i} Ⓢ Δ′ ⊢ X′ : Set_{i} and
for all Δ̂ ≤ Δ, Δ̂′ ≤ Δ′, d, d′, Δ̂ ⊢ d : X Ⓢ Δ̂′ ⊢ d′ : X′
implies Δ̂ ⊢ F · d : Set_{i} Ⓢ Δ̂′ ⊢ F′ · d′ : Set_{i}

Δ ⊢ f : Y Ⓢ Δ′ ⊢ f : Fun X′F′

⟺ Y = Fun XF for some X, F and
for all Δ̂ ≤ Δ, Δ̂′ ≤ Δ′, d, d′, Δ̂ ⊢ d : X Ⓢ Δ̂′ ⊢ d′ : X′
implies Δ̂ ⊢ f · d : F · d Ⓢ Δ̂′ ⊢ f′ · d′ : F′ · d′

Lemma 1. Ⓢ is symmetric and transitive. Lemma 2 (Type conversion). Let X′ : Set_{i}. If Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : X′ and Δ′ ⊢ X′ : Set_{i} Ⓢ Δ′ ⊢ X′′ : Set_{i} then Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : X′′. Proof. By induction on X′ : Set_{i}. Lemma 3 (Into and out of the model / escape lemma). Let X′ : Set_{i}. Then

1. (In:) If Δ ⊢ e ↘ u ⇓ X and Δ′ ⊢ e′ ↘ u ⇓ X′ then Δ ⊢ e : X Ⓢ Δ′ ⊢ e′ : X′.

2. (Out:) If Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : X′ then Δ ⊢ d ↘ v ⇑ X and Δ′ ⊢ d′ ↘ v ⇑ X′ for some v.

3. (Out-Type:) If Δ ⊢ X : Set_{i} Ⓢ Δ′ ⊢ X′ : Set_{i} Δ ⊢ X ↘ V ⇑ Set ⇝ j and Δ′ ⊢ X′ ↘ V ⇑ Set ⇝ j′ for some V and j, j′ ≤ i.

Proof. Simultaneously by induction on X′ : Set_{i}.

5.3 The Kripke model We now define

Δ ⊢ d = d′ : X ⟺ Δ ⊢ d : X Ⓢ Δ ⊢ d′ : X.

We can view the relation Δ ⊢ d = d′ : X as inductively generated by the following rules:

\overline{Δ ⊢ Set_{i} = Set_{i} : Set_{j}} i < j

\frac{Δ ⊢ E ↘ u ⇓ Set_{i} Δ ⊢ E′ ↘ u ⇓ Set_{i}}{Δ ⊢ E = E′ : Set_{j}} i ≤ j

\frac{Δ ⊢ e ↘ u ⇓ E_{1}  Δ ⊢ e′ ↘ u ⇓ E_{2}  Δ ⊢ E_{0}, E_{1}, E_{2} ↘ u′ ⇓ Set_{i}}{Δ ⊢ e = e′ : E_{0}}

\frac{Δ ⊢ X = X′ : Set_{i} Δ′ ⊢ F · d = F′ · d′ : Set_{i} for all Δ′ ≤ Δ and Δ′ ⊢ d = d′ : X}{Δ ⊢ Fun XF = Fun X′F′ : Set_{i}}

\frac{Δ′ ⊢ f · d = f′ · d′ : F · d for all Δ′ ≤ Δ and Δ′ ⊢ d = d′ : X}{Δ ⊢ f = f′ : Fun XF}

We let Δ ⊢ X = X′ iff there exists an i such that Δ ⊢ X = X′ : Set_{i}. We write Δ ⊢ d : X for Δ ⊢ d = d : X.

5.4 Validity of Syntactic Typing

Now we can show that all the rules for our typing and equality judgements are valid in the model. As a byproduct, we get completeness of NbE.

Let

Δ ⊢ ρ = ρ′ : Γ ⟺ ∀x ∈ dom(Γ). Δ ⊢ ρ(x) = ρ′(x) : Γ (x)ρ

Define Γ ⊩ J, meaning that Γ ⊢ J is valid in the Kripke model, as follows:

⋄ ⊩  :⟺ true
Γ, x:A ⊩  :⟺ Γ ⊩ A
Γ ⊩ A  :⟺ either A = Set_{i} and Γ ⊩ or Γ ⊩ A : Set_{i} for some i
Γ ⊩ t : A  :⟺ Γ ⊩ t = t : A
Γ ⊩ t = t′ : A :⟺ Γ ⊩ A and ∀Δ ⊢ ρ = ρ′ : Γ. Δ ⊢ tρ = t′ρ′ : Aρ
Γ ⊩ σ : Γ′  :⟺ Γ ⊩ σ = σ : Γ′
Γ ⊩ σ = σ′ : Γ′ :⟺ Γ ⊩ and Γ′ ⊩ and ∀Δ ⊢ ρ = ρ′ : Γ. Δ ⊢ σρ = σ′ρ′ : Γ′

Theorem 1 (Soundness of the inference rules). If Γ ⊢ J then Γ ⊩ J.

Proof. By induction on Γ ⊢ J. (Tedious, but easy.)

Lemma 4. Γ ρ_{id} ⊢ ρ_{id} = ρ_{id} : Γ.

Proof. For each x ∈ dom(Γ), we have Γ ρ_{id} ⊢ xρ_{id} = xρ_{id} : Γ (x)ρ_{id}.

Corollary 1 (Completeness of NbE). If Γ ⊢ t = t′ : A then Γ ρ_{id} ⊢ tρ_{id} ↘ v ⇑ Aρ_{id} and Γ ρ_{id} ⊢ t′ρ_{id} ↘ v ⇑ Aρ_{id} for some v.

6 Kripke Logical Relation and Soundness of NbE

In the previous section we have defined a logical relation Δ ⊢ d : X Ⓢ Δ′ ⊢ d′ : X′ between two semantic objects in their typing environments. Now we will define a logical relation between a well-typed expression Γ ⊢ t : A and a value d in its typing environment Δ ⊢ X. The relation shall imply that d at type X reifies in Δ to a normal form v which is judgmentally equal to t at type A in context Γ (Lemma 5). The construction is similar to [ACD07] but has Δ as additional parameter.

We write Γ′ ≤ Γ if Γ′ is a well-formed extension of Γ. By induction on X : Set_{i} we define the relation

Γ ⊢ t : C ◯^{R} Δ ⊢ d : X

between well-typed terms Γ ⊢ t : C and semantic objects Δ ⊢ d : X.

Γ ⊢ r : C ◯^{R} Δ ⊢ f : Fun XF ⟺

Γ ⊢ C = Fun A λxB : Set_{i} for some A, B and

Γ ⊢ A : Set_{i} ◯^{R} Δ ⊢ X : Set_{i} and

Γ′ ⊢ r s : B(σ_{id}, x=s) ◯^{R} Δ′ ⊢ f d : F d for all Γ′ ≤ Γ, Δ′ ≤ Δ

and Γ′ ⊢ s : A ◯^{R} Δ′ ⊢ d : X

Γ ⊢ r : C ◯^{R} Δ ⊢ Fun XF : Set_{i} ⟺

Γ ⊢ C = Set_{i} : Set_{i+1}

Γ ⊢ r = Fun A λxB : Set_{i} for some A, B and

Γ ⊢ A : Set_{i} ◯^{R} Δ ⊢ X : Set_{i} and

Γ′ ⊢ B(σ_{id}, x=s) : Set_{i} ◯^{R} Δ′ ⊢ F d : Set_{i} for all Γ′ ≤ Γ, Δ′ ≤ Δ

and Γ ⊢ s : A ◯^{R} Δ ⊢ d : X

Γ ⊢ r : C ◯^{R} Δ ⊢ d : X ⟺ Δ ⊢ d ↘ v ⇑ X and Γ ⊢ r = v : C

for X neutral or X = Set_{i} and d ≠ Fun Y F

The logical relation is closed under weakening of contexts (both the syntactic, Γ, and the semantic one, Δ) and under judgmental and Kripke model equality, meaning one can always trade expressions and values for equals without violating the relation.

Lemma 5 (Into and out of the logical relation / escape lemma). Let

Γ ⊢ C : Set_{i} ◯^{R} Δ ⊢ X : Set_{i}.

1. (In:) If Γ ⊢ u : C and Δ ⊢ e ↘ u ⇓ X then Γ ⊢ u : C ◯^{R} Δ ⊢ e : X.

2. (Out:) If Γ ⊢ r : C ◯^{R} Δ ⊢ d : X then Δ ⊢ d ↘ v ⇑ X for some v with Γ ⊢ r = v : C.

3. (Out-type:) Δ ⊢ X ↘ V ⇑ Set ⇝ j for j ≤ i and Γ ⊢ C = V : Set_{i}.

Proof. By induction on X : Set_{i}.

Fundamental theorem. We relate substitutions Γ′ ⊢ σ : Γ to environments Δ ⊢ ρ : Γ by the following definition:

Γ′ ⊢ σ ◯^{R} Δ ⊢ ρ :: Γ ⟺ for all x ∈ dom(Γ),

Γ′ ⊢ xσ : Γ (x)σ ◯^{R} Δ ⊢ ρ(x) : Γ (x)ρ

By induction on the length of Γ, we define the propositions Γ ⊪ J as follows:

⊪  ⟺ true
Γ, x:A ⊪  ⟺ Γ ⊪ A
Γ ⊪ A  ⟺ either A = Set_{i} and Γ ⊪ or Γ ⊪ A : Set_{i} for some i
Γ ⊪ t : A  ⟺ Γ ⊪ t = t : A
Γ ⊪ t = t′ : A ⟺ Γ ⊪ and

Γ′ ⊢ tσ : Aσ ◯^{R} Δ ⊢ t′ρ : Aρ for all Γ′ ⊢ σ ◯^{R} Δ ⊢ ρ :: Γ.

Γ ⊪ τ : Γ_{0}  ⟺ Γ ⊪ τ = τ : Γ_{0}
Γ ⊪ τ = τ′ : Γ_{0} ⟺ Γ ⊪ and Γ_{0} ⊪ and

Γ′ ⊢ τ ∘ σ ◯^{R} Δ ⊢ τ′ρ :: Γ_{0} for all Γ′ ⊢ σ ◯^{R} Δ ⊢ ρ :: Γ.

Theorem 2 (Fundamental theorem of logical relations). If Γ ⊢ J then Γ ⊪ J.

Proof. By induction on Γ ⊢ J.

Lemma 6. Γ ⊢ σ_{id} ◯^{R} (Γ ρ_{id}) ⊢ ρ_{id} :: Γ.

Proof. We have to show Γ ⊢ x : Γ (x) ◯^{R} Γ ρ_{id} ⊢ x : Γ (x)ρ_{id} for all x ∈ dom(Γ). This holds by Lemma 5 since Γ ρ_{id} ⊢ x ↘ x ⇓ (Γ ρ_{id})(x).

Corollary 2 (Soundness of NbE). If Γ ⊢ t : A then there is some v such that Γ ρ_{id} ⊢ tρ_{id} ↘ v ⇑ Aρ_{id} and Γ ⊢ t = v : A.

7 Completeness of Algorithmic Equality

In this section, we conclude the completeness of the equality algorithm from the completeness of NbE. In particular, if two values reify to the same normal form, they are algorithmically equal. Some care has to be paid to the case of functional values. It could be that f reifies to λxv since f · x reifies to v and f′ reifies to λx′v′ =_{α} λxv since f′ · x′ reifies to v′. Now we want to conclude that f and f′ are algorithmically equal, which requires f ·x_{Δ} equal to f′ ·x_{Δ}. But the induction hypothesis is not applicable since x, x′, x_{Δ} might be different variables, hence, f ·x and f ·x_{Δ} are different objects. If our values are actually normal expressions, we could use plain old α-conversion and rename the variables. However, we are dealing with values in an arbitrary syntactical applicative structure D!

We restrict the class of possible models to those that admit renaming of free variables. This is a sensible restriction since values should be parametric in the names of their free variables—case distinction on the name of a identifier is not a desirable program behavior.

Renamings. Let π be a bijective map from variables to variables. We assume a renaming operations dπ on values d ∈ D with the following properties:

ren-c cπ  = c
ren-var xπ  = π(x)
ren-app (f · d)π = fπ · dπ
ren-eval (tρ)π = t(ρπ)

Renaming can be defined for many syntactical applicative structures D: term models, explicit substitutions, closures, even Scott models which evaluate an abstraction (λxt)ρ to an actual function h : D → D with h(d) = t(ρ, x = d). Setting (hπ)(d) = (h(dπ^{−1}))π we have (h(d))π = (hπ)(dπ) [Pit06].

We define renaming of contexts π(Δ) by

ren-cxt-empty π(⋄)  = ⋄
ren-cxt-ext π(Δ, x:X) = π(Δ), π(x):Xπ

Remark 1. This is not to be confused with the operation Δπ which is composition defined by (Δπ)(x) = Δ(x)π. We have π(Δ)(xπ) = Δ(x)π. Thus, π(Δ) = π^{−1}Δπ is a conjugation.

Lemma 7 (Completeness of algorithmic equality w. r. t. reification). Let Δ = x_{1} :X_{1}, … x_{n}:X_{n} be a semantic context and π a permutation of names assigning the ith de Bruijn level to variable x_{i} (π(x_{i}) = x_{i} for i = 1..n).

1. If Δ ⊢ e ↘ u ⇓ X and Δ′ ⊢ e′ ↘ u ⇓ X′ then π(Δ) ⊢ eπ = e′π ⇓ Xπ.

2. If Δ ⊢ d ↘ v ⇑ X and Δ′ ⊢ d′ ↘ v ⇑ X′ then π(Δ) ⊢ dπ = d′π ⇑ Xπ.

3. If Δ ⊢ X ↘ V ⇑ Set ⇝ i and Δ′ ⊢ X′ ↘ V ⇑ Set ⇝ i′ then π(Δ) ⊢ Xπ = X′π ⇑ Set ⇝ max(i, i′).

Proof. Simultaneously by induction on the first derivation.

A name permutation π can be viewed as an environment, taking a variable x to π(x). This explains the notation tπ, and π(Γ) which satisfies π(Γ)(xπ) = Γ (x)π. Let π_{(x_{1}:A_{1},...x_{n}:A_{n})}(x_{i}) = x_{i} for i = 1..n.

Corollary 3 (Completeness of algorithmic equality). If Γ ⊢ t = t′ : A then π_{Γ} (Γ) ⊢ tπ_{Γ} = t′π_{Γ} ⇑ Aπ_{Γ}.

Proof. We have Γ ρ_{id} ⊢ tρ_{id}, t′ρ_{id} ↘ ⇑ Aρ_{id} by Cor. 1, thus, the corollary follows from Lemma 7 with ρ_{id}π_{Γ} = π_{Γ}.

8 Strong Semantic Typing and Soundness of Algorithmic Equality

In this section, we tackle the second problem: soundness of the equality algorithm. We show that if two values are algorithmically equal, then they reify to the same normal form. Rule aq-fun gives us a hard time:

aq-fun \frac{Δ ⊢ e = e′ ⇓ Fun XF  Δ ⊢ d = d′ ⇑ X}{Δ ⊢ e d = e′ d′ ⇓ F · d}

Using the induction hypothesis, we can show Δ ⊢ e′ d′ ↘ u v ⇓ F · d′ but we need F · d! The fact that d and d′ reify to the same normal form does not help us here, we need a stronger induction hypothesis.

Again, soundness of an algorithmic equality on syntax is usually trivial: one simply shows that each algorithmic rule is an instance of an inference rule. When trying to apply this intuition to our semantic typing and equality, the Kripke model, one realizes that it lacks a substitution principle: Judgements remain valid when substituting a term of the right type for a variable. In the following we will equip our semantics with a substitution principle by brute force! We define strong semantic judgements (a super Kripke model) to hold if the weak semantic judgements (Kripke model) hold for all well-typed valuations of free variables (cf. hypothetical judgements [CPT05]). As precondition, we need a model in which we can reevaluate values in a new environment.

Reevaluation. For the following, impose more conditions on the model D. It must be equipped with a reevaluation function dθ of value d in environment θ, satisfying the following laws:

reeval-id  d ρ_{id} = d
reeval-c cθ = c
reeval-var xθ  = θ(x)
reeval-fun-e (f · d)θ = fθ · dθ
reeval-esubst (tρ)θ = t(ρθ)

Reevaluation is easy to define on the syntactical applicative structure of closures; simply add ([λxt]ρ)θ = [λxt](ρθ) and (e d)θ = eθ · dθ to the above laws.

For Scott models, it is a bit more problematic. If f ∈ D → D, we can set (fθ)(d) = (f(x))((θ, x=d) for a fresh variable x. Freshness can be defined if we construct D as a nominal set [Shi05]. However, not all continuous functions f will fulfill reeval-fun-e: for (f(d))θ = (f(x))(θ, x = dθ) to hold f must treat variables parametrically. For example, the function f(d) = d if d not a variable and f(x) = Set_{0} for x a variable is not parametric and, thus, not compatible with reevaluation. The formulation of suitable parametricity conditions and the proof of parametricity for all values in the Kripke model remains open.

8.1 Super Kripke model

Let Θ range over semantic contexts and let

Δ ⊢ ρ = ρ′ : Θ ⟺ ∀x ∈ dom(Θ). Δ ⊢ xρ = xρ′ : Θ(x)ρ

We write Δ ⊢ ρ : Θ iff Δ ⊢ ρ = ρ : Θ. We define strong semantic equality by

Θ ⊧ d = d′ : X ⟺ ∀Δ ⊢ ρ = ρ′ : Θ. Δ ⊢ dρ = d′ρ′ : Xρ

Let Θ ⊧ X = X′ iff Θ ⊧ X = X′ : Set_{i} for some i. We write Θ ⊧ X for Θ ⊧ X = X and Θ ⊧ d : X for Θ ⊧ d = d : X, and say d is semantically strongly typed of type X in context Θ.

Since Δ ⊢ ρ_{id} = ρ_{id} : Δ, strong semantic equality Δ ⊧ d = d′ : X implies weak semantic equality Δ ⊢ d = d′ : X.

Lemma 8 (Admissible rules). The following implications, written as rules, hold for strong semantic equality.

\overline{Θ ⊧ x = x : Θ(x)} x ∈ dom(Θ)

\frac{Θ ⊧ f = f′ : Fun XF Θ ⊧ d = d′ : X}{Θ ⊧ f · d = f′ · d′ : F · d}

\frac{Θ ⊧ Fun XF  Θ ⊧ f : Fun XF  Θ ⊧ f′ : Fun XF Θ, x:X ⊧ f · x = f′ · x : F · x}{Θ ⊧ f = f′ : Fun XF}

\frac{Θ ⊧ Fun XF, Fun X′F′ : Set_{i} Θ ⊧ X = X′ : Set_{i} Θ, x:X ⊧ F · x = F′ · x : Set_{i}}{Θ ⊧ Fun XF = Fun X′F′ : Set_{i}}

\frac{Θ ⊧ d = d′ : X Θ ⊧ X = X′}{Θ ⊧ d = d′ : X′}

Proof. The soundness of the application rule relies on distributivity of valuation over application, (f · d)ρ = fρ · dρ.

Semantic context equality ⊧ Θ = Θ′ is given inductively by

\overline{⊧ ⋄ = ⋄}  \frac{⊧ Θ = Θ′  Θ ⊧ X = X′ : Set_{i}}{⊧ Θ, x:X = Θ′, x:X′} x ∉ dom(Θ)

We write ⊧ Θ for ⊧ Θ = Θ.

Lemma 9 (Soundness of algorithmic equality). Let ⊧ Δ.

1. If Δ ⊢ e = e′ ⇓ X then Δ ⊧ X and Δ ⊧ e = e′ : X.

2. If Δ ⊢ d = d′ ⇑ X and Δ ⊧ X and Δ ⊧ d, d′ : X then Δ ⊧ d = d′ : X.

3. If Δ ⊢ X = X′ ⇑ Set ⇝ i and Δ ⊧ X, X′ : Set_{i} then Δ ⊢ X = X′ : Set_{i}.

Proof. Simultaneously by induction on the derivation of algorithmic equality using the admissible rules.

8.2 Strong Validity of Syntactic Typing

In the following, we establish that our inference rules are also valid in the super Kripke model. However, no new inductive proof is needed. We have already shown that the rules are valid in the weak semantics (Kripke model) under all weakly typed environments. This is actually equivalent to being valid in the strong semantics (super Kripke model) under all strongly typed environments.

We define strongly typed environments by

Δ ⊧ ρ = ρ′ : Γ ⟺ ∀x ∈ dom(Γ). Δ ⊧ ρ(x) = ρ′(x) : Γ (x)ρ.

Lemma 10 (Composing strongly and weakly typed environments). If Θ ⊧ ρ = ρ′ : Γ and Δ ⊢ θ = θ′ : Θ then Δ ⊢ ρθ = ρ′θ′ : Γ.

Define Γ |⊧ J, meaning that Γ ⊢ J is valid in the super Kripke model, as follows:

⋄ |⊧  :⟺ true
Γ, x:A |⊧  :⟺ Γ |⊧ A
Γ |⊧ A  :⟺ either A = Set_{i} and Γ |⊧ or Γ |⊧ A : Set_{i} for some i
Γ |⊧ t : A  :⟺ Γ |⊧ t = t : A
Γ |⊧ t = t′ : A :⟺ Γ |⊧ A and ∀Δ ⊧ ρ = ρ′ : Γ. Δ ⊧ tρ = t′ρ′ : Aρ
Γ |⊧ σ : Γ_{0}  :⟺ Γ |⊧ σ = σ : Γ_{0}
Γ |⊧ σ = σ′ : Γ_{0} :⟺ Γ |⊧ and Γ_{0} |⊧ and
∀Δ ⊧ ρ = ρ′ : Γ. Δ ⊧ σρ = σ′ρ′ : Γ_{0}

Lemma 11 (Validity: weak implies strong). If Γ ⊩ J then Γ |⊧ J.

Proof. The hypothesis is ∀Δ ⊢ ρ = ρ′ : Γ. Δ ⊢ tρ = t′ρ′ : Aρ. Assume Θ ⊧ ρ = ρ′ : Γ and Δ ⊢ θ = θ′ : Θ and show Δ ⊢ tρθ = t′ρ′θ′ : Aρθ. By Lemma 10 Δ ⊢ ρθ = ρ′θ′ : Γ, hence our goal follows by assumption.

Corollary 4. If Γ ⊢ J then Γ |⊧ J.

Lemma 12. Γ ρ_{id} ⊧ ρ_{id} = ρ_{id} : Γ.

Corollary 5. If Γ ⊢ t : A then Γ ρ_{id} ⊧ tρ_{id} : Aρ_{id}.

Putting things together:

Theorem 3 (Soundness of algorithmic equality). If Γ ⊢ t, t′ : A and Γ ρ_{id} ⊢ tρ_{id} = t′ρ_{id} ⇑ Aρ_{id} then Γ ⊢ t = t′ : A.

Proof. We have Γ ⊢ t : A ◯^{R} Γ ρ_{id} ⊢ tρ_{id} : Aρ_{id} and Γ ⊢ t′ : A ◯^{R} Γ ρ_{id} ⊢ t′ρ_{id} : Aρ_{id}. Also ⊧ Γ ρ_{id}, Γ ρ_{id} ⊧ Aρ_{id}, Γ ρ_{id} ⊧ tρ_{id} : Aρ_{id}, and Γ ρ_{id} ⊧ t′ρ_{id} : Aρ_{id}. By semantic soundness of the algorithm, Γ ρ_{id} ⊧ tρ_{id} = t′ρ_{id} : Aρ_{id} which implies Γ ρ_{id} ⊢ tρ_{id} = t′ρ_{id} : Aρ_{id}, hence Γ ⊢ t : A ◯^{R} Γ ρ_{id} ⊢ t′ρ_{id} : Aρ_{id}. This entails Γ ⊢ t = t′ : A.

9 On Termination

What remains to show is termination of the algorithmic equality: Given two terms of the same type, the algorithm terminates on their values. We have already seen that the values of well-typed terms are reifiable, hence the NbEalgorithm, which compares the results of reification, is terminating. We would like to extend this result to algorithmic equality, which performs reification incrementally. One would expect a statement similar to Lemma 7:

If Δ ⊢ d ↘ ⇑ X and Δ ⊢ d′ ↘ ⇑ X then the query Δ ⊢ d = d′ ⇑ X terminates.

Generalizing this statement to the mutually defined notions of reification and algorithmic equality (⇓ and ⇑ Set), we see that the proof fails since during reification of d′, context and type diverge from Δ and X. (Similar considerations lead us to the definition of Ⓢ in Section 5.2.)

The skeleton of the algorithmic derivation is already determined by the derivation of Δ ⊢ d ↘ ⇑ X. Yet we have to show that the application f′ · x_{Δ} is terminating in aq-ext. Somehow we have to exploit that d′ originates from a well-typed term, thus, Δ ⊢ d′ : X and even Δ ⊧ d : X both hold. But it is unclear how to make use of these facts in a termination proof.

10 Conclusion and Related Work

We have presented a bidirectional incremental βη-equality algorithm for a dependent type theory with predicative universes and verified it using NbE-techniques. The algorithm is formulated with respect to an abstract representation of values which supports several implementations. In Sec. 8 we had to exclude the representation via higher order abstract syntax, which was used in an early version of Agdalight, a predecessor of Agda 2. In the future we want to explore how to generalize our proof so that we also cover this implementation technique. Furthermore, we want to close the gap and prove termination of the algorithm as well as soundness and completeness of type checking.

Some complications in the verification vanish if we restrict to a concrete, term-like implementation of values, for instance, closures [Coq96,AC08]. Closures are a special case of explicit substitutions, hence, soundness of algorithmic equality is trivial: each algorithmic rule can be replaced by a sequence of declarative rules. Termination also becomes apparent: algorithmic equality works only on well-typed terms, which are normalizing.

Related work. The current proof uses similar techniques to those in our previous work on NbE [ACD07]. However, there are several differences, in order to deal with contextual reification we here need a Kripke model instead of a plain PER model.

Goguen [Gog94] proves decidability of UTT using typed operational semantics. He treats η, universes, and even inductive types and a impredicative universe of propositions. Showing soundness and completeness of his syntactic Kripke model he establishes subject reduction, confluence, and strong normalization, which imply decidability. However, he is not concerned about particular algorithms. Since his approach is based on η-reduction instead of η-expansion, it is not clear whether it scales to a unit type with extensional equality.

Harper and Pfenning [HP05] present an incremental bidirectional βη-equality algorithm for LF using erasure of dependencies; this does not extend to large eliminations. Chapman, Altenkirch, and McBride [CAM07] share their algorithm with us. They describe an implementation, but no verification.

Grégoire and Leroy [GL02] have implemented an incremental β-conversion test for the Calculus of Inductive Constructions based on “normalization by execution”. Values are computed by compiling (open!) expression to Caml byte code. The result of executing the code is then read back to a β-normal expression. The soundness of this efficient form of evaluation has been formally verified in Coq. We expect that our and their work can be combined to obtain an efficient βη-conversion test. To this end, one needs to instantiate the syntactical applicative structure D to machine code and define contextual reification of code, similar to Grégoire and Leroy’s read back function.

Acknowledgments. Thanks to the anonymous referees who gave insightful comments and pointed to the problem of termination.

References

[AAD07] Andreas Abel, Klaus Aehlig, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with one universe. In Marcelo Fiore, editor, Proc. of the 23rd Conf. on the Mathematical Foundations of Programming Semantics (MFPS XXIII), volume 173 of Electr. Notes in Theor. Comp. Sci., pages 17–39. Elsevier, 2007.

[AC07] Andreas Abel and Thierry Coquand. Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Fundam. Inform., 77(4):345–395, 2007. TLCA’05 special issue.

[AC08] Thorsten Altenkirch and James Chapman. Big step normalisation. Draft, available on the authors’ homepages., 2008.

[ACD07] Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pages 3–12. IEEE Computer Soc. Press, 2007.

[ACD08] Andreas Abel, Thierry Coquand, and Peter Dybjer. A semantic βη-equality algorithm for Martin-Löf Type Theory (extended version). Technical report, Ludwig-Maximilians-University Munich, 2008. http://www.tcs.ifi.lmu.de/˜ abel/semEqTR.pdf.

[Bar84] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam, 1984.

[BL84] Kim B. Bruce and Giuseppe Longo. On combinatory algebras and their expansions. Theor. Comput. Sci., 31:31–40, 1984.

[BS91] Ulrich Berger and Helmut Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 203–211, July 1991.

[CAM07] James Chapman, Thorsten Altenkirch, and Conor McBride. Epigram reloaded: a standalone typechecker for ETT. In Marko C. J. D. van Eekelen, editor, Revised Selected Papers from the 6th Symp. on Trends in Functional Programming, TFP 2005, volume 6 of Trends in Functional Programming, pages 79–94. Intellect, 2007.

[Coq94] Catarina Coquand. From semantics to rules: A machine assisted analysis. In Egon Börger, Yuri Gurevich, and Karl Meinke, editors, Proc. of the 7th Wksh. on Computer Science Logic, CSL ’93, volume 832 of Lect. Notes in Comput. Sci., pages 91–105. Springer-Verlag, 1994.

[Coq96] Thierry Coquand. An algorithm for type-checking dependent types. In Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), volume 26 of Science of Computer Programming, pages 167–177. Elsevier Science, May 1996.

[CPT05] Thierry Coquand, Randy Pollack, and Makoto Takeyama. A logical framework with dependently typed records. Fundam. Inform., 65(1-2):113–134, 2005.

[Dan99] Olivier Danvy. Type-directed partial evaluation. In John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann, editors, Partial Evaluation – Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998, volume 1706 of Lect. Notes in Comput. Sci., pages 367–411. Springer-Verlag, 1999.

[Dyb96] Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs (TYPES’95), Torino, Italy, number 1158 in Lect. Notes in Comput. Sci., pages 120–134. Springer-Verlag, 1996.

[Dyb00] Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525–549, 2000.

[GL02] Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Proc. of the 7th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP ’02), volume 37 of SIGPLAN Notices, pages 235–246. ACM Press, September 2002.

[Gog94] Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994. Available as LFCS Report ECS-LFCS-94-304.

[HP05] Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic, 6(1):61–101, 2005.

[INR07] INRIA. The Coq Proof Assistant, Version 8.1. INRIA, 2007. http://coq.inria.fr/.

[Ler06] Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, Proc. of the 33rd ACM Symp. on Principles of Programming Languages, POPL 2006, pages 42–54. ACM Press, 2006.

[ML75] Per Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. In S. Kanger, editor, Proceedings of the 3rd Scandinavian Logic Symposium, pages 81–109, 1975.

[ML92] Per Martin-Löf. Substitution calculus. Unpublished notes from a lecture in Göteborg, November 1992.

[Nor07] Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-41296 Göteborg, Sweden, September 2007.

[Pit06] A. M. Pitts. Alpha-structural recursion and induction. Journal of the ACM, 53:459–506, 2006.

[Pol94] Robert Pollack. Closure under alpha-conversion. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs: International Workshop, Nijmegen, May 1993, Selected Papers, number 806 in LNCS, pages 313–332. Springer-Verlag, 1994.

[PS99] Frank Pfenning and Carsten Schürmann. System description: Twelf - a metalogical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lect. Notes in Art. Intell., pages 202–206, Trento, Italy, July 1999. Springer-Verlag.

[PT98] Benjamin C. Pierce and David N. Turner. Local type inference. In POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, 1998.

[Shi05] Mark Shinwell. The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, University of Cambridge, 2005.

[SS08] Carsten Schürmann and Jeffrey Sarnat. Structural logical relations. In Frank Pfenning, editor, Proc. of the 23nd IEEE Symp. on Logic in Computer Science (LICS 2008), 2008.