Towards Normalization by Evaluation for the βη-Calculus of Constructions

Andreas Abel

Project PI.R2, INRIA Rocquencourt and PPS, Paris

                        andreas.abel@ifi.lmu.de

Abstract. We consider the Calculus of Constructions with typed beta-eta equality and an algorithm which computes long normal forms. The normalization algorithm evaluates terms into a semantic domain, and reifies the values back to terms in normal form. To show termination, we interpret types as partial equivalence relations between values and type constructors as operators on PERs. This models also yields consistency of the beta-eta-Calculus of Constructions. The model construction can be carried out directly in impredicative type theory, enabling a formalization in Coq.

1 Introduction

The proof assistant Coq [INR08] based on intensional type theory is used for large verification projects in mathematics [Gon04] and computer science [Ler06]. However, to this day no complete meta theory of its logical core, the Calculus of Inductive Constructions (CIC) exists. The CIC is a dependent type theory with at least one impredicative base universe (Set or Prop or both) and an infinite cumulative hierarchy of predicative universes (Type_{i}) above this base. Inductive types with large (aka strong) eliminations exist at every level. The CIC is formulated with untyped equality, leading to complications in model constructions [MW03] and in the treatment of η-equality. As η-reduction, the subject reduction property requires contravariant subtyping, which is especially hard to model (I am only aware of Miquel’s coherence space model [Miq00]). And it cannot be formulated as η-expansion in an untyped setting. The lack of η-equality in Coq is an annoyance both for its implementers and its users.

Recently, formulations of CIC with typed equality, aka judgemental equality, have been considered since they admit simple set-theoretical models [Bar09]. Judgemental equality also integrates η-equality nicely. On the downside, injectivity of the function space constructor Π, crucial for the implementation of type checking, is notoriously difficult to establish. Goguen [Gog94] has obtained injectivity of Π in the Extended Calculus of Constructions via his Typed Operational Semantics, a typed Kripke term model with standardizing reduction. In predicative Martin-Löf Type Theory, it is the byproduct of a PER model construction which also yields Normalization by Evaluation (NbE) [ACD07].

In this article, we investigate NbE for the Calculus of Constructions (CoC), a fragment of the CIC with just one impredicative and one predicative universe, with typed βη-equality. By constructing a PER model, we obtain termination and completeness for NbE, the latter meaning that all judgmentally equal terms normalize to the same expression. As a consequence of the model, we obtain logical consistency of the βη-CoC.

The missing property of soundness of NbE, meaning that each term is judgmentally equal to its computed normal form, is implied by injectivity of Π and vice versa. Decidability of typing also hinges on injectivity. This leaves two options to complete this work and obtain a sound and complete type checker for the CoC with η: Prove soundness of NbE by Kripke logical relations between syntax and semantics as in [ACP09], or obtain injectivity by syntactical means. Adams [Ada06] obtained injectivity for functional pure type systems with judgemental β-equality; his proof might extend to βη.

Overview. This article is organized as follows: In Section 2 we introduce CoC with typed equality and explicit substitutions. In Section 3 we define normalization by evaluation for CoC using partial applicative structures, and we specify a type inference algorithm. In Section 4 we recapitulate a simple method how to classify CoC expressions into terms, types, and kinds, a device which helps us to bootstrap the PER model construction in Section 5. Section 6 proves the rules of CoC sound wrt. our model, and as a corollary we obtain termination and completeness of NbE and consistency of CoC. Loose ends are listed in the conclusions (Section 7).

2 Syntax

We present the Calculus of Constructions (CoC) as a pure type system (PTS) with annotated λ-abstraction, typed equality and explicit substitutions.

1. Annotated λ-abstraction (as in λ M N) enables us to compute the type of a term from the type of its free variables and its semantics from the semantics of its free variables (see Section 6). Thus, a term makes already sense in a context alone, it does not need an ascribed type.

2. Typed equality is the natural choice in the presence of η since untyped η-reduction is badly behaved in set-theoretical models and type-theoretical models without subtyping —this includes the semantics we are constructing. (Untyped η-expansion cannot be defined.)

3. Lambda calculi with explicit substitutions have more models than lambda calculi with substitution implemented as an operation. In particular, the model of closures in weak head normal form we will use in Section 3. Recent meta theoretic studies involving explicit substitutions include [Dan07,Cha09,Gra09,ACP09]. In the presence of explicit substitutions, variables are most naturally represented as de Bruijn indices [ACCL91].

2.1 Expressions and Typing

The CoC is a dependently typed lambda calculus with expressions on three levels: terms t, u, the data structures and programs of the language; the types T, U of terms, generalized to a lambda-calculus of type constructors^{1}; and the kinds κ, ι, the types of types.

1 E.g., List is a type constructor which produces a type of homogeneous lists List T for each element type T.

In the PTS-style presentation, there is just one language of expressions M, N for all three levels, and the classification of expressions into terms, type constructors, and kinds is a byproduct of typing, using the two sorts s ::= ∗, □. The inhabitants of sort □ are kinds, one of which is ∗, and the inhabitants of sort ∗ are types, whose inhabitants in turn are terms.

From our perspective, the CoC is a dependent version of System F^{ω}. In terms of the Calculus of Inductive Constructions, the core language of Coq [INR08], the sort ∗ is the impredicative Set, and the sort □ the predicative Type_{0}. Alternatively [Wer92], one could identify ∗ with the impredicative Prop and refer to the levels as proof terms, predicates, and kinds instead.

Syntax of expressions, substitutions, and contexts. We represent bound variables by de Bruijn indices; the 0th variable is represented by the expression v_{0}, the ith variable by the i-fold application of the lifting substitution ↑ to the expression v_{0}. Consequently, we use the expression v_{i} as a shorthand for the expression v_{0} ↑^{i}. Also, we abbreviate (id, N) by [N].

Sort ∋ s  ::= ∗ | □
Exp ∋ M, N, t, u, T, U, κ, ι ::= s | v_{0} | λ M N | M N | Π M N | M σ
Subst ∋ σ, τ  ::= ↑ | id | σ τ | (σ, M)
Cxt ∋ Γ, Δ  ::= () | Γ, M

We denote the length of context Γ by ∥Γ ∥. We use ≡ for literal identity of expressions, and the dot notations Π U. T and λ U. M to save parentheses.

Normal forms are those expressions that do not contain substitutions (except lifting of an index) or β-redexes. Normal forms starting with a variable are called neutral.

