Typed Applicative Structures and Normalization by Evaluation for System F^{ω}

Andreas Abel

Department of Computer Science Ludwig-Maximilians-University Munich

Abstract. We present a normalization-by-evaluation (NbE) algorithm for System F^{ω} with βη-equality, the simplest impredicative type theory with computation on the type level. Values are kept abstract and requirements on values are kept to a minimum, allowing many different implementations of the algorithm. The algorithm is verified through a general model construction using typed applicative structures, called type and object structures. Both soundness and completeness of NbE are conceived as an instance of a single fundamental theorem.

1 Introduction and Related Work

In theorem provers, such as Coq [INR07], Agda [Nor07], Epigram [CAM07], which are based on intensional type theory, checking the validity of proofs or typings relies on deciding equality of types. Types are recognized as equal if they have the same normal form. This is why normalization plays a key role in type theories, such as the Calculus of Constructions (CC) which underlies Coq, and Martin-Löf Type Theory which is the basis of Agda and Epigram. The hardwired type equality of Coq is restricted to computational equality (β), as opposed to Agda and Epigram which have βη-equality. Our goal is to integrate η-laws into Coq’s equality. As a prerequisite, we have to show normalization for the βη-CC.

Normalization by evaluation (NbE) [BS91,Dan99] is a systematic method to perform βη-normalization. In a first step, the object t of type T is evaluated. The resulting value d is then reified to an η-long β-normal form v. The reification process is directed by the shape of type T. NbE has proven a valid tool to structure extensional normalization, especially in the notoriously difficult case of sum types [ADHS01,BCF04,Bar08]. In previous work [ACD07], we have adapted NbE to a dependent type theory with one predicative universe and judgmental βη-equality. What is the challenge when stepping up to impredicativity? Predicative type theories allow to define the semantics of types from below via induction-recursion [Dyb00], and the reification function can be defined by induction on types. This fails in the presence of impredicativity, where one first has to lay out a lattice of semantic type candidates and then define impredicative quantification using an intersection over all candidates [GLT89]. Hence, the semantic type structure is not inductive, and reification cannot be defined by induction on types. There are at least two ways out of this dilemma: Altenkirch, Hofmann, and Streicher [AHS96] construct a total normalization function type-wise while building a model for System F. In previous work [Abe08], I have conceived reification as a deterministic relation between value d and normal form v and their type T, and showed through a model construction that it corresponds to a total function.

In this work, we are moving one step closer to NbE for the CC: we are considering the simplest type system which features impredicativity and computation on the type level: the higher-order polymorphic lambda-calculus F^{ω}. It adds to the problem of impredicativity the difficulty that types are no longer fixed syntactic expressions as in System F, but they need to be normalized as well. Of course, due to the simply-kinded structure of types they could be kept in long normal form using simple structural normalization. This does not scale to the CC, so we resist this temptation.

In our solution, reification of objects is directed by type values A. Syntactic types T are interpreted by a pair (A, A) of a type value A and a semantic type A which is a set of objects that are reifiable at type A. Furthermore, type value A reifies to a normal form V which is βη-equal to T. These considerations lead us to the concept of a type structure which captures the similarities between syntactic types, type values, and semantic types. Consequently, syntactic objects and their values both form an object structure over a type structure, the syntactical type structure in case of syntactic objects and the structure of type values in case of (object) values.

Or notions of type and object structures are very general, in essence typed versions of Barendregt’s syntactical applicative structures [Bar84, Def. 5.3.1]. The fundamental theorems we prove are also very general since we do not fix an interpretation of types; we only require that semantic types inhabit a candidate space. By choosing different candidate spaces we can harvest different results from the same fundamental theorem, e. g., soundness of NbE, completeness of NbE, or weak normalization of β- or βηreduction [Abe08].

In the following developments we omit most proofs due to lack of space. They can be found in the full version of this article on the author’s homepage [Abe09].

Preliminaries. Contexts Ξ, Θ, Γ, Δ, Φ, Ψ are functions from variables to some codomain. We write ⋄ for the totally undefined function and Φ, x: a for the function Φ′ with domain dom(Φ) ⊎ {x} such that Φ′(x) = a and Φ′(y) = Φ(y) for y ≠ x. We say Ψ′ extends Ψ, written Ψ′ ≤ Ψ, if Ψ′(x) = Ψ(x) for all x ∈ dom(Ψ).

Families T_{Ξ} indexed by a context Ξ are always understood to be Kripke, i. e., Ξ′ ≤ Ξ implies T_{Ξ} ⊆ T_{Ξ′}. The notion Kripke family is also used for maps M_{Ξ}. There it implies that M does not depend on the context parameter, i. e., M_{Ξ}(a) = M_{Ξ′}(a) for a ∈ dom(M_{Ξ}) and Ξ′ ≤ Ξ. (Note that dom(M_{Ξ}) ⊆ dom(M_{Ξ′}) since M is Kripke.)

We write (a ∈ A) → B(a) for the dependent function space {f ∈ A → ⋃_{a∈A} B(a) | f(a) ∈ B(a) for all a ∈ A}.

2 Syntax

In this section, we present the syntax and inference rules for System F^{ω}. The system consists of three levels: On the lowest level there live the objects, meaning polymorphic, purely functional programs. On the middle level live the types of objects, and the type constructors, which are classified by kinds that themselves inhabit the highest level.

Kinding Ξ ⊢ T : κ. “In context Ξ, type T has kind κ.”

\overline{Ξ ⊢ C : Σ(C)}  \overline{Ξ ⊢ X : Ξ(X)}

\frac{Ξ, X:κ ⊢ T : κ′}{Ξ ⊢ λX:κ. T : κ → κ′}  \frac{Ξ ⊢ T : κ → κ′  Ξ ⊢ U : κ}{Ξ ⊢ T U : κ′}

Type equality Ξ ⊢ T = T′ : κ. “In context Ξ, types T and T′ are βη-equal of kind κ.” Congruence closure of the following β- and η-axioms.

\frac{Ξ, X:κ ⊢ T : κ′  Ξ ⊢ U : κ}{Ξ ⊢ (λX:κ. T) U = T [U/X] : κ′}  \frac{Ξ ⊢ T : κ → κ′}{Ξ ⊢ λX:κ. T X = T : κ → κ′} X ∉ dom(Ξ)

Typing Ξ; Γ ⊢ t : T. “In contexts Ξ, Γ, object t has type T.”