Norm ∋ v, w, V, W ::= s | λV w | Π V W | n  β-normal form
Neut ∋ n, N  ::= v_{i} | n v  neutral normal form

Typing. The judgements Γ ⊢ “Γ is a well-formed context” and Γ ⊢ M : N “M has type N in context Γ ” are given inductively by the following rules.

\overline{() ⊢}  \frac{Γ ⊢  Γ ⊢ T : s}{Γ, T ⊢}

\frac{Γ ⊢}{Γ ⊢ ∗ : □}  \frac{Γ ⊢ U : s  Γ, U ⊢ T : s′}{Γ ⊢ Π U T : s′}

\frac{Γ ⊢ T : s}{Γ, T ⊢ v_{0} : T ↑}  \frac{Γ ⊢ U : s  Γ, U ⊢ T : s′  Γ, U ⊢ M : T}{Γ ⊢ λ U M : Π U T}

\frac{Γ ⊢ M : Π U T  Γ ⊢ N : U}{Γ ⊢ M N : T [N]}  \frac{Γ ⊢ M : T  Γ ⊢ T = T′ : s}{Γ ⊢ M : T′}

We come to the judgement for type equality, Γ ⊢ T = T′ : s, later. The typing rules for substitutions are:

\frac{Γ ⊢ σ : Δ  Δ ⊢ M : T}{Γ ⊢ M σ : T σ}  \frac{Γ ⊢ σ : Δ  Δ ⊢ T : s  Γ ⊢ M : T σ}{Γ ⊢ (σ, M) : Δ, T}

\frac{Γ ⊢}{Γ ⊢ id : Γ}  \frac{Γ_{1} ⊢ τ : Γ_{2}  Γ_{2} ⊢ σ : Γ_{3}}{Γ_{1} ⊢ σ τ : Γ_{3}}  \frac{Γ ⊢ T : s}{Γ, T ⊢ ↑ : Γ}

For i < ∥Γ ∥, we define context look-up Γ (i) by (Γ, T)(0) = T ↑ and (Γ, T)(i + 1) = Γ (i) ↑. It is easy to see that the general variable rule is derivable by induction on i:

\frac{Γ ⊢}{Γ ⊢ v_{i} : Γ (i)}

Using this rule, we can understand typing of expressions from the first set of rules alone, under an abstract view on substitution and equality.

2.2 Typed Equality

We formalize βησ-equality by the judgements Γ ⊢ M = M′ : T and Γ ⊢ σ = σ′ : Δ. Equality holds only between well-formed objects of syntax, thus the rules have to be formulated such that they entail Γ ⊢ M : T (and likewise for M′, σ, and σ′). For instance, the η-rule reads:

\frac{Γ ⊢ M : Π U T}{Γ ⊢ M = λ U. (M ↑) v_{0} : Π U T}

We will not spell out the rules will types and typing assumptions. Instead, we will just write down axioms in the form M = M′ and σ = σ′, the typing can be reconstructed. Also we will skip all congruence rules expressing that equality is an equivalence relation and that it is closed under all syntactic constructions. We have taken a similar approach before [ACP09] which is justified by Cartmell’s work on generalized algebraic theories [Car86].

Computation: β, resolution of substitutions, pushing substitution under constructions.

\begin{aligned}(λUM) N & = & M[N] \\ v_{0} (σ, M) & = & M \\ ↑ (σ, M) & = & σ \\ M id & = & M \\ s σ & = & s \end{aligned}  \begin{aligned}(M N) σ & = & (M σ) (N σ) \\ (λ U M) σ & = & λ U σ. M (σ ↑, v_{0}) \\ (Π U T) σ & = & Π U σ. T (σ ↑, v_{0}) \\ (M σ) τ & = & M (σ τ) \\ (σ, M) τ & = & (σ τ, M τ) \end{aligned}

Non-computational rules: Extensionality and rules of the category of substitutions.

\begin{aligned}M & = & λ U. (M ↑) v_{0} \\ id & = & (↑, v_{0}) \end{aligned}  \begin{aligned}id σ & = & σ \\ σ id & = & σ \\ (σ_{1} σ_{2}) σ_{3} & = & σ_{1} (σ_{2} σ_{3}) \end{aligned}

3 Normalization by Evaluation

We conceive normalization by evaluation as the composition of a standard interpreter ⦇ ⦈ : Exp → D mapping expressions into a semantics D and a reifier which computes a long normal form from a value in D. Coquand [ACP09] observed that the η-expansion part of reification can be carried out entirely within the semantics which splits reification into an η-expansion phase ↓ : D → D_{nf} and a read-back phase R^{nf} : D_{nf} → Norm ⊆ Exp.

\xymatrix{ &  & D \ar[d]_{↓} \\ Exp \ar[urr]^{⦇ ⦈} & Norm \ar[l]_{⊇} & D_{nf} \ar[l]_{R^{nf}} & D_{ne} \ar[ul]_{↑}}

η-expansion ↓ is mutually defined with reflection ↑ : D_{ne} → D which injects variables (de Bruijn levels), and more generally neutral values e ∈ D_{ne}, into the semantics in η-expanded form.

3.1 Weak head evaluation

While having used a Scott domain to represent values in previous work [ACP09], we now change to partial applicative structures which subsume Scott domains (and, indeed, all λ-models and -algebras). The following representation of values by closures is such a structure and it can be directly formalized in type theory which is not the case for any effective total applicative structure.

Values are defined in terms of closures (\underline{λ}t)η and de Bruijn levels. Level x_{j} represents the jth free variable. In effect, we are using a locally nameless presentation of values [Pol94] where bound variables are represented as relative references (de Bruijn indices v_{i}) and free variables as absolute references, i. e., names (de Bruijn levels x_{j}). The delayed η-expansions ↑^{\underline{Π} A F} e and ↓^{\underline{Π} A F} f are the defunctionalization of reflection and reification in the Scott domain (as closures are the defunctionalization of evaluation).

D ∋ a, b, f, A, B, F, G, K, L ::= s | \underline{Π} A F | (\underline{λ}t)η | ↑^{\underline{Π} A F} e | e  value
DNe ∋ e, E  ::= x_{j} (j ∈ ℕ) | e d  neutral value
DNf ∋ d, D  ::= ↓^{\underline{Π} A F} f | a  normal value
Env ∋ η  ::= id | (η, a)  environment

We let ↑^{B} e = e and ↓^{B} a = a if B is not a Π-type.