\frac{Ξ ⊢ Γ}{Ξ; Γ ⊢ x : Γ (x)}  \frac{Ξ; Γ, x:U ⊢ t : T}{Ξ; Γ ⊢ λx:U. t : U → T}  \frac{Ξ; Γ ⊢ t : U → T  Ξ; Γ ⊢ u : U}{Ξ; Γ ⊢ t u : T}
\frac{Ξ ⊢ T : κ → ⋆  Ξ, X:κ; Γ ⊢ t : T X}{Ξ; Γ ⊢ ΛX:κ. t : ∀^{κ}T} X ∉ dom(Ξ)  \frac{Ξ; Γ ⊢ t : ∀^{κ}T  Ξ ⊢ U : κ}{Ξ; Γ ⊢ t U : T U}

\frac{Ξ; Γ ⊢ t : T Ξ ⊢ T = T′ : ⋆}{Ξ; Γ ⊢ t : T′}

Object equality Ξ; Γ ⊢ t = t′ : T. “In contexts Ξ, Γ, objects t and t′ are βη-equal of type T.” Congruence closure of the following β- and η-axioms.

\frac{Ξ; Γ, x:U ⊢ t : T  Ξ; Γ ⊢ u : U}{Ξ; Γ ⊢ (λx:U. t) u = t[u/x] : T}  \frac{Ξ; Γ ⊢ t : U → T}{Ξ; Γ ⊢ λx:U. t x = t : U → T} x ∉ dom(Γ)
\frac{Ξ, X:κ; Γ ⊢ t : T  Ξ ⊢ U : κ}{Ξ; Γ ⊢ (ΛX:κ. t) U = t[U/X] : T [U/X]}  \frac{Ξ; Γ ⊢ t : ∀^{κ}T}{Ξ; Γ ⊢ ΛX:κ. t X = t : ∀^{κ}T} X ∉ dom(Ξ)

Fig. 1. F^{ω}: kinding, type equality, typing, object equality.

Kinds κ ∈ Ki are given by the grammar κ ::= ⋆ | κ → κ′. Kind ⋆ classifies type constructors which are actually types, and kind κ → κ′ classifies the type constructors which map type constructors of kind κ to type constructors of kind κ′. In the following, we will refer to all type constructors as types.

Assume a countably infinite set of type variables TyVar whose members are denoted by X, Y, Z. Kinding contexts Ξ, Θ ∈ KiCxt are partial maps from the type variables into Ki. The set TyCst = {→, ∀^{κ} | κ ∈ Ki} contains the type constants C. Their kinds are given by the signature Σ ∈ TyCst → Ki defined by Σ(→) = ⋆ → ⋆ → ⋆ and Σ(∀^{κ}) = (κ → ⋆) → ⋆ for all κ ∈ Ki.

Types are given by the grammar T, U, V ::= C | X | λX: κ. T | T U, where X ∈ TyVar, and form a “simply-kinded” lambda calculus. As usual, we write T → U for → T U. Objects are given by the grammar t, u, v ::= x | λx: T. t | t u | ΛX: κ. t | t U and form a polymorphic lambda-calculus with type abstraction and type application. Herein, object variables x are drawn from a countably infinite set ObjVar which is disjoint from TyVar. We write b[a/x] for capture-avoiding substitution of a for variable x in syntactic expression b, and FV for the function returning the set of all free type and object variables of a syntactic expression.

The judgements and inference rules of F^{ω} are displayed in Figure 1. Herein, the auxiliary judgement Ξ ⊢ Γ, read “Γ is a well-formed typing context in Ξ”, is defined as Ξ ⊢ Γ (x) : ⋆ for all x ∈ dom(Γ).

3 Abstract Normalization by Evaluation

In the following, we present normalization by evaluation (NbE) for System F^{ω} for an abstract domain D of values and type values. This leaves the freedom to implement values in different ways, e. g., β-normal forms, weak head normal forms (as in Pollack’s constructive engine [Pol94]), closures (as in Coquand’s type checker [Coq96]), tagged functions (Epigram 2 [CAM07]) or virtual machine instructions (compiled reduction in Coq [GL02]). All implementations of values that satisfy the interface given in the following can be used with our NbE algorithm, and in this article we provide a framework to prove all these implementations correct.

In this section, we will understand functions in terms of a programming language, i. e., partial and possibly non-terminating. We unify the syntax of kinds, types, and objects into a grammar of expressions Exp. Let Var = TyVar ∪ ObjVar.

Expressions Exp ∋ M, N ::= ⋆ | C | X | x | λx:M. N | ΛX:M. N | M N
Values  D ∋ d, e, f, A, B, F, G (abstract)

Environments Env are finite maps from variables to values. Look-up of variable x in environment ρ is written ρ(x), update of environment ρ with new value v for variable x is written ρ[x ↦ v], and the empty environment is written ⋄. The call fresh(ρ) returns a variable x which is not in dom(ρ).

Application and evaluation (see Fig. 2) make values into a syntactical applicative structure [Bar84, 5.3.1], provided the equations below are satisfied. Such structures will appear later, in a sorted setting, as type and object structures (defs. 1 and 13). Note that establishing the laws of evaluation can be arbitrarily hard, e. g., if ⦇ ⦈ involves an optimizing compiler.

Values are converted back to expressions through reification. However, this process can only be implemented for term-like value domains, in particular, we require an embedding of variables into D, and an analysis neView of values that arise as iterated application of a variable (a so-called neutral value) or as iterated application of a constant (a constructed value). Some constructed values are types or kinds, they are analyzed by tyView, which can actually be defined from neView.

Values d of type V in context Δ, which assigns type values to variables, are reified by a call to ↘^{⇑}(Δ, d, V). It is mutually defined with ↘^{⇑}(Δ, n) which returns the normal form M and type V of neutral value n. Later in this article, reification will be presented as two relations Δ ⊢ d ↘ M ⇓⇑ V such that Δ ⊢ d ↘ M ⇑ V iff ↘^{⇑}(Δ, d, V) = M and Δ ⊢ d ↘ M ⇓ V iff ↘^{⇓}(Δ, d) = (M, V).

NbE is now obtained as reification after evaluation. For closed expressions M of type or kind N we define nbe(M, N) = ↘^{⇑}(⋄, ⦇M⦈_{⋄}, tyView⦇N⦈_{⋄}).

Applicative structure D of values.

Application ·  : D → D → D
Evaluation ⦇ ⦈  : Exp → Env → D
⦇x⦈_{ρ}  = ρ(x)
⦇λx:M. N⦈_{ρ} · d = ⦇N⦈_{ρ[x↦d]}
⦇X⦈_{ρ}  = ρ(X)
⦇ΛX:M. N⦈_{ρ} · G = ⦇N⦈_{ρ[X↦G]}
⦇M N⦈_{ρ}  = ⦇M⦈_{ρ} · ⦇N⦈_{ρ}

D is term-like.

Embedding var : Var → D
View as neutral NeView ∋ n  ::= C | X | x | e d
neView  : D → NeView
neView⦇C⦈_{ρ}  = C
neView(var X)  = X
neView(var x)  = x
neView(e · d)  = e d if neView e is defined
View as type TyView ∋ V ::= ⋆ | A → B | ∀^{κ}F
tyView  : D → TyView
tyView ⦇⋆⦈_{ρ}  = ⋆
tyView ⦇M → N⦈_{ρ} = tyView ⦇M⦈_{ρ} → tyView ⦇N⦈_{ρ}
tyView ⦇∀^{κ}M⦈_{ρ}  = ∀^{κ} tyView ⦇M⦈_{ρ}

Reification.

↘^{⇑}  : Env → D → TyView → Exp
↘^{⇑}(Δ, f, A → B) = let x  = fresh(Δ) (U, ) = ↘^{⇓}(Δ, neView A)

in λx:U. ↘^{⇑}(Δ[x ↦ A], f · var x, tyView B)

↘^{⇑}(Δ, d, ∀^{κ}F) = let X = fresh(Δ) in ΛX:κ. ↘^{⇑}(Δ[X ↦ κ], d · var X, tyView(F · var X))
↘^{⇑}(Δ, e, ⋆)  = let (M, ) = ↘^{⇓}(Δ, neView e) in M
↘^{⇓}  : Env → NeView → Exp × TyView
↘^{⇓}(Δ, C)  = (C, Σ(C))
↘^{⇓}(Δ, X)  = (X, tyView(Δ(X)))
↘^{⇓}(Δ, x)  = (x, tyView(Δ(x)))
↘^{⇓}(Δ, e d)  = let (M, V) = ↘^{⇓}(Δ, e) in case V of
A → B ↦ (M (↘^{⇑}(Δ, d, tyView A)), tyView B)
∀^{κ}F ↦ (M (↘^{⇑}(Δ, d, κ)), tyView(F · d))

Normalization by evaluation. nbe(M, N) = ↘^{⇑}(⋄, ⦇M⦈_{⋄}, tyView⦇N⦈_{⋄})

Fig. 2. Specification of an NbE algorithm.

A concrete instance of NbE is obtained by defining a recursive data type D with the constructors:

Constr : TyCst → D^{∗} → D
Ne : Var → D^{∗} → D
Abs : (D → D) → D

Application, evaluation, and variable embedding are given by the following equations.

(Constr C Gs) · G = Constr C (Gs, G)
(Ne x ds)  · d = Ne x (ds, d)
(Abs f)  · d = f d
⦇λx:M. N⦈_{ρ}  = Abs f  where f d = ⦇N⦈_{ρ[x↦d]}
⦇ΛX:M. N⦈_{ρ}  = Abs f  where f G = ⦇N⦈_{ρ[X↦G]}
⦇C⦈_{ρ}  = Constr C ()

Variables are embedded via var x = Ne x (). This instance of NbE is now easily completed using the equations of the specification, and can be implemented directly in Haskell.

In this article we show that any instance of the NbE-specification terminates with the correct result for well-formed expressions of F^{ω}, i. e., we show the following two properties:

1. Soundness: if ⊢ M : N, then ⊢ nbe(M, N) = M : N.

2. Completeness: if ⊢ M : N and ⊢ M′ : N, then nbe(M, N) = nbe(M′, N) (same expression up to α).

In contrast to the untyped presentation in this section, which saves us from some repetition, we will distinguish the three levels of F^{ω} consequently in the remainder of the article.

4 Type Structures

In this section, we define type structures as an abstraction over syntactic types, type values, and semantic types. Type structures form a category which has finite products. Let Ty_{Ξ}^{κ} = {T | Ξ ⊢ T : κ}.

Definition 1 (Type structure). An (F^{ω}) type structure is a tuple (T , Cst, App, [[ ]] ) where T is a Kripke family T_{Ξ}^{κ} of sets with the following Kripke families of maps:

Cst_{Ξ}  ∈ (C ∈ TyCst) → T_{Ξ}^{Σ(C)}
App_{Ξ}^{κ→κ′} ∈ T_{Ξ}^{κ→κ′} → T_{Ξ}^{κ} → T_{Ξ}^{κ′}

Usually, we will just write F · G for App_{Ξ}^{κ→κ′}(F, G). Let ρ ∈ T_{Θ}^{Ξ} iff ρ(X) ∈ T_{Θ}^{Ξ(X)} for all X ∈ dom(Ξ). The interpretation function has the following properties:

\begin{aligned}[[ ]] & ∈ & Ty_{Ξ}^{κ} → T_{Θ}^{Ξ} → T_{Θ}^{κ} \\ [[C]]_{ρ} & = & Cst_{Θ}(C) \\ [[X]]_{ρ} & = & ρ(X) \end{aligned}  \begin{aligned}[[λX:κ. T]]_{ρ} · G & = & [[T]]_{ρ[X↦G]} \\ [[T U]]_{ρ} & = & [[T]]_{ρ} · [[U]]_{ρ} \\ [[T [U/X]]]_{ρ} & = & [[T]]_{ρ[X↦[[U]]_{ρ}]} (∗) \end{aligned}

If the condition (∗) is fulfilled, we speak of a combinatory type structure, since (∗) is a characterizing property of combinatory algebras. The condition (∗) is only necessary since we chose to use eager substitution in the inference rules of F^{ω}, it can be dropped when switching to explicit substitutions [ACD08].

We use “interpretation” and “evaluation” synonymously. Note that while the equations determine the interpretation of constants, variables, and application, there is some freedom in the interpretation of functions [[λX: κ. T]]_{ρ}. It could be lambda-terms (taking T = Ty), set-theoretical functions (see Def. 20), functional values in an interpreter, machine code etc.

Since Cst_{Ξ} is independent of Ξ, we have Cst_{Ξ} = Cxt_{⋄}, we usually suppress the index Ξ in Cst_{Ξ}. We may even drop Cst altogether, i. e., we just write → ∈ T_{Ξ}^{⋆→⋆→⋆} instead of Cst(→) ∈ T_{Ξ}^{⋆→⋆→⋆}.

To avoid ambiguities when different type structures are in scope, we may write →_{T}, ∀_{T}^{κ}, ·_{T} and T [[ ]] to emphasize that we mean the type structure operations of T .