Evaluation and application. We introduce the judgements ⦇M⦈_{η} ↘ a “in environment η, expression M evaluates to a”, ⦇σ⦈_{η} ↘ η′ “in environment η, substitution σ evaluates to environment η′”, and f ·a ↘ b “value f applied to value a evaluates to b” inductively by the following rules.

\overline{⦇s⦈_{η} ↘ s}  \overline{⦇v_{0}⦈_{(η,a)} ↘ a}  \overline{⦇λ U t⦈_{η} ↘ (\underline{λ}t)η}  \frac{⦇U⦈_{η} ↘ A}{⦇Π U T ⦈_{η} ↘ \underline{Π} A (\underline{λ}T)η}

\frac{⦇t⦈_{η} ↘ f  ⦇u⦈_{η} ↘ a  f · a ↘ b}{⦇t u⦈_{η} ↘ b}  \frac{⦇σ⦈_{η} ↘ η′  ⦇t⦈_{η′} ↘ a}{⦇t σ⦈_{η} ↘ a}

\overline{⦇↑⦈_{(η,a)} ↘ η} \overline{⦇id⦈_{η} ↘ η} \frac{⦇σ⦈_{η} ↘ η′  ⦇t⦈_{η} ↘ a}{⦇(σ, t)⦈_{η} ↘ (η′, a)} \frac{⦇τ⦈_{η} ↘ η′  ⦇σ⦈_{η′} ↘ η′′}{⦇σ τ⦈_{η} ↘ η′′}

\frac{⦇t⦈_{(η,a)} ↘ b}{(\underline{λ}t)η · a ↘ b}  \frac{F · a ↘ B}{(↑^{\underline{Π} A F} e) · a ↘ ↑^{B}(e ↓^{A} a)}

These three relations are deterministic, thus, they can be turned into partial functions ⦇ ⦈ : Exp × Env ⇀ D, ⦇ ⦈ : Subst × Env ⇀ Env, and · : D × D ⇀ D.

3.2 Read-back (aka Reification)

We introduce two judgements m ⊢ d ↘ v “at level m, normal value d reifies to normal form v”, and m ⊢^{ne} e ↘ n “at level m, neutral value reifies to neutral normal form n” inductively by the following rules. The natural number m corresponds to the de Bruijn level of the next fresh variable.

\overline{m ⊢ ∗ ↘ ∗}  \frac{m ⊢ A ↘ V  F · ↑^{A} x_{m} ↘ B  m + 1 ⊢ B ↘ W}{m ⊢ \underline{Π} A F ↘ Π V W}

\frac{m ⊢ A ↘ V  F · ↑^{A} x_{m} ↘ B  f · ↑^{A} x_{m} ↘ b  m + 1 ⊢ ↓^{B} b ↘ w}{m ⊢ ↓^{\underline{Π} A F} f ↘ λ V w}

\frac{m ⊢^{ne} e ↘ n}{m ⊢ e ↘ n} \overline{m ⊢^{ne} x_{j} ↘ v_{m−(j+1)}} \frac{m ⊢^{ne} e ↘ n  m ⊢ d ↘ v}{m ⊢^{ne} e d ↘ n v}

In the but last rule, we use the “monus” function on ℕ where m − m′ = 0 if m′ ≥ m.

Read-back is deterministic, so we introduce two partial functions by R_{m}^{nf} d = v iff m ⊢ d ↘ v and R_{m}^{ne} e = n iff m ⊢^{ne} e ↘ n. These correspond to the read-back function by Gregoire and Leroy [GL02] and own previous work [ACP09].

3.3 Type Inference

In the following we adopt bidirectional value-based type checking [Coq96,ACD08] to de Bruijn style. Since we have typed abstraction, the type of every well-typed term is inferable. We specify the type inference algorithm by a deterministic inductive judgement

Δ ⊢ t ⇉ A

meaning that in context Δ, the principal type of t is A. We keep context Δ and type A in evaluated form. The algorithm is very similar to Huet’s constructive engine [Hue89] as refined by Pollack [Pol06].

By induction on a context of values Δ, we define the η-expanded environment id_{Δ} which maps de Bruijn indices to their corresponding de Bruijn levels. We write x_{Δ} for x_{∥Δ∥}.

id_{()} = id id_{Δ,A} = (id_{Δ}, ↑^{A} x_{Δ})

Type inference is given inductively by the following rules. Note that only type checked terms are evaluated, and only values enter the contexts or are returned.

\overline{Δ ⊢ ∗ ⇉ □}  \frac{Δ ⊢ U ⇉ s  Δ, ⦇U⦈_{id_{Δ}} ⊢ T ⇉ s′}{Δ ⊢ Π U T ⇉ s′}  \overline{Δ ⊢ v_{i} ⇉ Δ(i)}

\frac{Δ ⊢ U ⇉ s  ⦇U⦈_{id_{Δ}} ↘ A  Δ, A ⊢ t ⇉ B  Δ, A ⊢ B ⟶^{λ} F}{Δ ⊢ λ U t ⇉ \underline{Π} A F}

\frac{Δ ⊢ t ⇉ \underline{Π} A F  Δ ⊢ u ⇉ B  Δ ⊢ A ≅ B}{Δ ⊢ t u ⇉ F · ⦇u⦈_{id_{Δ}}}

In the last two rules we have used two auxiliary judgements. In the application rule, we check the ascribed type A and the inferred type B for βη-equality using Δ ⊢ A ≅ B. In the application rule, we need to turn the type value B of the function body t into a

function over the last variable x_{Δ}, which is of type A. We write Δ, A ⊢ B ⟶^{λ} F for this abstraction operation.

Δ ⊢ A ≅ B  ⟺ ∥Δ∥ ⊢ A ↘ V and ∥Δ∥ ⊢ B ↘ V
Δ, A ⊢ B ⟶^{λ} F ⟺ ∥Δ, A∥ ⊢ B ↘ V and F ≡ (\underline{λ}V)id

Type values A and B are equal if they reify to the same normal form V. Due to our

locally nameless style values, abstraction Δ, A ⊢ B ⟶^{λ} F is a bit cumbersome. We implement it by first reifying value B in context Δ, A to term V and then building the closure F ≡ (\underline{λ}V)id.

3.4 Normalization

During type inference, values are reified to normal forms to test equality. We can also compose evaluation and read-back to obtain a normalization function for terms. Let ⦇Γ ⦈ be evaluation of contexts partially defined by