Simple examples of type structures are Ty and Ty modulo β, βη, or judgmental equality. In these instances, the interpretation function is parallel substitution.

Definition 2 (Type structure morphism). Given two type structures S and T , a type structure morphism M : S → T is a Kripke family of maps M_{Ξ}^{κ} ∈ S_{Ξ}^{κ} → T_{Ξ}^{κ} that commute with the operations of S, i. e.,

\begin{aligned}M_{Ξ}^{κ}(C_{S}) & = & C_{T} \\ M_{Ξ}^{κ′}(F ·_{S} G) & = & M_{Ξ}^{κ→κ′}(F) ·_{T} M_{Ξ}^{κ}(G) \\ M_{Θ}^{κ}(S[[T]]_{ρ}) & = & T [[T]]_{M_{Θ}^{Ξ}∘ρ} where (M_{Θ}^{Ξ} ∘ ρ)(X) := M_{Θ}^{Ξ(X)}(ρ(X)). \end{aligned}

The Cartesian product S × T of two type structures forms a type structure with pointwise application and tupled interpretation. The two projections π_{1} : S × T → S and π_{2} : S × T → T are trivially type structure morphisms, and × is a product in the category of type structures and their morphisms.

4.1 Type Substructures and the Fundamental Theorem for Kinding

Definition 3 (Type substructure). The Kripke family S_{Ξ}^{κ} ⊆ T_{Ξ}^{κ} is a type substructure of T if all of T ’s operations are well-defined on S, i. e., C_{T} ∈ S_{Ξ}^{κ}, ·_{T} ∈ S_{Ξ}^{κ→κ′} → S_{Ξ}^{κ} → S_{Ξ}^{κ′}, and T [[ ]] ∈ Ty_{Ξ}^{κ} → S_{Θ}^{Ξ} → S_{Θ}^{κ}.

In the following we simply write S ⊆ T to mean S_{Ξ}^{κ} ⊆ T_{Ξ}^{κ} for all κ, Ξ.

Lemma 1 (Projection type substructure). If S ⊆ T_{1} × T_{2} is a type substructure, so are π_{1}(S) ⊆ T_{1} and π_{2}(S) ⊆ T_{2}.

Definition 4 (Function space). We write K ∈ T̂^{κ} if K is a Kripke family of subsets K_{Ξ} ⊆ T_{Ξ}^{κ}. Given K ∈ T̂^{κ} and K′ ∈ T̂^{κ′} we define the Kripke function space

(K →T̂ K′)_{Ξ} = {F ∈ T_{Ξ}^{κ→κ′} | F · G ∈ K′_{Ξ′} for all Ξ′ ≤ Ξ and G ∈ K_{Ξ′}}

If no ambiguities arise, we write → for →T̂.

Definition 5 (Induced type structure). Let T be a type structure and S ⊆ T be Kripke. If C_{T} ∈ S_{Ξ}^{Σ(C)} for all constants C and S_{Ξ}^{κ→κ′} = (S^{κ} →T̂ S^{κ′})_{Ξ} then S is called induced or an induced type substructure of T (see Thm. 1).

Such an S is called induced since it is already determined by the choice of the denotation of the base kind S^{⋆}.

Theorem 1 (Fundamental theorem of kinding). Let T be a type structure. If S ⊆ T is induced, then S is a type substructure of T .

Proof. We mainly need to show that evaluation is well-defined. This is shown by induction on the kinding derivation, as usual. ⊓ ⊔

4.2 NbE for Types and Its Soundness

We are ready to define the reification relation for type values and show that NbE, i. e., the composition of evaluation of a syntactic type T and reification to a normal form V, is sound, i. e., T and V are judgmentally equal. As a byproduct, we show totality of NbE on well-kinded types. The structure T of type values is left abstract. However, not every T permits reification of its inhabitants. It needs to include the variables which need to be distinguishable from each other and other type values. Neutral types, i. e., of the shape X · G, need to be analyzable into head X and spine G. We call a suitable T term-like; on such a T we can define contextual reification [ACD08,Abe08].

Definition 6 (Term-like type structure). A type structure T is term-like if there exists exists a Kripke family of maps Var_{Ξ} ∈ (X ∈ dom(Ξ)) → T_{Ξ}^{Ξ(X)} and a Kripke family of partial maps

View_{Ξ}^{κ} ∈ T_{Ξ}^{κ} ⇀ {(C, G) ∈ TyCst × T_{Ξ}^{κ} | Σ(C) = κ → κ}
+ {(X, G) ∈ TyVar × T_{Ξ}^{κ} | Ξ(X) = κ → κ}

such that View(F) = (C, G) iff F = Cst(C) · G (“F is constructed”) and View(F) = (X, G) iff F = Var(X) · G (“F is neutral”).

Usually, we drop the index Ξ to Var. We may write Var_{T} to refer to the variable embedding of type structure T .

Definition 7 (Type reification). On a term-like type structure T we define reification relations

Ξ ⊢ F ↘ V ⇑ κ  in Ξ, F reifies to V at kind κ,
Ξ ⊢ H ↘ U ⇓ κ  in Ξ, H reifies to U, inferring kind κ,

(where F, H ∈ T_{Ξ}^{κ} with H neutral or constructed, and V, U ∈ Ty_{Ξ}^{κ}) inductively by the following rules:

\overline{Ξ ⊢ X ↘ X ⇓ Ξ(X)}  \frac{Ξ ⊢ H ↘ U ⇓ κ → κ′  Ξ ⊢ G ↘ V ⇑ κ}{Ξ ⊢ H · G ↘ U V ⇓ κ′}

\overline{Ξ ⊢ C ↘ C ⇓ Σ(C)}  \frac{Ξ ⊢ H ↘ U ⇓ ⋆}{Ξ ⊢ H ↘ U ⇑ ⋆}  \frac{Ξ, X:κ ⊢ F · X ↘ V ⇑ κ′}{Ξ ⊢ F ↘ λX:κ. V ⇑ κ → κ′}

Reification is deterministic in the following sense: For all Ξ, κ, F (inputs) and neutral or constructed H (input) there is at most one V (output) such that Ξ ⊢ F ↘ V ⇑ κ and at most one U and κ′ (outputs) such that Ξ ⊢ H ↘ U ⇓ κ′.

Seen as logic programs with inputs and outputs as indicated above, these relations denote partial functions, where ↘^{⇑} is defined by cases on the kind κ and and ↘^{⇓} by cases on the neutral value H.

We continue by constructing a model of the kinding rules which proves soundness of NbE for types. Kinds κ are interpreted as sets G_{Ξ}^{κ} of pairs (F, T) glued together [CD97] by reification, i. e., the type value F reifies to syntactic type T up to βη-equality. Function kinds are interpreted via Tait’s function space (see Def. 4), thus, the fundamental theorem of kinding yields that G is indeed a type structure.

Definition 8 (Glueing candidate). Fix a term-like type structure T . We define the families \underline{Gl}, \overline{Gl} ⊆ T × Ty by

\overline{Gl}_{Ξ}^{κ} = \{(F, T) ∈ T_{Ξ}^{κ} × Ty_{Ξ}^{κ} | Ξ ⊢ F ↘ V ⇑ κ and Ξ ⊢ T = V : κ\},
\underline{Gl}_{Ξ}^{κ} = \{(H, T) ∈ T_{Ξ}^{κ} × Ty_{Ξ}^{κ} | Ξ ⊢ H ↘ U ⇓ κ and Ξ ⊢ T = U : κ\}.

A family S with \underline{Gl}^{κ} ⊆ S^{κ} ⊆ \overline{Gl}^{κ} is called a glueing candidate.

Def. and Lem. 2 (Kind candidate space) \underline{Gl}^{κ}, \overline{Gl}^{κ} form a kind candidate space, i. e., satisfy the following laws, where we write \underline{κ} for \underline{Gl}^{κ} and \overline{κ} for \overline{Gl}^{κ}.

\underline{⋆} ⊑ \overline{⋆},  \underline{κ} → \overline{κ′} ⊑ \overline{κ → κ′},  \underline{κ → κ′} ⊑ \overline{κ} → \underline{κ′}.

Def. and Lem. 3 (Glueing type structure) Given a type structure T , we define G ⊆ T × Ty by G_{:}^{⋆} = \underline{⋆} and G_{:}^{κ→κ′} = G^{κ} →{ \atop T ×Ty} G^{κ′}. G is a glueing candidate, i. e.,

\underline{Gl}^{κ} ⊆ G^{κ} ⊆ \overline{Gl}^{κ} for all κ.

Since G is induced, by the fundamental theorem of kinding it is a type substructure of T × Ty. Thus, for all T ∈ Ty_{Ξ}^{κ}, G[[T]]_{Var_{G}} = (T [[T]]_{Var_{T}} , T) ∈ G_{Ξ}^{κ} ⊆ \overline{Gl}_{Ξ}^{κ}, entailing soundness.

Theorem 4 (Soundness of NbE for types). Let T be a term-like type structure. If Ξ ⊢ T : κ then there is a V ∈ Ty_{Ξ}^{κ} such that Ξ ⊢ T [[T]]_{Var_{T}} ↘ V ⇑ κ and Ξ ⊢ T = V : κ.

5 Type Groupoids

Completeness of NbE means that it models judgmental type equality, i. e., if Ξ ⊢ T = T′ : κ then Ξ ⊢ [[T]] ↘ V ⇑ κ and Ξ ⊢ [[T′]] ↘ V ⇑ κ. Completeness will be shown by a fundamental theorem of type equality. Judgmental equality is usually modelled by partial equivalence relations (PERs), which can be seen as groupoids. Hence, we introduce the notion of a groupoidal type structure, or type groupoid. The advantage over PERs is that we can directly reuse the fundamental theorem of kinding, instantiated to a groupoidal type structure ^{2}T of pairs of types, instead of having to prove this theorem again for kinds modelled as PERs.

A groupoid is a set G with inversion ^{−1} : G → G and partial but associative composition ∗ : G×G → G such that a^{−1}∗a and a∗a^{−1} are always defined, and if a∗b is defined, then a∗b∗b^{−1} = a, and a^{−1} ∗a∗b = b. One easily shows that (a^{−1})^{−1} = a and if a∗b is defined then (a∗b)^{−1} = b^{−1} ∗a^{−1}. Examples of groupoids include partial equivalence relations R, where (s, t)^{−1} = (t, s) and (r, s) ∗ (s, t) = (r, t), and any set S with the trivial groupoidal structure: s^{−1} = s and r ∗ s is defined iff r = s, and then s ∗ s = s.

A subgroupoid is a subset H ⊆ G that is closed under inversion and composition.

5.1 Type Groupoids and the Fundamental Theorem of Type Equality

Definition 9 (Type groupoid). A type structure is groupoidal if each T_{Ξ}^{κ} is a groupoid, constants are preserved under inversion, and inversion and composition distribute over application, i. e., C^{−1} = C, (F · G)^{−1} = F^{−1} · G^{−1}, and (F · G) ∗ (F′ · G′) = (F ∗ F′) · (G ∗ G′).

Given a type structure T we define the square type groupoid^{2}T as the product type structure T × T equipped with (F, G)^{−1} = (G, F) and (F, G) ∗ (G, H) = (F, H). If K ∈ T̂^{κ} and K′ ∈ T̂^{κ′} are groupoids, so is K →T̂ K′ ∈ T̂^{κ→κ′}

Definition 10 (Induced type groupoid). Let T be a type structure and E ⊆ ^{2}T . We say E is induced if E is an induced type structure and E_{Ξ}^{⋆} is groupoidal for all Ξ.

Since type equality refers to kinding, we will have to refer to the fundamental theorem of kinding in the proof of the fundamental theorem of type equality.

Lemma 2 (Fundamental theorem of kinding for type groupoids). Let T be a type structure and E ⊆ ^{2}T be induced. Then,

1. E is a type subgroupoid of^{2}T , and

2. if Ξ ⊢ T : κ and (ρ, ρ′) ∈ E_{Θ}^{Ξ} then (T [[T]]_{ρ}, T [[T]]_{ρ′}) ∈ E_{Θ}^{κ}.

Definition 11 (Model/respect type equality). E ⊆ ^{2}T models type equality if Ξ ⊢ T = T′ : κ and (ρ, ρ′) ∈ E_{Θ}^{Ξ} imply (T [[T]]_{ρ}, T [[T′]]_{ρ′}) ∈ E_{Θ}^{κ}. A type structure T′ respects type equality if Ξ ⊢ T = T′ : κ implies T′[[T]]_{ρ} = T′[[T′]]_{ρ} for all ρ ∈ T′_{Θ}^{Ξ}.

Theorem 5 (Fundamental theorem of type equality). Let T be a combinatory type structure and E ⊆ ^{2}T an induced type structure. Then E models type equality.

5.2 Completeness of NbE for Types