⦇()⦈ = () ⦇Γ, U⦈ = ⦇Γ ⦈, ⦇U⦈_{id_{⦇Γ ⦈}}

Using the partially defined identity environment η_{Γ} := id_{⦇Γ ⦈}, the partial normalization function is now obtained as

nbe_{Γ}^{T} (t) = R_{∥Γ ∥}^{nf} (↓^{⦇T ⦈_{η_{Γ}}} ⦇t⦈_{η_{Γ}})
Nbe_{Γ} (T) = nbe_{Γ}^{□}(T).

The goal of this work is to show its correctness on well-formed expressions, i. e.:

1. Soundness: if Γ ⊢ t : T then Γ ⊢ t = nbe_{Γ}^{T} (t) : T.

2. Completeness: if Γ ⊢ t = t′ : T then nbe_{Γ}^{T} (t) ≡ nbe_{Γ}^{T} (t′).

3. Termination: if Γ ⊢ t : T then nbe_{Γ}^{T} (t) is defined.

The termination property is a consequence of soundness and also of completeness, since judgemental equality and expression equality presuppose definedness. Remarks on soundness can be found in the long version of this paper [Abe10]. In the remainder of the paper, we will focus on completeness, which will be established by a PER model construction.

4 Classification of Expressions

If Γ ⊢ κ : □, then κ is a called a kind. If Γ ⊢ T : κ for a kind κ, then T is called a type constructor. In particular, if Γ ⊢ T : ∗, then T is called a type. If Γ ⊢ t : T for a type T, then t is called a term. We obtain three syntactic subclasses Kind, Ty, Tm of Exp. There are no kind variables, only term variables and type (constructor) variables.

Kind ∋ κ, ι ::= ∗ | Π κ κ′ | Π U κ
Ty ∋ T, U ::= Π U T | Π κ T
| X | λ κ T | T U | λ U T | T u
Tm ∋ t, u ::= x | λ U t | t u | λ κ t | t U

It is well-known that all dependencies in pure CoC can be erased such that one ends up with the terms, type constructors, and kinds of System F^{ω}. This way, one can inherit normalization of CoC from F^{ω} [GN91]. However, since we want to add inductive types in ∗ with large eliminations into ∗ (just as Werner [Wer92]), we cannot pursue this path; CoC with natural numbers has types defined by recursion on a number, so it can express types of functions with varying arity, like

(X:∗) → (n:Nat) → \underbrace{X → ⋯ → X}_{n times} → X

which have no counterpart in F^{ω}. However, without large eliminations into □, so no kinds defined by recursion, the structure of kinds is still simple and dependencies can be erased on the kind level. This observation by Coquand and Gallier [CG90] and Werner [Wer92] has been exploited by Barras and Werner [BW97] to completely formalize strong normalization of pure CoC in Coq. Following their lead, we will use erased kinds to bootstrap our model construction in Section 5.

Simple kinds. We enrich the kinds of F^{ω} by a base kind ⋄ of terms.

SKi ∋ k ::= ⋄ | l  simple kind
SKiP ∋ l ::= ∗ | k → l  proper simple kind
SCxt ∋ γ, δ ::= () | γ, k  simple kinding context

The simple kind ⋄ → k is the erasure of the indexed kind Π T κ. The grammar forbids k → ⋄, the kind of functions from constructors of simple kind k to terms, which is a subset of the terms, so we set k → ⋄ := ⋄.

We define the judgements γ ⊢ M ÷ k “in context γ, expression M has simple kind k”, γ ⊢ σ ÷ δ “in context γ, substitution σ has simple kinding δ, and γ ⊢ M ≐ k “in context γ, expression M has skeleton k” inductively by the rules to follow. These rules are basically an erasure of the typing rules. Kinds κ are related to their skeleton k by γ ⊢ κ ≐ k, where Types T : ∗ are assigned skeleton ⋄. Type constructors T : κ are be related to the skeleton k of κ by judgement γ ⊢ T ÷ k, and terms to skeleton ⋄.

\overline{γ ⊢ ∗ ≐ ∗}  \frac{γ ⊢ U ≐ k  γ, k ⊢ T ≐ k′}{γ ⊢ Π U T ≐ k → k′}  \frac{γ ⊢ T ÷ ∗}{γ ⊢ T ≐ ⋄}

\overline{γ, k ⊢ v_{0} ÷ k}  \frac{γ ⊢ U ≐ k  γ, k ⊢ M ÷ k′}{γ ⊢ λ U M ÷ k → k′}

\frac{γ ⊢ M ÷ k → k′  γ ⊢ N ÷ k}{γ ⊢ M N ÷ k′}  \frac{γ ⊢ σ ÷ δ  δ ⊢ M ⋆ k}{γ ⊢ M σ ⋆ k} ⋆ ∈ \{÷, ≐\}

\overline{γ, k ⊢ ↑ ÷ γ}  \overline{γ ⊢ id ÷ γ}  \frac{γ ⊢ σ ÷ δ  γ ⊢ M ÷ k}{γ ⊢ (σ, M) ÷ δ, k}

\frac{γ_{1} ⊢ τ ÷ γ_{2} γ_{2} ⊢ σ ÷ γ_{3}}{γ_{1} ⊢ σ τ ÷ γ_{3}}

Shape computation. We now define two (total) functions, |M|_{γ}^{÷} “the kind of M in simple context γ”, and |M| ._{=}_{γ} “the skeleton of M in simple context γ”, by means of a general shape function |M|_{γ} which returns a pair (⋆, k) with ⋆ ∈ {≐, ÷}:

|M| ._{=}_{γ} = \{ \begin{matrix}k & if |M|_{γ} = (≐, k) \\ ⋄ & otherwise \end{matrix} |M|_{γ}^{÷} = \{ \begin{matrix}k & if |M|_{γ} = (÷, k) \\ ∗ & otherwise \end{matrix}

The shape function is defined mutually with the function |σ|_{γ}^{÷}, written |σ|_{γ}, which computes the kinds of the expressions in σ. We also define the skeleton |Γ | of a context.

|∗|_{γ} = (≐, ∗)
|Π U T |_{γ} = (≐, |U| ._{=}_{γ} → |T | ._{=}_{γ,|U|._{=}_{γ}})
|v_{0}|_{γ,k} = (÷, k)
|v_{0}|_{()} = (÷, ⋄)
|λ U M|_{γ} = (÷, |U| ._{=}_{γ} → |M|_{γ,|U|._{=}_{γ}}^{÷})
|M N|_{γ} = \{ \begin{matrix}(÷, k′) & if |M|_{γ}^{÷} = k → k′ \\ (÷, ⋄) & otherwise \end{matrix}
|M σ|_{γ} = |M|_{|σ|_{γ}}

|↑|_{γ,k}  = γ_{|↑|_{()}  = ()}_{|id|_{γ}  = γ}_{|(σ, M)|_{γ} = |σ|_{γ}, |M|_{γ}^{÷}}_{|σ τ|_{γ} = |σ|_{|τ|_{γ}}}_{|()|  = ()}_{|Γ, T | = |Γ |, |T | ._{=}_{|Γ |}}

Lemma 1 (Soundness of shape computation). For L ::= M | σ and R ::= k | γ and γ ⊢ L ⋆ R we have R = |L|_{γ}^{⋆}.

Lemma 2 (Kind skeleton independence). |M| ._{=}_{γ} = |M| ._{=}_{γ′} for all γ, γ′.

Therefore, we may suppress γ and just write |M| ._{=}.

Theorem 1 (Shapes of wellformed expressions). Let γ = |Γ |.

1. If Γ ⊢ κ : □ then γ ⊢ κ ≐ |κ| ._{=}_{γ}.

2. If Γ ⊢ κ = κ′ : □ then |κ| ._{=}_{γ} = |κ′| ._{=}_{γ}.

3. If Γ ⊢ T : ∗ then γ ⊢ T ≐ |T | ._{=}_{γ} = ⋄.

4. If Γ ⊢ M : T ≢ □ then γ ⊢ M ÷ |M|_{γ}^{÷} = |T | ._{=}_{γ}.

5. If Γ ⊢ σ : Δ then γ ⊢ σ ÷ |σ|_{γ} = |Δ|.

Proof. Simultaneously by induction on the typing/equality derivation. Note that Γ ⊢ M = M′ : T ≢ □ implies |M|_{γ}^{÷} = |M′|_{γ}^{÷} since the kinds of M and M′ equal the skeleton of T.

5 A Model for the βη-CoC with Large Eliminations

In this section, we present a PER model of CoC. Each expression M is modeled by a pair (F, F) where F : D is simply the value of M and F is the semantic role of M. Terms t ÷ ⋄ have no semantic role, they are modeled by a pair (a, ()). Types T ÷ ∗ are modeled by a pair (A, A) where A is a partial equivalence relation (PER) between semantic terms. The objects (a, ()) and (a′, ()) are related by A iff, intuitively, a and a′ are βη-equal values of type A. Formally that means that ↓^{A} a and ↓^{A} a′ must read back as the same expression; this connection between A and A is written A ⊩ A and pronounced “A realizes A”. Type constructors T ÷ k → k′ are modeled as (F, F) where F is a higher-order operator on PERs, it maps constructors (G, G) of kind k to constructors F(G, G) of kind k′. Note that unlike in System F^{ω} or erased versions of the CoC [BW97,Geu94], F also depends on a value G (see [Wer92,SG96]). Finally kinds κ ≐ k are modeled as (K, K) where the PER K relates constructors (F, F) and (F′, F′) of kind k if F and F′ are extensionally equal operators and ↓^{K} F and ↓^{K} F′ have the same normal form (thus, K realizes K). To avoid duplication we have modeled types and kinds uniformly in the formal presentation of the semantics, probably at the cost of readability; may this informal exposition serve as an Ariadne thread in the maze to follow.

Meta language. We use an impredicative type-theoretic meta language, i. e., we will not speak in terms of sets, but in terms of types and predicates. However, we will use some set-theoretic notation with care. For a type α, the type P(α) contains the predicates over α, and for P : P(α) and a : α we write a ∈ P if P (a) holds. The subset type {a : α | P (a)} is the type of pairs (a, p) such that p is a proof of P (a). Usually, we suppress the proof and write just a ∈ {a : α | P (a)}. The value f(a, p) of a function f : {a : α | P (a)} → β may not depend on the form of the proof p.

A setoid is a pair of a type α and an equivalence relation =_{α} : P(α × α). We write α for the setoid. A function f : α → β is a (setoid) morphism, f ∈ α → β, if it respects setoid equality, i. e., a =_{α} a′ implies f(a) =_{β} f(a′). Two morphisms f, f′ are equal, f =_{α→β} f′ iff a =_{α} a′ implies f(a) =_{β} f′(a). This makes (α → β, =_{α→β}) a setoid in turn.

A partial equivalence relation A : Per(α) is a binary relation over type α which is symmetric and transitive. We write a = a′ ∈ A for a, a′ : α with (a, a′) ∈ A, and a ∈ A for a = a ∈ A. Equality A = A′ of PERs holds extensionally if for all a, a′ : α, a = a′ ∈ A iff a = a′ ∈ A′. Each PER A can be coerced into an associated setoid {a : α | a ∈ A} with setoid equality A. This defines the notion of morphism F ∈ A → β from PER A to setoid β. We define Ne : Per(DNe) and Nf : Per(DNf) by

e = e′ ∈ Ne ⟺ ∀m : ℕ. ∃n : Neut. m ⊢^{ne} e ↘ n and m ⊢^{ne} e′ ↘ n
d = d′ ∈ Nf ⟺ ∀m : ℕ. ∃v : Norm. m ⊢ d ↘ v and m ⊢ d′ ↘ v.

Note that transitivity follows from determinism of read-back.

A partial function H : α ⇀ β is a pair (dom(H) : P(α), apply(H) : {a : α | a ∈ dom H} → β) where dom(H) and apply(H) respect the setoid equalities associated to α and β. We will write H(a) ⇂ “H(a) is defined” if there is a proof p that a ∈ dom(H), and then H(a) stands for apply(H)(a, p). Two partial functions H, H′ are equal H =_{α⇀β} H′ if they have equal domains and coincide pointwise (wrt. to setoid equalities); this makes α ⇀ β a setoid.

Raw interpretation of kinds. Let () denote the unit type with single inhabitant (). We define the candidate space ⟨k⟩ for simple kind k and an inhabitant ⊥^{k} : ⟨k⟩ by recursion on k:

\begin{aligned}⟨⋄⟩ & = & () \\ ⟨∗⟩ & = & Per(D × ()) \\ ⟨k → k′⟩ & = & (D × ⟨k⟩) ⇀ ⟨k′⟩ \end{aligned}  \begin{aligned}⊥^{⋄} & = & () \\ ⊥^{∗} & = & Ne^{()} \\ ⊥^{k→k′}(G : D, G : ⟨k⟩) & = & ⊥^{k′} \end{aligned}

where Ne^{()} = Ne × () = {((e, ()), (e′, ())) | e = e′ ∈ Ne}. Extensional setoid equality F =_{⟨k⟩} F′ is defined along the way. We set ⟨⟨k⟩⟩ = Per(D×⟨k⟩). Note that ⟨⟨⋄⟩⟩ = ⟨∗⟩.

Sort interpretation. For K : D, K : ⟨⟨k⟩⟩ we define \underline{K}, \overline{K} : ⟨⟨k⟩⟩ and K ⊩ K, “K realizes K”, by

\begin{aligned}(F, F) = (F′, F′) ∈ \overline{K} & ⟺ & ↓^{K} F = ↓^{K} F′ ∈ Nf \\ (↑^{K} E, ⊥^{k}) = (↑^{K} E′, ⊥^{k}) ∈ \underline{K} & ⟺ & E = E′ ∈ Ne \\ K ⊩ K & ⟺ & \underline{K} ⊆ K ⊆ \overline{K} \end{aligned}

In words, code K realizes PER K iff equal inhabitants F of K reify to the same normal form, where K directs the amount of η-expansion during reification; and neutrals E can be reflected at code K into K. Equivalently, we could say K ⊩ K iff ↓^{K} ∘ π_{1} ∈ K → Nf, “↓^{K} after the first projection is a PER morphism from K to Nf”, and (E : DNe ↦ (↑^{K} E, ⊥^{k})) ∈ Ne → K, “↑^{K} paired with ⊥^{k} is a PER morphism from Ne to K”.

Lemma 3 (Least PER is a candidate). For all E ∈ Ne, E ⊩ ⊥^{∗} : ⟨⟨⋄⟩⟩.

Equality of candidates (K, K) = (K′, K′) ∈ \overline{\overline{k}} shall hold iff

1. K ⊩ K and K′ ⊩ K′.

2. K =_{⟨⟨k⟩⟩} K′ and ↓ K = ↓ K′ ∈ Nf.

3. ↑^{K} = ↑^{K′} ∈ Ne × {⊥^{k}} → K and ↓^{K} = ↓^{K′} ∈ π_{1}(K) → Nf.

This states that K and K′ are extensionally equal PERs, plus the associated codes K and K′ are reifiable, plus they are indistinguishable with respect to their own normal form and their directive behaviour during reification of inhabitants of K and reflection of neutrals into K. Now sort ∗ is interpreted by \overline{\overline{⋄}} and □ (informally) by ⋃_{k≠⋄} \overline{\overline{k}}.

Lemma 4. For all k, \overline{\overline{k}} is a PER over D × ⟨k⟩. If K ⊩ K then (K, K) ∈ \overline{\overline{k}}.

Lemma 5 (Interpretation of ∗). We have ∗ ⊩ \overline{\overline{⋄}} : ⟨⟨∗⟩⟩ and (∗, \overline{\overline{⋄}}) = (∗, \overline{\overline{⋄}}) ∈ \overline{\overline{∗}}.

Function space construction. For simple kinds k, l : SKi we define

∏k,l  : (K ∈ ⟨⟨k⟩⟩) → (K → ⟨⟨l⟩⟩) → ⟨⟨k → l⟩⟩
∏^{k,l} K L = {((F, F), (F′, F)) : (D × ⟨k → l⟩)^{2} | for all (G, G) = (G′, G′) ∈ K,
F · G ⇂, F′ · G′ ⇂, F(G, G) ⇂, F′(G′, G′) ⇂, and
(F · G, F(G, G)) = (F′ · G′, F′(G′, G′)) ∈ L(G, G)}.

In case l = ⋄ both F, F′ : ⟨k → l⟩ = () are trivial and we let the application F(G, G) be defined as (). Otherwise, F, F′ : D × ⟨k⟩ ⇀ ⟨l⟩.

∏^{k,l} K L is indeed a PER, the proof is standard. The definition above is a bit abstract, the following table conveys some intuition about ∏^{k,l}.

k  l description  PTS rule

⋄ ⋄ dependent function space (∗, ∗, ∗) not ⋄ ⋄ universal quantification (□, ∗, ∗) ⋄ not ⋄ indexed kind formation (∗, □, □) not ⋄ not ⋄ function kind formation (□, □, □)

Where is the impredicativity? For k = ∗ and l = ⋄ we should recover the impredicative quantification of System F. Let us look at the definition of this instance ∏^{∗,⋄} : (K ∈ Per(D × ⟨∗⟩)) → (K → ⟨∗⟩) → ⟨∗⟩. Remember that ⟨∗⟩ = Per(D × ()), thus, modulo the isomorphism D × () ≅ D we get

\begin{aligned}∏^{∗,⋄} K L = \{(F, F′) : D^{2} & | & ∀G, G′ : D, G, G′ : ⟨∗⟩. \\ & & (G, G) = (G′, G′) ∈ K ⟹ F · G = F′ · G′ ∈ L(G, G)\}. \end{aligned}

Hence, to obtain a new element ∏ K L : ⟨∗⟩ we quantify over all G, G′ : ⟨∗⟩ — there is System F impredicativity.

Lemma 6 (Function type formation, introduction, and elimination). Let K, K′ : ⟨⟨k⟩⟩, L, L′ ∈ K → ⟨⟨l⟩⟩, and F, F′ ∈ K → ⟨l⟩. The following inferences are valid in the model.

\frac{\begin{matrix}(K, K) = (K′, K′) ∈ \overline{\overline{k}} \\ (L · G, L(G, G)) = (L′ · G′, L′(G′, G′)) ∈ \overline{\overline{l}} for all (G, G) = (G′, G′) ∈ K \end{matrix}}{(\underline{Π} K L, ∏ K L) = (\underline{Π} K′ L′, ∏ K′ L′) ∈ \overline{\overline{k → l}}}

\frac{(F · G, F(G, G)) = (F′ · G′, F′(G′, G′)) ∈ L(G, G) for all (G, G) = (G′, G′) ∈ K}{(F, F) = (F′, F′) ∈ ∏ K L}

\frac{(F, F) = (F′, F′) ∈ ∏ K L (G, G) = (G′, G′) ∈ K}{(F · G, F(G, G)) = (F′ · G′, F′(G′, G′)) ∈ L(G, G)}

Proof. Introduction and elimination follow directly from the definition of ∏ K L. The formation rule follows from properties of reflection and reification at function types [ACD07].

6 Soundness of the Model

We extend the raw semantic interpretation to shapes by setting ⟨÷, k⟩ = ⟨k⟩ and ⟨≐, k⟩ = ⟨⟨k⟩⟩, and to simple kinding contexts via ⟨()⟩ = () and ⟨γ, k⟩ = ⟨γ⟩ × ⟨k⟩.

Interpretation. By induction on M/σ we simultaneously define the partial functions [[M]]_{η;γ;} : (ρ : ⟨γ⟩) ⇀ ⟨|M|_{γ}⟩ and [[σ]]_{η;γ;} : (ρ : ⟨γ⟩) ⇀ ⟨|σ|_{γ}⟩.

\begin{aligned}[[∗]]_{η;γ;ρ} & = & \overline{\overline{⋄}} : ⟨⟨∗⟩⟩ \\ [[Π U T]]_{η;γ;ρ} & = & ∏^{|U|._{=},|T |._{=}}[[U]]_{η;γ;ρ} ((G, G) ∈ [[U]]_{η;γ;ρ} ↦ [[T]]_{η,G;γ,|U|._{=};ρ,G}) \\ [[v_{0}]]_{η;γ,k;ρ,G} & = & G : ⟨k⟩ \\ [[λ U M]]_{η;γ;ρ} & = & ((G, G) ∈ [[U]]_{η;γ;ρ} ↦ [[M]]_{η,G;γ,|U|._{=};ρ,G}) \\ [[M N]]_{η;γ;ρ} & = & [[M]]_{η;γ;ρ}(⦇N⦈_{η}, [[N]]_{η;γ;ρ}) \\ [[M σ]]_{η;γ;ρ} & = & [[M]]_{⦇σ⦈_{η};|σ|_{γ};[[σ]]_{η;γ;ρ}} \\ [[↑]]_{η;γ,k;ρ,o} & = & ρ : ⟨γ⟩ \\ [[id]]_{η;γ;ρ} & = & ρ : ⟨γ⟩ \\ [[(σ, M)]]_{η;γ;ρ} & = & [[σ]]_{η;γ;ρ}, [[M]]_{η;γ;ρ} : ⟨|σ|_{γ}, |M|_{γ}^{÷}⟩ \\ [[σ τ]]_{η;γ;ρ} & = & [[σ]]_{⦇τ⦈_{η};|τ|_{γ};[[τ]]_{η;γ;ρ}} : ⟨|σ|_{|τ|_{γ}} ⟩ \end{aligned}

The prime source of partiality is the potential undefinedness of ⦇N⦈_{η} in the interpretation of the application M N. Contrast this to Barras and Werner [BW97] where ⦇N⦈_{η} is gone and with it the large eliminations.

The precise conditions for definedness can be extracted mechanically from this definition, for instance, [[Π U T]]_{η;γ;ρ} is defined iff [[U]]_{η;γ;ρ} is defined and for all (G, G) ∈

[[U]]_{η;γ;ρ}, [[T]]_{η,G;γ,|U|._{=};η;G} is defined.

Validity. We define the relation (η; ρ) = (η′; ρ′) ∈ [[Γ]] for η, η′ : Env and ρ, ρ′ : ⟨|Γ |⟩ inductively by the rules

\overline{((); ()) = ((); ()) ∈ [[()]]} \frac{(η; ρ) = (η′; ρ′) ∈ [[Γ]] (G, G) = (G′, G′) ∈ [[T]]_{η;|Γ |;ρ}}{(η, G; ρ, G) = (η, G′; ρ, G′) ∈ [[Γ, T]]}

There is an implicit premise [[T]]_{η;|Γ |;ρ} ⇂ in the second rule. By induction on Γ we simultaneously define the following propositions:

() ⊧  :⟺ true
Γ, T ⊧  :⟺ Γ ⊧ T : □
Γ ⊧ κ = κ′ : □  :⟺ Γ ⊧ and for all (η, ρ) = (η′, ρ′) ∈ [[Γ]],

(⦇κ⦈_{η}, [[κ]]_{η;|Γ |;ρ}) = (⦇κ′⦈_{η′}, [[κ′]]_{η′;|Γ |;ρ′}) ∈ \overline{\overline{|κ| ._{=}}}

Γ ⊧ M = M′ : T ≢ □ :⟺ Γ ⊧ T : □ and for all (η, ρ) = (η′, ρ′) ∈ [[Γ]],

(⦇M⦈_{η}, [[M]]_{η;|Γ |;ρ}) = (⦇M′⦈_{η′}, [[M′]]_{η′;|Γ |;ρ′}) ∈ [[T]]_{η;|Γ |;ρ}

Γ ⊧ M : T  :⟺ Γ ⊧ M = M : T
Γ ⊧ σ = σ′ : Δ  :⟺ Γ ⊧ and Δ ⊧ and for all (η, ρ) = (η′, ρ′) ∈ [[Γ]],

(⦇σ⦈_{η}, [[σ]]_{η;|Γ |;ρ}) = (⦇σ′⦈_{η′}, [[σ′]]_{η′;|Γ |;ρ′}) ∈ [[Δ]]

Γ ⊧ σ : Δ  :⟺ Γ ⊧ σ = σ : Δ

Lemma 7. If Γ ⊧ then = ∈ [[Γ]] is a PER.

Theorem 2 (Fundamental theorem). If Γ ⊢ J then Γ ⊧ J.

Proof. Simultaneously by for all judgements J by induction on Γ ⊢ J.

Theorem 3 (Completeness of NbE). If Γ ⊢ M = M′ : T then nbe_{Γ}^{T} M ≡ nbe_{Γ}^{T} M′.

Proof. Define ρ_{Γ} by the clauses ρ_{()} = () and ρ_{Γ,U} = ρ_{Γ} , ⊥^{|U|._{=}} and prove that (η_{Γ} , ρ_{Γ}) ∈ [[Γ]] by induction on Γ. Let (F, F) = (⦇M⦈_{η_{Γ}} , [[M]]_{η_{Γ};|Γ |;ρ_{Γ}}) and (F′, F′) analogously. If T ≢ □ then with (K, K) = (⦇T ⦈_{η_{Γ}} , [[T]]_{η_{Γ};|Γ |;ρ_{Γ}}) we obtain (F, F) = (F′, F′) ∈ K and K ⊩ K by the fundamental theorem. Hence, ↓^{K} F = ↓^{K} F′ ∈ Nf, so in particular R_{∥Γ ∥}^{nf} (↓^{K} F) ≡ R_{∥Γ ∥}^{nf} (↓^{K} F′). If T ≡ □ then the fundamental theorem

yields (F, F) = (F′, F′) ∈ \overline{\overline{k}} for k = |M| ._{=} which also implies ↓ F = ↓ F′ ∈ Nf.

6.1 On Consistency

From our PER model we can prove the consistency of CoC as follows. Add a new type constant ∅, the empty type, with rules Γ ⊢ ∅ : ∗ and Γ ⊢ ∅ = ∅ : ∗ and semantics [[∅]]_{η;γ;ρ} = Ne^{()}.

Theorem 4 (Consistency). ⊬ t : ∅.

Proof. Let a = ⦇t⦈_{id} and observe that a cannot mention a de Bruijn level x_{j}. Since a ∈ Ne by the fundamental theorem (Thm .2), we have 0 ⊢^{ne} a ↘ n for some n. But this means that a is of the shape x_{j} d for some j, contradiction!

7 Conclusion

We have built a model for the Calculus of Constructions with typed βη-equality which proves termination and completeness of normalization by evaluation. The model supports extensions of the CoC by small inductive types (“small” meaning “in ∗”) and large (aka strong) eliminations into ∗, i. e., types defined by recursion [Wer92]. The model is formalizable directly in impredicative dependent type theories with inductive definitions, e. g., in the Calculus of Inductive Constructions (CIC) [INR08].

This work is a first step towards a metatheory of CIC with typed βη-equality using normalization by evaluation. The long term goal is a correctness proof for the Coq type checker in the presence of η. However, a number of things need to be done:

– Construct a Kripke logical relation between expressions and values that proves the soundness of NbE without external reference to injectivity. As a consequence, we obtain soundness and completeness of the type checker of Section 3.

– Extend the calculus to more universes and to large inductive types. This will break simple kinding, requiring a new way to bootstrap the model. The usual technique are inaccessible cardinals [Luo89,Gog94,Miq00], however, we seek a more direct representation in type theory.

Acknowledgments. The author acknowledges the support of INRIA through a guest researcher fellowship. He would like to thank Hugo Herbelin and Pierre-Louis Curien for the invitation, and Bruno Barras and Benjamin Werner for discussions on the topic of this work. Their [Wer92,BW97] and Stefanova and Geuver’s work [SG96] were a major help in understanding models for the CoC. Thanks also to the anonymous referees for their comments which helped to improve the quality of this paper.

References

[Abe10] Andreas Abel. Towards Normalization by Evaluation for the Calculus of Constructions (Extended Version). Available on the author’s homepage, 2010.

[ACCL91] Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. JFP, 1(4):375–416, 1991.

[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.

[ACP09] Andreas Abel, Thierry Coquand, and Miguel Pagano. A modular type-checking algorithm for type theory with singleton types and proof irrelevance. In TLCA’09, volume 5608 of LNCS, pages 5–19. Springer, 2009.

[Ada06] Robin Adams. Pure type systems with judgemental equality. JFP, 16(2):219–246, 2006.

[Bar09] Bruno Barras. Sets in Coq, Coq in sets. In The 1st Coq Workshop, Proceedings. Technische Universität München, 2009.

[BW97] Bruno Barras and Benjamin Werner. Coq in Coq. Available on the WWW, 1997.

[Car86] John Cartmell. Generalised algebraic theories and contextual categories. APAL, pages 32–209, 1986.

[CG90] Thierry Coquand and Jean Gallier. A proof of strong normalization for the theory of constructions using a kripke-like interpretation. In Proceedings of the First Workshop on Logical Frameworks, 1990.

[Cha09] James Chapman. Type Checking and Normalization. PhD thesis, School of Computer Science, University of Nottingham, 2009.

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

[Dan07] Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In TYPES’06, volume 4502 of LNCS, pages 93–109. Springer, 2007.

[Geu94] Herman Geuvers. A short and flexible proof of strong normalization for the Calculus of Constructions. In Types for Proofs and Programs, Int. Workshop TYPES ’94, volume 996 of LNCS, pages 14–38, Båstad, Sweden, 1994. Springer.

[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.

[GN91] Herman Geuvers and Mark-Jan Nederhof. Modular proof of strong normalization for the calculus of constructions. JFP, 1(2):155–189, 1991.

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

[Gon04] Georges Gonthier. A computer-checked proof of the four colour theorem. Technical report, Microsoft Research, 2004. Available at http://research.microsoft.com/˜ gonthier/.

[Gra09] Johan Granström. Reference and Computation in Intuitionistic Type Theory. PhD thesis, Mathematical Logic, Uppsala University, 2009.

[Hue89] Gérard Huet. The constructive engine. In 2nd European Symposium on Programming, Nancy, March 1988, 1989. Final version in anniversary volume Theoretical Computer Science in memory of Gift Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.

[INR08] INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.2 edition, 2008. http://coq.inria.fr/.

[Ler06] Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL’06, pages 42–54. ACM, 2006.

[Luo89] Zhaohui Luo. ECC, an Extended Calculus of Constructions. In LICS’89, pages 386– 395. IEEE CS Press, 1989.

[Miq00] Alexandre Miquel. A model for impredicative type systems, universes, intersection types and subtyping. In LICS’00, pages 18–29, 2000.

[MW03] Alexandre Miquel and Benjamin Werner. The not so simple proof-irrelevant model of CC. In TYPES’02, volume 2646 of LNCS, pages 240–258. Springer, 2003.

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

[Pol06] Randy Pollack. The constructive engine. Talk presented at the TYPES Workshop Curry-Howard Implementation Techniques - Connecting Humans And Theorem provers, CHIT-CHAT 2006, Radboud University, Nijmegen, The Netherlands, 2006.

[SG96] Milena Stefanova and Herman Geuvers. A simple model construction for the calculus of constructions. In TYPES’95, volume 1158 of LNCS, pages 249–264. Springer, 1996.

[Wer92] Benjamin Werner. A normalization proof for an impredicative type system with large eliminations over integers. In TYPES’92, pages 341–357, 1992.