In the following we show that the relation “reify to the same η-long form” gives rise to an equivalence relation on types which models type equality. This implies that NbE is complete.

Def. and Lem. 6 (Kind candidate space for completeness) Let T be term-like.

\overline{Per}_{Ξ}^{κ} = \{(F, F′) ∈ ^{2}T_{Ξ}^{κ} | Ξ ⊢ F ↘ V ⇑ κ and Ξ ⊢ F′ ↘ V ⇑ κ for someV ∈ Ty_{Ξ}^{κ}\}
\underline{Per}_{Ξ}^{κ} = \{(F, F′) ∈ ^{2}T_{Ξ}^{κ} | Ξ ⊢ F ↘ V ⇓ κ and Ξ ⊢ F′ ↘ V ⇓ κ for someV ∈ Ty_{Ξ}^{κ}\}

\underline{Per}^{κ} and \overline{Per}^{κ} are Kripke families of subgroupoids, and form a kind candidate space.

Def. and Lem. 7 (Type groupoid for completeness) Let T be a type structure. We define P^{κ} ⊆ ^{2}T^{κ} by recursion on κ: P^{⋆} := \underline{Per}^{⋆} and P^{κ→κ′} = P^{κ} →^{ ˆ2}T P^{κ′}. P is an induced type groupoid.

Theorem 8 (Completeness of NbE for types). Let T be a term-like type structure. If Ξ ⊢ T = T′ : κ then Ξ ⊢ [[T]]_{Var} ↘ V ⇑ κ and Ξ ⊢ [[T′]]_{Var} ↘ V ⇑ κ for some V.

Proof. Since (Var, Var) ∈ P_{Ξ}^{Ξ}, by the fundamental theorem of type equality we have ([[T]]_{Var}, [[T′]]_{Var}) ∈ P_{Ξ}^{κ} ⊆ \overline{Per}_{Ξ}^{κ} which entails the goal. ⊓ ⊔

6 Object Structures

In this section, we introduce object structures which model both the syntactic object structure Obj indexed by syntactic types in Ty and structures of values D indexed by type values from a structure T . The following development, leading up the fundamental theorem of typing and the soundness of NbE for objects, parallels the preceding one on the type level. However, while we could define the glueing type structure G^{κ} by induction on kind κ, we cannot define a similar glueing objects structure gl by induction on types, due to impredicativity. Hence, we will define gl as a structure of candidates for semantic types.

Definition 12 (Typing context). Given a type structure T , a T_{Ξ}-context Δ ∈ T_{Ξ}^{cxt} is a partial map from the term variables into T_{Ξ}^{⋆}. If Γ ∈ Ty_{Ξ}^{cxt} and ρ ∈ T_{Θ}^{Ξ} then [[Γ]]_{ρ} ∈ T_{Θ}^{cxt} is defined by [[Γ]]_{ρ}(x) = [[Γ (x)]]_{ρ}.

Let Obj_{Γ}^{Ξ ⊢T} = {t | Ξ; Γ ⊢ t : T }.

Definition 13 (Object structure). Let T be a type structure. An object structure over T is a family D^{Ξ ⊢A} (A ∈ T_{Ξ}^{⋆}) of Kripke sets indexed by T_{Ξ}-contexts Δ such that Ξ′ ≤ Ξ implies D_{Δ}^{Ξ ⊢A} = D_{Δ}^{Ξ′ ⊢A}. It respects type equality, i. e., Ξ ⊢ T = T′ : ⋆ implies D^{Θ ⊢[[T]]_{ρ}} = D^{Θ ⊢[[T′]]_{ρ}} for any ρ ∈ T_{Θ}^{Ξ}, and there are operations:

app_{Δ}^{Ξ ⊢A→B} ∈ D_{Δ}^{Ξ ⊢A→B} → D_{Δ}^{Ξ ⊢A} → D_{Δ}^{Ξ ⊢B},
TyApp_{Δ}^{Ξ ⊢∀^{κ}F} ∈ D_{Δ}^{Ξ ⊢∀^{κ}F} → (G ∈ T_{Ξ}^{κ}) → D_{Δ}^{Ξ ⊢F ·G}.

We write · for both of these operations. For Δ, Ψ ∈ T_{Θ}^{cxt}, let η ∈ D_{Δ}^{Θ ⊢Ψ} iff η(x) ∈ D_{Δ}^{Θ ⊢Ψ(x)} for all x ∈ dom(Ψ). We stipulate a family of evaluation functions

⦇ ⦈^{ρ} ∈ Obj_{Γ}^{Ξ ⊢T} → D_{Δ}^{Θ ⊢[[Γ]]_{ρ}} → D_{Δ}^{Θ ⊢[[T]]_{ρ}}

indexed by ρ ∈ T_{Θ}^{Ξ} which satisfy the following equations:

\begin{aligned}⦇x⦈_{η}^{ρ} & = & η(x) \\ ⦇r s⦈_{η}^{ρ} & = & ⦇r⦈_{η}^{ρ} · ⦇s⦈_{η}^{ρ} \\ ⦇t U⦈_{η}^{ρ} & = & ⦇t⦈_{η}^{ρ} · [[U]]_{ρ} \\ ⦇t[u/x]⦈_{η}^{σ} & = & ⦇t⦈_{η[x↦⦇u⦈_{η}^{σ}]}^{σ} & (∗) \end{aligned}  \begin{aligned}⦇λx:U. t⦈_{η}^{ρ} · d & = & ⦇t⦈_{η[x↦d]}^{ρ} & ifd ∈ D_{Δ}^{Θ ⊢[[U]]_{ρ}} \\ ⦇ΛX:κ. t⦈_{η}^{ρ} · G & = & ⦇t⦈_{η}^{ρ[X↦G]} & ifG ∈ T_{Θ}^{κ} \\ ⦇t[U/X]⦈_{η}^{σ} & = & ⦇t⦈_{η}^{σ[X↦[[U]]_{σ}]} & (∗) \end{aligned}

Again, (∗) have to hold only in combinatory object structures.

With parallel substitution, Obj (modulo β, βη, or judgmental equality) forms an object structure over Ty (modulo the same equality).

Definition 14 (Object substructure). Let S, T be type structures with S ⊆ T and let D be an object structure over T . Let E^{Ξ ⊢A} ⊆ D^{Ξ ⊢A} be a Kripke family of subsets indexed by Δ ∈ S_{Ξ}^{cxt} for all A ∈ S_{Ξ}^{⋆}. Then E is an object substructure of D over S if application and evaluation are well defined on E.

Definition 15 (Reindexed object structure). Let M : S → T be a type structure morphism and D an object structure over T . The type structure E^{Ξ ⊢A} := D^{Ξ ⊢M(A)} over S with f ·_{E} d := f ·_{D} d, d ·_{E} G := d ·_{D} (M(G)), and E⦇ ⦈^{ρ} := D⦇ ⦈^{M∘ρ} is called D reindexed by M.

Given object structures D_{1} over T_{1} and D_{2} over T_{1} we define the product object structure D_{1} × D_{2} over T_{1} × T_{2} in the obvious way.

6.1 Realizability Type Structure and the Fundamental Theorem of Typing

Fix some term-like type structure T and an object structure D over T . Let A ∈ D̂_{Ξ}^{A} if A_{Δ} ⊆ D_{Δ}^{Ξ ⊢A} and A is Kripke. D̂_{Ξ}^{A} forms a complete lattice for all Ξ, A.

Definition 16 (Function space and type abstraction on D̂).

→D̂  ∈ D̂_{Ξ}^{A} → D̂_{Ξ}^{B} → D̂_{Ξ}^{A→B}
(A → B)_{Δ} := {f ∈ D_{Δ}^{Ξ ⊢A→B} | for all d, Δ′ ≤ Δ, d ∈ A_{Δ′} impliesf · d ∈ B_{Δ′}}
( . )^{∀^{κ}F} ∈ (G ∈ T_{Ξ}^{κ}) → D̂_{Ξ}^{F ·G} → D̂_{Ξ}^{∀^{κ}F}
(G.A)_{Δ}^{∀^{κ}F} := {d ∈ D_{Δ}^{Ξ ⊢∀^{κ}F} | d · G ∈ A_{Δ}}

Constructors of higher kind are interpreted as operators on Kripke sets.

Definition 17 (Kripke operators of higher kind). We define D̂_{Ξ}^{F:κ} by D̂_{Ξ}^{A:⋆} := D̂_{Ξ}^{A} and D̂_{Ξ}^{F:κ→κ′} := (G ∈ T_{Ξ}^{κ}) → D̂_{Ξ}^{G:κ} → D̂_{Ξ}^{F ·G:κ′}.

Definition 18 (Type candidate space). A type candidate space C for D over T consists of two Kripke sets \underline{C}^{Ξ ⊢A}, \overline{C}^{Ξ ⊢A} ∈ D̂_{Ξ}^{A}, (written \underline{A}, \overline{A} if no ambiguities arise) for each type A ∈ T_{Ξ}^{⋆} such that the following conditions hold.

\underline{H}  ⊆ \overline{H}  ∈ D̂_{Ξ}^{H} (H neutral )
\underline{∀^{κ}F}  ⊆ G.\underline{F · G} ∈ D̂_{Ξ}^{∀^{κ}F} (G ∈ T_{Ξ}^{κ})
X.\overline{F · X} ⊆ \overline{∀^{κ}F}  ∈ D̂_{Ξ}^{∀^{κ}F} (X ∉ dom(Ξ))

\underline{A → B} ⊆ \overline{A} →D̂ \underline{B} ∈ D̂_{Ξ}^{A→B}_{\underline{A} →D̂ \overline{B} ⊆ \overline{A → B} ∈ D̂_{Ξ}^{A→B}}

Definition 19 (Realizable semantic types). If F ∈ T_{Ξ}^{κ} and F ∈ D̂_{Ξ}^{F:κ} then F ⊩_{C}^{κ} F (pronounced F realizes F) is defined by induction on κ as follows:

\begin{aligned}A ⊩_{C}^{⋆} A & :⟺ & \underline{A} ⊆ A ⊆ \overline{A} \\ F ⊩_{C}^{κ→κ′} F & :⟺ & F · G ⊩_{C}^{κ′} F(G, G) for all G ⊩_{C}^{κ} G \end{aligned}

We define the Kripke families T D̂_{Ξ}^{κ} = {(F, F) ∈ T_{Ξ}^{κ} × D̂_{Ξ}^{F:κ}} and C_{Ξ}^{κ} = {(F, F) ∈ T_{Ξ}^{κ} × D̂_{Ξ}^{F:κ} | F ⊩_{C}^{κ} F}. For the remainder of this section, we fix a type candidate space C.

Definition 20 (Interpretation into D̂). For T ∈ Ty_{Ξ}^{κ} and (σ, ρ) ∈ T D̂_{Θ}^{Ξ} we define D̂[[T]]_{σ,ρ} ∈ D̂_{Θ}^{T [[T]]_{σ}:κ} as follows:

D̂[[X]]_{σ,ρ}  := ρ(X)
D̂[[λX:κ. T]]_{σ,ρ} := ((G, G) ∈ T D̂_{Θ}^{κ}) ↦ D̂[[T]]_{(σ,ρ)[X↦(G,G)]}
D̂[[T U]]_{σ,ρ}  := D̂[[T]]_{σ,ρ}(T [[U]]_{σ}, D̂[[U]]_{σ,ρ})
D̂[[C]]_{σ,ρ}  := CD̂
where ∀κ ; D̂  ∈ D̂_{Ξ}^{∀^{κ}:(κ→⋆)→⋆}
∀κ ; D̂(F, F)  := ⋂_{G⊩^{κ}G} G.F(G, G)

Since the kind function space is the full set-theoretic one, D̂ is combinatory and respects type equality.

Theorem 9 (Realizability). T D̂ is a type structure with application (F, F) · (G, G) = (F · G, F(G, G)) and evaluation T D̂[[T]]_{σ,ρ} = (T [[T]]_{σ}, D̂[[T]]_{σ,ρ}). C is a type substructure of T D̂.

Theorem 10 (Fundamental theorem of typing). Let D be an object structure over T and \underline{C}, \overline{C} ∈ D̂ a type candidate space. Let S ⊆ C be a type substructure of the associated realizability type structure C. Then the family E_{(Δ,Φ)}^{Ξ ⊢(A,A)} := A_{Δ} is an object substructure of D reindexed by π_{1} : S → T .

6.2 Soundness of NbE for Objects

Term-like object structures and neutral objects are now defined analogously to term-like type structures.

Definition 21 (Object reification). Given a term-like type structure T and a term-like object structure D over T , we define the relations

Ξ; Δ ⊢ d ↘ v ⇑ A  d reifies to v at type A,
Ξ; Δ ⊢ e ↘ u ⇓ A  e reifies to u, inferring type A,

(where d, e ∈ D_{Δ}^{Ξ ⊢A} and v, u are syntactical objects) inductively by the following rules:

\overline{Ξ; Δ ⊢ x ↘ x ⇓ Δ(x)}  \frac{Ξ; Δ ⊢ e ↘ u ⇓ A → B  Ξ; Δ ⊢ d ↘ v ⇑ A}{Ξ; Δ ⊢ e d ↘ u v ⇓ B}

\frac{Ξ; Δ ⊢ e ↘ u ⇓ ∀^{κ}F  Ξ ⊢ G ↘ V ⇑ κ}{Ξ; Δ ⊢ e G ↘ u V ⇓ F · G}  \frac{Ξ, X:κ; Δ ⊢ f · X ↘ v ⇑ F · X}{Ξ; Δ ⊢ f ↘ ΛX:κ. v ⇑ ∀^{κ}F}

\frac{Ξ; Δ, x:A ⊢ f · x ↘ v ⇑ B Ξ ⊢ A ↘ U ⇑ ⋆}{Ξ; Δ ⊢ f ↘ λx:U. v ⇑ A → B} \frac{Ξ; Δ ⊢ e ↘ u ⇓ H}{Ξ; Δ ⊢ e ↘ u ⇑ H} H neutral

As for types, object reification is deterministic.

Note that we cannot say now in which Obj_{Γ}^{Ξ ⊢T} the objects u and v live. The conjecture is those Γ, T with Ξ ⊢ Δ ↘ Γ and Ξ ⊢ A ↘ T ⇑ ⋆. However, this does not follow directly from the definition, it is a consequence of Thm. 12.

Def. and Lem. 11 (Glueing type candidate space) Let S ⊆ T × Ty a glueing candidate, ⊩_{Gl} S. For (A, T) ∈ S_{Ξ}^{⋆} we define the Kripke families \underline{gl}^{Ξ ⊢(A,T)}, \overline{gl}^{Ξ ⊢(A,T)} ∈

{ \atop D × Obj}_{Ξ}^{(A,T)} by

\overline{gl}_{(Δ,Γ)}^{Ξ ⊢(A,T)} := \{(d, t) | Ξ; Δ ⊢ d ↘ v ⇑ A and Ξ; Γ ⊢ t = v : T for somev\},
\underline{gl}_{(Δ,Γ)}^{Ξ ⊢(A,T)} := \{(e, t) | Ξ; Δ ⊢ e ↘ u ⇓ A and Ξ; Γ ⊢ t = u : T for someu\}.

gl is a type candidate space.

Theorem 12 (Soundness of NbE for objects). Let D be a term-like object structure over a term-like type structure T . If Ξ; Γ ⊢ t : T then there is a long normal form v such that Ξ; T [[Γ]]_{Var} ⊢ D⦇t⦈_{var}^{Var} ↘ v ⇑ T [[T]]_{Var} and Ξ; Γ ⊢ t = v : T.

6.3 Completeness of NbE for objects

Completeness on the object level is shown analogously to completeness on the type level. Define object groupoids as groupoidal object structures and show that Kripke function space and impredicative quantification on D̂ preserve the groupoid structure. Then prove a fundamental theorem of object equality and instantiate it to the type candidate space defined analogously to Per. Due to lack of space, we cannot spell out the details and refer to the full version of this article instead [Abe09].

7 Conclusion

We have developed type and object structures, which are sorted applicative structures on type and object level, in order to facilitate generic model constructions for System F^{ω}—which are an alternative to categorical semantics [See87] and Bruce-Meyer-Mitchell models [BM84]. Using special instances of kind candidate spaces we have shown soundness and completeness of an abstract normalization by evaluation algorithm for types. We have gone on to show soundness and completeness of NbE for objects.

We seek to extend NbE to the Calculus of Constructions, using ideas from this work. Due to dependency, type and object levels cannot be defined in sequence, but must be defined simultaneously; this seems to be the main remaining technical difficulty.

References

[Abe08] Andreas Abel. Weak βη-normalization and normalization by evaluation for System F. In LPAR’08, volume 5330 of LNAI, pages 497–511. Springer, 2008.

[Abe09] Andreas Abel. Typed applicative structures and nor-

malization  by  evaluation  for  System  F^{ω}  (full  version).

http://www.tcs.ifi.lmu.de/~abel/fomegaNbe.pdf, 2009.

[ACD07] Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In LICS’07, pages 3–12. IEEE CS Press, 2007.

[ACD08] Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semantic βηconversion test for Martin-Löf type theory. In MPC’08, volume 5133 of LNCS, pages 29–56. Springer, 2008.

[ADHS01] Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In LICS’01, pages 303–310. IEEE CS Press, 2001.

[AHS96] Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for a polymorphic system. In LICS’96, pages 98–106. IEEE CS Press, 1996.

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

[Bar08] Freiric Barral. Decidability for non-standard conversions in lambda-calculus. PhD thesis, Ludwig-Maximilians-University Munich, 2008.

[BCF04] Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL’04, pages 64–76. ACM, 2004.

[BM84] Kim B. Bruce and Albert R. Meyer. The semantics of second order polymorphic lambda calculus. In Semantics of Data Types, volume 173 of LNCS, pages 131–144. Springer, 1984.

[BS91] Ulrich Berger and Helmut Schwichtenberg. An inverse to the evaluation functional for typed λ-calculus. In LICS’91, pages 203–211. IEEE CS Press, 1991.

[CAM07] James Chapman, Thorsten Altenkirch, and Conor McBride. Epigram reloaded: a standalone typechecker for ETT. In TFP’05, volume 6 of Trends in Functional Programming, pages 79–94. Intellect, 2007.

[CD97] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. MSCS, 7(1):75–94, 1997.

[Coq96] Thierry Coquand. An algorithm for type-checking dependent types. In MPC’95, volume 26 of SCP, pages 167–177. Elsevier, 1996.

[Dan99] Olivier Danvy. Type-directed partial evaluation. In Partial Evaluation Summer School ’98, volume 1706 of LNCS, pages 367–411. Springer, 1999.

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

[GL02] Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In ICFP’02, volume 37 of SIGPLAN Notices, pages 235–246. ACM, 2002.

[GLT89] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in TCS. CUP, 1989.

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

[Nor07] Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers, Göteborg, Sweden, 2007.

[Pol94] Robert Pollack. Closure under alpha-conversion. In TYPES’93, volume 806 of LNCS, pages 313–332. Springer, 1994.

[See87] R. A. G. Seely. Categorical semantics for higher order polymorphic lambda calculus. JSL, 52(4):969–989, 1987.