Yale University Department of Computer Science

A Type System for Certified Binaries

Zhong Shao Bratin Saha Valery Trifonov Nikolaos Papaspyrou Yale University

YALEU/DCS/TR-1211 March 2001 (revised September 2001)

This research is based on work supported in part by DARPA OASIS grant F30602-99-1-0519, NSF grant CCR-9901011, and NSF ITR grant CCR-0081590. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies.

Abstract

A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In this paper, we present a general framework for explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects while still maintaining decidable typechecking. We show how to integrate an entire proof system (the calculus of inductive constructions) into a compiler intermediate language and how the intermediate language can undergo complex transformations (CPS and closure conversion) while preserving proofs represented in the type system. Our work provides a foundation for the process of automatically generating certified binaries in a type-theoretic framework.

A Type System for Certified Binaries

Zhong Shao Bratin Saha Valery Trifonov Nikolaos Papaspyrou Department of Computer Science, Yale University New Haven, CT 06520-8285, U.S.A.

                         {shao, saha, trifonov, nickie}@cs.yale.edu

Technical Report YALEU/DCS/TR-1211 March 2001 (revised September 2001)

Abstract

A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In this paper, we present a general framework for explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects while still maintaining decidable typechecking. We show how to integrate an entire proof system (the calculus of inductive constructions) into a compiler intermediate language and how the intermediate language can undergo complex transformations (CPS and closure conversion) while preserving proofs represented in the type system. Our work provides a foundation for the process of automatically generating certified binaries in a typetheoretic framework.

1 Introduction

Proof-carrying code (PCC), as pioneered by Necula and Lee [30, 29], allows a code producer to provide a machine-language program to a host, along with a formal proof of its safety. The proof can be mechanically checked by the host; the producer need not be trusted because a valid proof is incontrovertible evidence of safety.

The PCC framework is general because it can be applied to certify arbitrary data objects with complex specifications [32, 2]. For example, the Foundational PCC system [3] can certify any property expressible in Church’s higher-order logic. Harper et al. [19, 7] call all these proof-carrying constructs certified binaries (or deliverables [7]). A certified binary is a value (which can be a function, a data structure, or a combination of both) together with a proof that the value satisfies a given specification.

Unfortunately, little is known on how to construct or generate certified binaries. Existing certifying compilers [31, 9] have focused on simple memory and control-flow safety only. Typed intermediate languages [22] and typed assembly languages [28] are effective techniques for automatically generating certified code; however, none of these type systems can rival the expressiveness of the actual higher-order logic as used in some PCC systems [3].

In this paper, we present a type-theoretic framework for constructing, composing, and reasoning about certified binaries. Our plan is to use the formulae-as-types principle [24] to represent propositions and proofs in a general type system, and then to investigate their relationship with compiler intermediate and assembly languages. We show how to integrate an entire proof system (the calculus of inductive constructions [35, 11]) into an intermediate language, and how to define complex transformations (CPS and closure conversion) of programs in this language so that they preserve proofs represented in the type system. Our paper builds upon a large body of previous work in the logic and theorem-proving community (see Barendregt et al. [5, 4] for a good summary), and makes the following new contributions:

• We show how to design new typed intermediate languages that are capable of representing and manipulating propositions and proofs. In particular, we show how to maintain decidability of typechecking when reasoning about certified programs that involve effects. This is different from the work done in the logic community which focuses on strongly normalizing (primitive recursive) programs.

• We maintain a phase distinction between compile-time typechecking and run-time evaluation. This property is often lost in the presence of dependent types (which are necessary for representing proofs in predicate logic). We achieve this by never having the type language (see Section 3) dependent on the computation language (see Section 4). Proofs are instead always represented at the type level using dependent kinds.

• We show how to use propositions to express program invariants and how to use proofs to serve as static capabilities. Following Xi and Pfenning [44], we use singleton types [23] to support the necessary interaction between the type and computation languages. We can assign an accurate type to unchecked vector (or array) access (see Section 4.2). Xi and Pfenning [44] can achieve the same using constraint checking, but their system does not support arbitrary propositions and (explicit) proofs, so it is less general than ours.

• We use a single type language to typecheck different compiler intermediate languages. This is crucial because it is impractical to have separate proof libraries for each intermediate language. We achieve this by using inductive definitions to define all types used to classify computation terms. This in turn nicely fits our work on (fully reflexive) intensional type analysis [39] into a single system.

• We show how to perform CPS and closure conversion on our intermediate languages while still preserving proofs represented in the type system. Existing algorithms [28, 21, 26, 6] all require that the transformation be performed on the entire type language. This is impractical because proofs are large in size; transforming them can alter their meanings and break the sharing among different languages. We present new techniques that completely solve these problems (Sections 5–6).

This research is based on work supported in part by DARPA OASIS grant F30602-99-1-0519, NSF grant CCR-9901011, and NSF ITR grant CCR-0081590. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies.

• Our type language is a variant of the calculus of inductive constructions [35, 11]. Following Werner [41], we give rigorous proofs for its meta-theoretic properties (subject reduction, strong normalization, confluence, and consistency of the underlying logic). We also give the soundness proof for our sample computation language. See Sections 3 and 4, and the appendix for more details.

As far as we know, our work is the first comprehensive study on how to incorporate higher-order predicate logic (with inductive terms and predicates) into typed intermediate languages. Our results are significant because they open up many new exciting possibilities in the area of type-based language design and compilation. The fact that we can internalize a very expressive logic into our type system means that formal reasoning traditionally done at the meta level can now be expressed inside the actual language itself. For example, much of the past work on program verification using Hoare-like logics may now be captured and made explicit in a typed intermediate language.

From the standpoint of type-based language design, recent work [22, 44, 13, 15, 40, 39] has produced many specialized, increasingly complex type systems, each with its own metatheoretical proofs, yet it is unclear how they will fit together. We can hope to replace them with one very general type system whose meta theory is proved once and for all, and that allows the definition of specialized type operators via the general mechanism of inductive definitions. For example, inductive definitions subsume and generalize earlier systems on intensional type analysis [22, 14, 39].

We have started implementing our new type system in the FLINT compiler [36, 37], but making the implementation realistic still involves solving many remaining problems (e.g., efficient proof representations). Nevertheless, we believe our current contributions constitute a significant step toward the goal of providing a practical end-to-end compiler that generates certified binaries.

2 Approach

Our main objectives are to design typed intermediate and low-level languages that can directly manipulate propositions and proofs, and then to use them to certify realistic programs. We want our type system to be simple but general; we also want to support complex transformations (CPS and closure conversion) that preserve proofs represented in the type system. In this section, we describe the main challenges involved in achieving these goals and give a high-level overview of our main techniques.

Before diving into the details, we first establish a few naming conventions that we will use in the rest of this paper. Typed intermediate languages are usually structured in the same way as typed λ-calculi. Figure 1 gives a fragment of a richly typed λ-calculus, organized into four levels: kind schema (kscm) u, kind κ, type τ, and expression (exp) e. If we ignore kind schema and other extensions, this is just the polymorphic λ-calculus F_{ω} [18].

We divide each typed intermediate language into a type sublanguage and a computation sub-language. The type language contains the top three levels. Kind schemas classify kind terms while kinds classify type terms. We often say that a kind term κ has kind schema u, or a type term τ has kind κ. We assume all kinds used to classify type terms have kind schema Kind, and all types used to classify expressions have kind Ω. Both the function type τ_{1} → τ_{2} and the polymorphic type ∀t : κ. τ have kind Ω. Following the tradition, we sometimes say “a kind κ” to imply that κ has kind schema Kind, “a type τ” to imply that τ has kind Ω, and “a type constructor τ” to imply that τ has kind “κ→ ⋯→Ω.” Kind terms with other kind schemas, or type terms with other kinds are strictly referred to as “kind terms” or “type terms.” the type language:

(kscm) u ::= Kind | …
(kind) κ ::= κ_{1} →κ_{2} | Ω | …
(type) τ ::= t | λt:κ. τ | τ_{1} τ_{2} | τ_{1} →τ_{2} | ∀t:κ. τ | …

the computation language:

(exp) e ::= x | λx:τ. e | e_{1} e_{2} | Λt:κ. e | e[τ] | …

Figure 1: Typed λ-calculi—a skeleton

The computation language contains just the lowest level which is where we write the actual program. This language will eventually be compiled into machine code. We often use names such as computation terms, computation values, and computation functions to refer to various constructs at this level.

2.1 Representing propositions and proofs

The first step is to represent propositions and proofs for a particular logic in a type-theoretic setting. The most established technique is to use the formulae-as-types principle (a.k.a. the Curry-Howard correspondence) [24] to map propositions and proofs into a typed λ-calculus. The essential idea, which is inspired by constructive logic, is to use types (of kind Ω) to represent propositions, and expressions to represent proofs. A proof of an implication P ⊃Q is a function object that yields a proof of proposition Q when applied to a proof of proposition P. A proof of a conjunction P ∧ Q is a pair (e_{1}, e_{2}) such that e_{1} is a proof of P and e_{2} is a proof of Q. A proof of disjunction P ∨Q is a pair (b, e)—a tagged union—where b is either 0 or 1 and if b=0, then e is a proof of P; if b=1 then e is a proof of Q. There is no proof for the false proposition. A proof of a universally quantified proposition ∀x∈B.P (x) is a function that maps every element b of the domain B into a proof of P (b) where P is a unary predicate on elements of B. Finally, a proof of an existentially quantified proposition ∃x∈B.P (x) is a pair (b, e) where b is an element of B and e is a proof of P (b).

Proof-checking in the logic now becomes typechecking in the corresponding typed λ-calculus. There has been a large body of work done along this line in the last 30 years; most type-based proof assistants are based on this fundamental principle. Barendregt et al. [5, 4] give a good survey on previous work in this area.

2.2 Representing certified binaries

Under the type-theoretic setting, a certified binary S is just a pair (v, e) that consists of:

• a value v of type τ where v could be a function, a data structure, or any combination of both;

• and a proof e of P (v) where P is a unary predicate on elements of type τ.

Here e is just an expression with type P (v). The predicate P is a dependent type constructor with kind τ →Ω. The entire package S has a dependent strong-sum type Σx:τ.P (x).

For example, suppose Nat is the domain for natural numbers and Prime is a unary predicate that asserts an element of Nat as a prime number, we introduce a type nat representing Nat, and a type constructor prime (of kind nat→Ω) representing Prime. We can build a certified prime-number package by pairing a value v (a natural number) with a proof for the proposition prime(v); the resulting certified binary has type Σx:nat. prime(x).

Function values can be certified in the same way. Given a function f that takes a natural number and returns another one as the result (i.e., f has type nat → nat), in order to show that f always maps a prime to another prime, we need a proof for the following proposition:

∀x∈Nat. Prime(x) ⊃ Prime(f(x))

In a typed setting, this universally quantified proposition is represented as a dependent product type:

Πx:nat. prime(x) → prime(f(x))

The resulting certified binary has type

Σf:nat → nat. Πx:nat. prime(x) → prime(f(x))

Here the type is not only dependent on values but also on function applications such as f(x), so verifying a certified binary involves typechecking the proof which in turn requires evaluating the underlying function application.

2.3 The problems with dependent types

The above scheme unfortunately fails to work in the context of typed intermediate (or assembly) languages. There are at least four problems with dependent types; the third and fourth are present even in the general context.

First, real programs often involve effects such as assignment, I/O, or non-termination. Effects interact badly with dependent types. In our previous example, suppose the function f does not terminate on certain inputs; then clearly, typechecking—which could involve applying f—would become undecidable. It is possible to use the effect discipline [38] to force types to be dependent on pure computation only, but this does not work in some typed λ-calculi; for example, a “pure” term in Girard’s λU [18] could still diverge.

Even if applying f does not involve any effects, we still have more serious problems. In a type-preserving compiler, the body of the function f has to be compiled down to typed low-level languages. A few compilers perform typed CPS conversion [28], but in the presence of dependent types, this is a very difficult problem [6]. Also, typechecking in low-level languages would now require performing the equivalent of β-reductions on the low-level (assembly) code; this is awkward and difficult to support cleanly.

Third, it is important to maintain a phase distinction between compile-time typechecking and run-time evaluation. Having dependent strong-sum and dependent product types makes it harder to preserve this property. It is also difficult to support first-class certified binaries.

Finally, it would be nice to support a notion of subset types [10, 33]. A certified binary of type Σx:nat. prime(x) contains a natural number v and a proof that v is a prime. However, in some cases, we just want v to belong to a subset type {x:nat | prime(x)}, i.e., v is a prime number but the proof of this is not together with v; instead, it can be constructed from the current context.

2.4 Separating the type and computation languages

We solve these problems by making sure that our type language is never dependent on the computation language. Because the actual program (i.e., the computation term) would have to be compiled down to assembly code in any case, it is a bad idea to treat it as part of types. This strong separation immediately gives us back the phase-distinction property.

To represent propositions and proofs, we lift everything one level up: we use kinds to represent propositions, and type terms to represent proofs. The domain Nat is now represented by a kind Nat; the predicate Prime is represented by a dependent kind term Prime which maps a type term of kind Nat into a proposition. A proof for proposition Prime(n) certifies that the type term n is a prime number.

To maintain decidable typechecking, we insist that the type language is strongly normalizing and free of side effects. This is possible because the type language no longer depends on any runtime computation. Given a type-level function g of kind Nat→Nat, we can certify that it always maps a prime to another prime by building a proof τ_{p} for the following proposition, now represented as a dependent product kind:

Πt:Nat.Prime(t)→Prime(g(t)).

Essentially, we circumvent the problems with dependent types by replacing them with dependent kinds and by lifting everything (in the proof language) one level up.

To reason about actual programs, we still have to connect terms in the type language with those in the computation language. We follow Xi and Pfenning [44] and use singleton types [23] to relate computation values to type terms. In the previous example, we introduce a singleton type constructor snat of kind Nat→Ω. Given a type term n of kind Nat, if a computation value v has type snat(n), then v denotes the natural number represented by n.

A certified binary for a prime number now contains three parts: a type term n of kind Nat, a proof for the proposition Prime(n), and a computation value of type snat(n). We can pack it up into an existential package and make it a first-class value with type:

∃n:Nat.∃t:Prime(n).snat(n).

Here we use ∃ rather than Σ to emphasize that types and kinds are no longer dependent on computation terms. Under the erasure semantics [16], this certified binary is just an integer value of type snat(n) at run time.

A value v of the subset type (for prime numbers) would simply have type snat(n) as long as we can construct a proof for Prime(n) based on the information from the context.

We can also build certified binaries for programs that involve effects. Returning to our example, assume again that f is a function in the computation language which may not terminate on some inputs. Suppose we want to certify that if the input to f is a prime, and the call to f does return, then the result is also a prime. We can achieve this in two steps. First, we construct a type-level function g of kind Nat → Nat to simulate the behavior of f (on all inputs where f does terminate) and show that f has the following type:

∀n:Nat. snat(n) → snat(g(n))

Here following Figure 1, we use ∀ and → to denote the polymorphic and function types for the computation language. The type for f says that if it takes an integer of type snat(n) as input and does not loop forever, then it will return an integer of type snat(g(n)). Second, we construct a proof τ_{p} showing that g always maps a prime to another prime. The certified binary for f now also contains three parts: the type-level function g, the proof τ_{p}, and the computation function f itself. We can pack it into an existential package with type:

∃g:Nat→Nat. ∃p:(Πt:Nat.Prime(t)→Prime(g(t))).
∀n:Nat. snat(n) → snat(g(n))

Notice this type also contains function applications such as g(n), but g is a type-level function which is always strongly normalizing, so typechecking is still decidable.

We can also restrict f so that it can only be applied to prime numbers; all we need is to add an additional proof argument, so f has type:

∀n:Nat.∀t:Prime(n). snat(n) → snat(g(n)).

Here, the parameter t serves as a static capability; a proof for Prime(n) exists only if n is indeed a prime.

2.5 Designing the type language

We can incorporate propositions and proofs into typed intermediate languages, but designing the actual type language is still a challenge. For decidable typechecking, the type language should not depend on the computation language and it must satisfy the usual meta-theoretical properties (e.g. strong normalization).

But the type language also has to fulfill its usual responsibilities. First, it must provide a set of types (of kind Ω) to classify the computation terms. A typical compiler intermediate language supports a large number of basic type constructors (e.g., integer, array, record, tagged union, and function). These types may change their forms during compilation, so different intermediate languages may have different definitions of Ω; for example, a computation function at the source level may be turned into CPS-style, or later, to one whose arguments are machine registers [28]. We also want to support intensional type analysis [22] which is crucial for typechecking runtime services [27].

Our solution is to provide a general mechanism of inductive definitions in our type language and to define each such Ω as an inductive kind. This was made possible only recently [39] and it relies on the use of polymorphic kinds. Taking the type language in Figure 1 as an example, we add kind variables k and polymorphic kinds Πk: u. κ, and replace Ω and its associated type constructors with inductive definitions (not shown):

(kscm) u ::= Kind | …
(kind) κ ::= κ_{1} →κ_{2} | k | Πk:u. κ | …
(type) τ ::= t | λt:κ. τ | τ_{1} τ_{2} | λk:u. τ | τ[κ] | …

At the type level, we add kind abstraction λk: u. τ and kind application τ[κ]. The kind Ω is now inductively defined as follows (see Sections 3–4 for more details):

Inductive Ω : Kind := → → : Ω→Ω→Ω | ∀ ∀ : Πk:Kind. (k →Ω)→Ω ⋮

Here → → and ∀ ∀ are two of the constructors (of Ω). The polymorphic type ∀t: κ. τ is now written as ∀ ∀[κ] (λt: κ. τ); the function type τ_{1} →τ_{2} is just → →τ_{1}τ_{2}.

Inductive definitions also greatly increase the programming power of our type language. We can introduce new data objects (e.g., integers, lists) and define primitive recursive functions, all at the type level; these in turn are used to help model the behaviors of the computation terms.

To have the type language double up as a proof language for higher-order predicate logic, we add dependent product kind Πt: κ_{1}. κ_{2}, which subsumes the arrow kind κ_{1} → κ_{2}; we also add kind-level functions to represent predicates. Thus the type language naturally becomes the calculus of inductive constructions [35].

Notice standard formulation of Church’s higher-order logic puts propositions at the same level as terms (which are type terms in our setup); proofs are then represented at a level below (parallel to our computation language). This does not work because we already require polymorphic kinds for the inductive definition of Ω; with impredicative polymorphism on both the kind and type levels, the proof language becomes Girard’s λU [18] which is known to be inconsistent.

2.6 Proof-preserving compilation

Even with a proof system integrated into our intermediate languages, we still have to make sure that they can be CPS- and closure-converted down to low-level languages. These transformations should preserve proofs represented in the type system; in fact, they should not traverse the proofs at all since doing so is impractical with large proof libraries.

These challenges are non-trivial but the way we set up our type system makes it easier to solve them. First, because our type language does not depend on the computation language, we do not have the difficulties involved in CPS-converting dependently typed λ-calculi [6]. Second, all our intermediate languages share the same type language thus also the same proof library; this is possible because the Ω kind (and the associated types) for each intermediate language is just a regular inductive definition.

Finally, a type-preserving program transformation often requires translating the source types (of the source Ω kind) into the target types (of the target Ω kind). Existing CPS- and closureconversion algorithms [28, 21, 26] all perform such translation at the meta-level; they have to go through every type term (thus every proof term in our setting) during the translation, because any type term may contain a sub-term which has the source Ω kind. In our framework, the fact that each Ω kind is inductively defined means that we can internalize and write the type-translation function inside our type language itself. This leads to elegant algorithms that do not traverse any proof terms but still preserve typing and proofs (see Sections 5–6 for details).

2.7 Putting it all together

A certifying compiler in our framework will have a series of intermediate languages, each corresponding to a particular stage in the compilation process; all will share the same type language. An intermediate language is now just the type language plus the corresponding computation terms, along with the inductive definition for the corresponding Ω kind. In the rest of this paper, we first give a formal definition of our type language (which will be named as TL from now on) in Section 3; we then present a sample computation language λ_{H} in Section 4; we show how λ_{H} can be CPS- and closure-converted into low-level languages in Sections 5–6; finally, we discuss related work and then conclude.

3 The Type Language TL

Our type language TL resembles the calculus of inductive constructions (Cic) implemented in the Coq proof assistant [25]. This is a great advantage because Coq is a very mature system and it has a large set of proof libraries which we can potentially reuse. For this paper, we decided not to directly use Cic as our type language for three reasons. First, Cic contains some features designed for program extraction [34] which are not required in our case (where proofs are only used as specifications for the computation terms). Second, as far as we know, there are still no formal studies covering the entire Cic language. Third, for theoretical purposes, we want to understand what are the most essential features for modeling certified binaries.

Motivations Following the discussion in Section 2.5, we organize TL into the following three levels:

(kscm) u ::= z | Πt:κ. u | Πk:u_{1}. u_{2} | Kind
(kind) κ ::= k | λt:κ_{1}. κ_{2} | κ[τ] | λk:u. κ | κ_{1} κ_{2} | Πt:κ_{1}. κ_{2} | Πk:u. κ | Πz:Kscm. κ | Ind(k:Kind){κ⃗} | Elim[κ′, u](τ){κ⃗}

(type) τ ::= t | λt:κ. τ | τ_{1} τ_{2} | λk:u. τ | τ[κ] | λz:Kscm. τ | τ[u] | Ctor (i, κ) | Elim[κ′, κ](τ′){τ⃗}

Here kind schemas (kscm) classify kind terms while kinds classify type terms. There are variables at all three levels: kind-schema variables z, kind variables k, and type variables t. We have an external constant Kscm classifying all the kind schemas; essentially, TL has an additional level above kscm, of which Kscm is the sole member.

A good way to comprehend TL is to look at its five Π constructs: there are three at the kind level and two at the kind-schema level. We use a few examples to explain why each of them is necessary. Following the tradition, we use arrow terms (e.g., κ_{1} →κ_{2}) as a syntactic sugar for the non-dependent Π terms (e.g., Πt:κ_{1}. κ_{2} is non-dependent if t does not occur free in κ_{2}).

• Kinds Πt : κ_{1}. κ_{2} and κ_{1} → κ_{2} are used to typecheck the type-level function λt : κ. τ and its application form τ_{1} τ_{2}. Assuming Ω and Nat are inductive kinds (defined later) and Prime is a predicate with kind schema Nat → Kind, we can write a type term such as λt : Ω. t which has kind Ω → Ω, a type-level arithmetic function such as plus which has kind Nat → Nat → Nat, or the universally quantified proposition in Section 2.2 which is represented as a kind Πt:Nat.Prime(t)→Prime(g(t)).

• Kinds Πk : u. κ and u → κ are used to typecheck the typelevel kind abstraction λk: u. τ and its application form τ[κ]. As mentioned in Section 2.5, this is needed to support intensional analysis of quantified types [39]. It can also be used to define logic connectives and constants, e.g.

True : Kind = Πk:Kind. k →k
False : Kind = Πk:Kind. k

True has the polymorphic identity as a proof:

id : True = λk:Kind. λt:k. t

but False is not inhabited (this is essentially the consistency property of TL which we will show later).

• Kind Πz : Kscm. κ is used to typecheck the type-level kindschema abstraction λz : Kscm. τ and its application form τ[u]. This is not in the core calculus of constructions [11]. We use it in the inductive definition of Ω (see Section 4) where both the ∀ ∀_{Kscm} and ∃∃_{Kscm} constructors have kind Πz: Kscm. (z →Ω)→Ω. These two constructors in turn allow us to typecheck predicate-polymorphic computation terms, which occur fairly often since the closure-conversion phase turns all functions with free predicate variables (e.g, Prime) into predicate-polymorphic ones.

• Kind schemas Πt: κ. u and κ → u are used to typecheck the kind-level type abstraction λt:κ_{1}. κ_{2} and its application form κ[τ]. The predicate Prime has kind schema Nat → Kind. A predicate with kind schema Πt: Nat. Prime(t)→Kind is only applicable to prime numbers. We can also define e.g. a binary relation:

LT : Nat→Nat→Kind

so that LT t_{1} t_{2} is a proposition asserting that the natural number represented by t_{1} is less than that of t_{2}.

Inductive Bool : Kind := true : Bool | false : Bool

Inductive Nat : Kind := zero : Nat | succ : Nat→Nat

plus : Nat→Nat→Nat

plus(zero) = λt:Nat. t
plus(succ t) = λt′:Nat. succ ((plus t) t′)

ifez : Nat→(Πk:Kind. k →(Nat→k)→k)

ifez(zero) = λk:Kind. λt_{1} :k. λt_{2} :Nat→k. t_{1}
ifez(succ t) = λk:Kind. λt_{1} :k. λt_{2} :Nat→k. t_{2} t

le : Nat→Nat→Bool

le(zero) = λt:Nat. true
le(succ t) = λt′:Nat. ifez t′ Bool false (le t)

lt : Nat→Nat→Bool

lt = λt:Nat. le (succ t)

Cond : Bool→Kind→Kind→Kind

Cond(true) = λk_{1} :Kind. λk_{2} :Kind. k_{1}
Cond(false) = λk_{1} :Kind. λk_{2} :Kind. k_{2}

Figure 2: Examples of inductive definitions

• Kind schemas Πk : u_{1}. u_{2} and u_{1} → u_{2} are used to typecheck the kind-level function λk : u. κ and its application form κ_{1} κ_{2}. We use it to write higher-order predicates and logic connectives. For example, the logical negation operator can be written as follows:

Not : Kind → Kind = λk:Kind. (k →False)

The consistency of TL implies that a proposition and its negation cannot be both inhabited—otherwise applying the proof of the second to that of the first would yield a proof of False.

TL also provides a general mechanism of inductive definitions [35]. The term Ind(k : Kind){κ⃗} introduces an inductive kind k containing a list of constructors whose kinds are specified by κ⃗. Here k must only occur “positively” inside each κ_{i} (see Appendix D for the formal definition of positivity). The term Ctor (i, κ) refers to the i-th constructor in an inductive kind κ. For presentation, we will use a more friendly syntax in the rest of this paper. An inductive kind I = Ind(k:Kind){κ⃗} will be written as:

Inductive I : Kind := c_{1} : [I/k]κ_{1} ; | c_{2} : [I/k]κ_{2} ; ⋮ ; | c_{n} : [I/k]κ_{n}

We give an explicit name c_{i} to each constructor, so c_{i} is just an abbreviation of Ctor (i, I). For simplicity, the current version of TL does not include parameterized inductive kinds, but supporting them is quite straightforward [41, 35].

TL provides two iterators to support primitive recursion on inductive kinds. The small elimination Elim[κ′, κ](τ′){τ⃗} takes a type term τ′ of inductive kind κ′, performs the iterative operation specified by τ⃗ (which contains a branch for each constructor of κ′), and returns a type term of kind κ[τ′] as the result. The large elimination Elim[κ′, u](τ){κ⃗} takes a type term τ of inductive kind κ′, performs the iterative operation specified by κ⃗, and returns a kind

(sort) s ::= Kind | Kscm | Ext
(var) X ::= z | k | t
(ptm) A, B ::= s | X | λX:A. B | A B | ΠX:A. B | Ind(X:Kind){A⃗} | Ctor (i, A) | Elim[A′, B′](A){B⃗}

Figure 3: Syntax of the type language TL

term of kind schema u as the result. These iterators generalize the Typerec operator used in intensional type analysis [22, 14, 39].

Figure 2 gives a few examples of inductive definitions including the inductive kinds Bool and Nat and several type-level functions which we will use in Section 4. The small elimination for Nat takes the following form Elim[Nat, κ](τ′){τ_{1}; τ_{2}}. Here, κ is a dependent kind with kind schema Nat → Kind; τ′ is the argument which has kind Nat. The term in the zero branch, τ_{1}, has kind κ[τ′]. The term in the succ branch, τ_{2}, has kind Nat → κ[τ′] → κ[τ′]. TL uses the ι-reduction to perform the iterator operation. For example, the two ι-reduction rules for Nat work as follows:

Elim[Nat, κ](zero){τ_{1}; τ_{2}} ⇝_{ι} τ_{1}
Elim[Nat, κ](succ τ){τ_{1}; τ_{2}} ⇝_{ι} τ_{2} τ (Elim[Nat, κ](τ){τ_{1}; τ_{2}})

The general ι-reduction rule is defined formally in Appendix D. In our examples, we take the liberty of using the pattern-matching syntax (as in ML) to express the iterator operations, but they can be easily converted back to the Elim form.

In Figure 2, plus is a function which calculates the sum of two natural numbers. The function ifez behaves like a switch statement: if its argument is zero, it returns a function that selects the first branch; otherwise, the result takes the second branch and applies it to the predecessor of the argument. The function le evaluates to true if its first argument is less than or equal to the second. The function lt performs the less-than comparison.

The definition of function Cond, which implements a conditional with result at the kind level, uses large elimination on Bool. It has the form Elim[Bool, u](τ){κ_{1}; κ_{2}}, where τ is of kind Bool; both the true and false branches (κ_{1} and κ_{2}) have kind schema u.

Formalization We want to give a formal semantics to TL and then reason about its meta-theoretical properties. But the five Π constructs have many redundancies, so in the rest of this paper, we will model TL as a pure type system (PTS) [4] extended with inductive definitions. Intuitively, instead of having a separate syntactical category for each level, we collapse all kind schemas u, kind terms κ, type terms τ, and the external constant Kscm into a single set of pseudoterms (ptm), denoted as A or B. Similar constructs can now share typing rules and reduction relations.

Figure 3 gives the syntax of TL, written in PTS style. There is now only one Π construct (ΠX : A. B), one λ-abstraction (λX : A. B), and one application form (A B); two iterators for inductive definitions are also merged into one (Elim[A′, B′](A){B⃗}). We use X and Y to represent generic variables, but we will still use t, k, and z if the class of a variable is clear from the context.

TL has the following PTS specification which we will use to derive its typing rules:

S = Kind, Kscm, Ext
A = Kind:Kscm, Kscm:Ext
R = (Kind, Kind), (Kscm, Kind), (Ext, Kind)

(Kind, Kscm), (Kscm, Kscm)

Here S contains the set of sorts used to denote universes. We have to add the constant Ext to support quantification over Kscm. Our names for the sorts reflect the fact we lifted everything one level up; they are related to other systems via the following table:

Systems  Notations
TL  Kind  Kscm  Ext
Werner [41]  Set  Type  Ext
Coq/Cic [25] Set,Prop Type(0) Type(1)
Barendregt [4]  ∗  □  △

The axioms in the set A denote the relationship between different sorts; an axiom “s_{1} : s_{2}” means that s_{2} classifies s_{1}. The rules in the set R are used to define well-formed Π constructs, from which we can deduce the set of well-formed λ-definitions and applications. For example, the five rules for TL can be related to the five Π constructs through the following table:

PTS rules\ptm ΠX:A. B  λX:A. B A B
(Kind, Kind)  Πt:κ_{1}. κ_{2}  λt:κ. τ  τ_{1} τ_{2}
(Kscm, Kind)  Πk:u. κ  λk:u. τ  τ[κ]
(Ext, Kind) Πz:Kscm. κ λz:Kscm. τ τ[u]
(Kind, Kscm)  Πt:κ. u  λt:κ_{1}. κ_{2} κ[τ]
(Kscm, Kscm) Πk:u_{1}. u_{2}  λk:u. κ  κ κ′

We define a context Δ as a list of bindings from variables to pseudoterms:

(ctxt) Δ ::= · | Δ, X:A

The typing judgment for the PTS-style TL now takes the form Δ ⊢ A : A′ meaning that within context Δ, the pseudoterm A is wellformed and has A′ as its classifier. We can now write a single typing rule for all the Π constructs:

\begin{aligned}Δ ⊢ A : s_{1} & Δ, X:A ⊢ B : s_{2} & (s_{1}, s_{2}) ∈ R \\ & Δ ⊢ ΠX:A. B : s_{2} \end{aligned}  (prod)

Take the rule (Kind, Kscm) as an example. To build a well-formed term ΠX : A. B, which will be a kind schema (because s_{2} is Kscm), we need to show that A is a well-formed kind and B is a well-formed kind schema assuming X has kind A. We can also share the typing rules for all the λ-definitions and applications:

{Δ, X:A ⊢ B : B′  Δ ⊢ ΠX:A. B′ : s \atop Δ ⊢ λX:A. B : ΠX:A. B′}  (fun)

\begin{matrix}Δ ⊢ A : ΠX:B′. A′ & Δ ⊢ B : B′ \\ Δ ⊢ A B : [B/X]A′ \end{matrix}  (app)

The reduction relations can also be shared. TL supports the standard β- and η-reductions (denoted as ⇝_{β} and ⇝_{η}) plus the previously mentioned ι-reduction (denoted as ⇝_{ι}) on inductive objects (see Appendix D). We use ⊳_{β}, ⊳_{η}, and ⊳_{ι} to denote the relations that correspond to the rewriting of subterms using the relations ⇝_{β}, ⇝_{η}, and ⇝_{ι} respectively. We use ⇝ and ⊳ for the unions of the above relations. We also write =_{βηι} for the reflexive-symmetric-transitive closure of ⊳.

The complete typing rules for TL and the definitions of all the reduction relations are given in Appendix D. Following Werner [41] and Geuvers [17], we have shown that TL satisfies all the key meta-theoretic properties including subject reduction, strong normalization, Church-Rosser (and confluence), and consistency of the underlying logic. The detailed proofs for these properties are given in Appendix D.

4 The Computation Language λ_{H}

The language of computations λ_{H} for our high-level certified intermediate format uses proofs, constructed in the type language, to

(exp) e ::= x | \overline{n} | tt | ff | f | fix x:A. f | e e′ | e[A] | ⟨X =A, e:A′⟩ | open e as ⟨X, x⟩ in e′ | ⟨e_{0}, … e_{n−1}⟩ | sel[A](e, e′) | e aop e′ | e cop e′ | if[A, A′](e, X_{1}. e_{1}, X_{2}. e_{2})

where n ∈ ℕ
(fun) f ::= λx:A. e | ΛX:A. f
(arith) aop ::= + | …
(cmp) cop ::= < | …

Figure 4: Syntax of the computation language λ_{H}.

verify propositions which ensure the runtime safety of the program. Furthermore, in comparison with other higher-order typed calculi, the types assigned to programs can be more refined, since program invariants expressible in higher-order predicate logic can be represented in our type language. These more precise types serve as more complete specifications of the behavior of program components, and thus allow the static verification of more programs.

One approach to presenting a language of computations is to encode its syntax and semantics in a proof system, with the benefit of obtaining machine-checkable proofs of its properties, e.g. type safety. This appears to be even more promising for a system with a type language like Cic, which is more expressive than higherorder predicate logic: The Cic proofs of some program properties, embedded as type terms in the program, may not be easily representable in meta-logical terms, thus it may be simpler to perform all the reasoning in Cic. However our exposition of the language TL is focused on its use as a type language, and consequently it does not include all features of Cic. We therefore leave this possibility for future work, and give a standard meta-logical presentation instead; we address some of the issues related to adequacy in our discussion of type safety.

In this section we often use the unqualified “term” to refer to a computation term (expression) e, with syntax defined in Figure 4. Most of the constructs are borrowed from standard higher-order typed calculi. To simplify the exposition we only consider constants representing natural numbers (\overline{n} is the value representing n ∈ ℕ) and boolean values (tt and ff). The term-level abstraction and application are standard; type abstractions and fixed points are restricted to function values, with the call-by-value semantics in mind and to simplify the CPS and closure conversions. The type variable bound by a type abstraction, as well as the one bound by the open construct for packages of existential type, can have either a kind or a kind schema. Dually, the type argument in a type application, and the witness type term A in the package construction ⟨X =A, e:A′⟩ can be either a type term or a kind term.

The constructs implementing tuple operations, arithmetic, and comparisons have nonstandard static semantics, on which we focus in section 4.1, but their runtime behavior is standard. The branching construct is parameterized at the type level with a proposition (which is dependent on the value of the test term) and its proof; the proof is passed to the executed branch.

Dynamic semantics We present a small step call-by-value operational semantics for λ_{H} in the style of Wright and Felleisen [42]. The values are defined as

v ::= \overline{n} | tt | ff | f | fix x:A. f | ⟨X =A, v:A′⟩ | ⟨v_{0}, … v_{n−1}⟩

The reduction relation ↪ is specified by the rules

(λx:A. e) v ↪ [v/x]e  (R-β)

(ΛX:B. f)[A] ↪ [A/X]f  (R-ty-β)
sel[A](⟨v_{0}, … v_{n−1}⟩, \overline{m}) ↪ v_{m}  (m < n)  (R-sel)

open ⟨X′ =A, v:A′⟩ as ⟨X, x⟩ in e

↪ [v/x][A/X]e (R-open)

(fix x:A. f) v ↪ ([fix x:A. f/x]f) v  (R-fix)
(fix x:A. f)[A′] ↪ ([fix x:A. f/x]f)[A′]  (R-tyfix)
\overline{m} +\overline{n} ↪ \overline{m + n}  (R-add)
\overline{m} <\overline{n} ↪ tt  (m < n)  (R-lt-T)
\overline{m} <\overline{n} ↪ ff  (m ≥ n)  (R-lt-F)
if[B, A](tt, X_{1}. e_{1}, X_{2}. e_{2}) ↪ [A/X_{1}]e_{1}  (R-if-T)
if[B, A](ff, X_{1}. e_{1}, X_{2}. e_{2}) ↪ [A/X_{2}]e_{2}  (R-if-F)

An evaluation context E encodes the call-by-value discipline:

E ::= • | E e | v E | E[A] | ⟨X =A, E:A′⟩ | open E as ⟨X, x⟩ in e | open v as ⟨X, x⟩ in E | ⟨v_{0}, … v_{i}, E, e_{i+2}, …, e_{n−1}⟩ | sel[A](E, e) | sel[A](v, E) | E aop e | v aop E | E cop e | v cop E | if[A, A′](E, X_{1}. e_{1}, X_{2}. e_{2})

The notation E{e} stands for the term obtained by replacing the hole • in E by e. The single step computation ↦ relates E{e} to E{e′} when e ↪ e′, and ↦^{∗} is its reflexive transitive closure.

As shown the semantics is standard except for some additional passing of type terms in R-sel and R-if-T/F. However an inspection of the rules shows that types are irrelevant for the evaluation, hence a type-erasure semantics, in which all type-related operations and parameters are erased, would be entirely standard.

4.1 Static semantics

The static semantics of λ_{H} shows the benefits of using a type language as expressive as TL. We can now define the type constructors of λ_{H} as constructors of an inductive kind Ω, instead of having them built into λ_{H}. As we will show in Section 5, this property is crucial for the conversion to CPS, since it makes possible transforming direct-style types to CPS types within the type language.

Inductive Ω : Kind := snat : Nat→Ω | sbool : Bool→Ω | → → : Ω→Ω→Ω | tup : Nat→(Nat→Ω)→Ω | ∀ ∀_{Kind} : Πk:Kind. (k →Ω)→Ω | ∃∃_{Kind} : Πk:Kind. (k →Ω)→Ω | ∀ ∀_{Kscm} : Πz:Kscm. (z →Ω)→Ω | ∃∃_{Kscm} : Πz:Kscm. (z →Ω)→Ω

Informally, all well-formed computations have types of kind Ω, including singleton types of natural numbers snat A and boolean values sbool B, as well as function, tuple, polymorphic and existential types. To improve readability we also define the syntactic sugar

A → B ≡ → → A B
\begin{matrix}∀_{s}X:A. B \\ ∃_{s}X:A. B \end{matrix} \begin{matrix}≡ \\ ≡ \end{matrix} \begin{matrix}∀ ∀_{s} A (λX:A. B) \\ ∃∃_{s} A (λX:A. B) \end{matrix}\} where s ∈ \{Kind, Kscm\}

and often drop the sort s when s = Kind; e.g. the type void, containing no values, is defined as ∀t:Ω. t ≡ ∀ ∀_{Kind} Ω (λt:Ω. t).

Using this syntactic sugar we can give a familiar look to many of the formation rules for λ_{H} expressions and functional values. Figure 5 contains the inference rules for deriving judgments of the form Δ; Γ ⊢ e : A, which assign type A to the expression e in a context Δ and a type environment Γ defined by

(type env) Γ ::= · | Γ, x:A

We introduce some of the notation used in these rules in the course of the discussion.

Rules E-nat, E-true, and E-false assign singleton types to numeric and boolean constants. For instance the constant \overline{1} has type succ zero in any valid environment. In rule E-nat we use the metafunction ˆ · to map natural numbers n ∈ ℕ to their representations as type terms. It is defined inductively by ˆ0 = zero and { \atop n+1} = succ n̂, so Δ ⊢ n̂ : Nat holds for all valid Δ and n ∈ ℕ.

Singleton types play a central role in reflecting properties of values in the type language, where we can reason about them constructively. For instance rules E-add and E-lt use respectively the type terms plus and lt (defined in Section 3) to reflect the semantics of the term operations into the type level via singleton types.

However, if we could only assign singleton types to computation terms, in a decidable type system we would only be able to typecheck terminating programs. We regain expressiveness of the computation language using existential types to hide some of the too detailed type information. Thus for example one can define the usual types of all natural numbers and boolean values as

nat : Ω = ∃t:Nat. snat t
bool : Ω = ∃t:Bool. sbool t

For any term e with singleton type snat A the package ⟨t = A, e: snat t⟩ has type nat. Since in a type-erasure semantics of λ_{H} all types and operations on them are erased, there is no runtime overhead for the packaging. For each n ∈ ℕ there is a value of this type denoted by ˆ \overline{n} ≡ ⟨t = n̂, \overline{n} : snat t⟩. Operations on terms of type nat are derived from operations on terms of singleton types of the form snat A; for example an addition function of type nat → nat → nat is defined as the expression

add = λx_{1} :nat. λx_{2} :nat. open x_{1} as ⟨t_{1}, x′_{1}⟩ in open x_{2} as ⟨t_{2}, x′_{2}⟩ in ⟨t=plus t_{1} t_{2}, x′_{1} + x′_{2} :snat t⟩

Rule E-tup assigns to a tuple a type of the form tup A B, in which the tup constructor is applied to a type A representing the tuple size, and a function B mapping offsets to the types of the tuple components. This function is defined in terms of operations on lists of types:

Inductive List : Kind := nil : List | cons : Ω→List→List

nth : List→Nat→Ω

nth nil  = λt:Nat. void
nth (cons t_{1} t_{2}) = λt:Nat. ifez t Ω t_{1} (nth t_{2})

Thus nth L n̂ reduces to the n-th element of the list L when n is less than the length of L, and to void otherwise. We also use the infix form A::A′ ≡ cons A A′. The type of pairs is derived: A × A′ ≡ tup ˆ2 (nth (A::A′::nil)). Thus for instance ·;· ⊢ ⟨\overline{42}, \overline{7}⟩ : snat ˆ42 × snat ˆ7 is a valid judgment.

The rules for selection and testing for the less-than relation (the only comparison we discuss for brevity) refer to the kind term LT with kind schema Nat → Nat → Kind. Intuitively, LT represents a binary relation on kind Nat, so LT m̂ n̂ is the kind of type terms representing proofs of m < n. LT can be thought of as the parameterized inductive kind of proofs constructed from instances of the axioms ∀n ∈ ℕ. 0 < n+1 and ∀m, n ∈ ℕ. m < n ⊃ m+1 < n+1:

Inductive LT : Nat→Nat→Kind

:= ltzs : Πt:Nat. LT zero (succ t)
| ltss : Πt:Nat. Πt′:Nat. LT t t′ →LT (succ t) (succ t′)

To simplify the presentation of our type language, we allowed inductive kinds of kind scheme Kind only. Thus to stay within the scope of this paper we actually use a Church encoding of LT (defined later); this is sufficient since proof objects are never analyzed in λ_{H}, so the full power of elimination is not necessary for LT.

In the component selection construct sel[A](e, e′) the type A represents a proof that the value of the subscript e′ is less than the size of the tuple e. In rule E-sel this condition is expressed as an application of the type term LT. Due to the consistency of the logic represented in the type language, only the existence and not the structure of the proof object A is important. Since its existence is ensured statically in a well-formed expression, A would be eliminated in a type-erasure semantics.

The branching construct if[B, A](e, X_{1}. e_{1}, X_{2}. e_{2}) takes a type term A representing a proof of the proposition encoded as either B true or B false, depending on the value of e. The proof is passed to the appropriate branch in its bound type variable (X_{1} or X_{2}). The correspondence between the value of e and the kind of A is again established through a singleton type. Note that unlike Xi and Harper [43] we allow imprecise information flow into the branches by not restricting B false to be the negation of B true. In particular this makes possible the encoding of the usual oblivious (in proof-passing sense) if using B = λt:Bool. True.

4.2 Example: bound check elimination

A simple example of the generation, propagation, and use of proofs in λ_{H} is a function which computes the sum of the components of any vector of naturals. Let us first introduce some auxiliary types and functions. The type assigned to a homogeneous tuple (vector) of n terms of type A is βηι-convertible to the form vec n̂ A for

vec : Nat→Ω→Ω

vec = λt:Nat. λt′:Ω. tup t (nth (repeat t t′))

where repeat : Nat→Ω→List

repeat zero = λt′:Ω. nil
repeat (succ t) = λt′:Ω. t′::(repeat t) t′

Then we can define a term which sums the elements of a vector with a given length as follows:

sumVec : ∀t:Nat. snat t → vec t nat → nat
≡ Λt:Nat. λn:snat t. λv:vec t nat. (fix loop:nat → nat → nat. λi:nat. λsum:nat. open i as ⟨t′, i′⟩ in if[LTOrTrue t′ t, ltPrf t′ t] (i′ < n, t_{1}. loop (add i ˆ \overline{1}) (add sum (sel[t_{1}](v, i′))), t_{2} . sum)) ˆ \overline{0}ˆ \overline{0}

where LTOrTrue : Nat→Nat→Bool→Kind

LTOrTrue = λt_{1} :Nat. λt_{2} :Nat. λt:Bool. Cond t (LTt_{1} t_{2})True

and ltPrf of kind Πt′ : Nat. Πt : Nat. LTOrTrue t′ t (lt t′ t) is a type term defined later.

The comparison i′ < n, used in this example as a loop termination test, checks whether the index i′ is smaller than the vector size n. If it is, the adequacy of the type term lt with respect to the lessthan relation ensures that the type term ltPrf t′ t represents a proof of the corresponding proposition at the type level, namely LT t′ t. This proof is then bound to t_{1} in the first branch of the if, and the sel construct uses it to verify that the i′-th element of v exists, thus avoiding a second test. The type safety of λ_{H} (Theorem 1) guaran-Δ ⊢ Kind : Kscm

Δ ⊢ · ok (TE-mt)

Δ ⊢ Γ ok Δ ⊢ A : Ω Δ ⊢ Γ, x:A ok (TE-ext)

{Δ ⊢ Γ ok \atop Δ; Γ ⊢ x : Γ(x)} (E-var)

Δ ⊢ Γ ok Δ; Γ ⊢ \overline{n} : snat n̂ (E-nat)

Δ ⊢ Γ ok

Δ; Γ ⊢ tt : sbool true

(E-true)

Δ ⊢ Γ ok

Δ; Γ ⊢ ff : sbool false

(E-false)

Δ ⊢ A : Ω Δ; Γ, x:A ⊢ f : A Δ; Γ ⊢ fix x:A. f : A

(E-fix)

{Δ ⊢ A : Ω  Δ; Γ, x:A ⊢ e : A′ \atop Δ; Γ ⊢ λx:A. e : A → A′}  (E-fun)

{Δ; Γ ⊢ e_{1} : A → A′  Δ; Γ ⊢ e_{2} : A \atop Δ; Γ ⊢ e_{1} e_{2} : A′}  (E-app)

{Δ ⊢ B : s  Δ, X:B; Γ ⊢ f : A \atop Δ; Γ ⊢ ΛX:B. f : ∀_{s}X:B. A} (\begin{matrix}X ∉ Δ \\ s ≠ Ext \end{matrix}) (E-tfun)

{Δ; Γ ⊢ e : ∀_{s}X:B. A′  Δ ⊢ A : B \atop Δ; Γ ⊢ e[A] : [A/X]A′} (s ≠ Ext) (E-tapp)

\begin{matrix}Δ ⊢ A : B  Δ ⊢ B : s \\ Δ; Γ ⊢ e : [A/X]A′ \end{matrix} ; Δ; Γ ⊢ ⟨X =A, e:A′⟩ : ∃_{s}X:B. A′ (s ≠ Ext) (E-pack)

\begin{matrix}Δ; Γ ⊢ e : ∃_{s}X′:B. A Δ ⊢ A′ : Ω \\ Δ, X:B; Γ, x:[X/X′]A ⊢ e′ : A′ \end{matrix} Δ; Γ ⊢ open e as ⟨X, x⟩ in e′ : A′ (\begin{matrix}X ∉ Δ \\ s ≠ Ext \end{matrix}) (E-open)

Δ; Γ ⊢ e : snat A Δ; Γ ⊢ e′ : snat A′ Δ; Γ ⊢ e + e′ : snat (plus A A′)

(E-add)

Δ; Γ ⊢ e : snat A Δ; Γ ⊢ e′ : snat A′ Δ; Γ ⊢ e < e′ : sbool (lt A A′)

(E-lt)

for all i < n Δ; Γ ⊢ e_{i} : A_{i}

Δ; Γ ⊢ ⟨e_{0}, … e_{n−1}⟩ : tup n̂ (nth (A_{0}:: …::A_{n−1}::nil))

(E-tup)

Δ; Γ ⊢ e : tup A′′ B Δ; Γ ⊢ e′ : snat A′ Δ ⊢ A : LT A′ A′′

Δ; Γ ⊢ sel[A](e, e′) : B A′

(E-sel)

Δ ⊢ B : Bool→Kind Δ; Γ ⊢ e : sbool A′′
Δ ⊢ A : B A′′  Δ, X_{1} :B true; Γ ⊢ e_{1} : A′
Δ ⊢ A′ : Ω  Δ, X_{2} :B false; Γ ⊢ e_{2} : A′
Δ; Γ ⊢ if[B, A](e, X_{1}. e_{1}, X_{2}. e_{2}) : A′

(E-if)

{Δ; Γ ⊢ e : A  A =_{βηι} A′  Δ ⊢ A′ : Ω \atop Δ; Γ ⊢ e : A′} (E-conv)

Figure 5: Static semantics of the computation language λ_{H}.

tees that implementations of sel need not check the subscript at runtime. Since the proof t_{2} is ignored in the “else” branch, ltPrf t′ t is defined to reduce to the trivial proof of True when the value of i′ is not less than that of n.

The usual vector type, which keeps the length packaged with the content, is

vector : Ω→Ω = λt:Ω. ∃t′:Nat. snat t′ × vec t′ t.

Now we can write a wrapper function for sumVec with the standard type vector nat → nat; we leave the details to the reader.

4.3 Type safety

The type safety of λ_{H} is a corollary of its properties of progress and subject reduction. A pivoting element in proving progress (Lemma 4 in Appendix A) is the connection between the existence of a proof (type) term of kind LT m̂ n̂, provided by rule E-sel, and the existence of a (meta-logical) proof of the side condition m<n, required by rule R-sel. Similarly, subject reduction (Lemma 5 in Appendix A) in the cases of R-add and R-lt-T/F relies on the adequate representation of addition and comparison by plus and lt.

Lemma 1 (Adequacy of the TL representation of arithmetic) 1. For all m, n ∈ ℕ, plus m̂ n̂ =_{βηι} { \atop m+n}.

2. For all m, n ∈ ℕ, lt m̂ n̂ =_{βηι} true if and only if m < n.

3. For all m, n ∈ ℕ, m < n if and only if there exists a type A such that · ⊢ A : LT m̂ n̂.

Proof sketch (3) For the forward direction it suffices to observe that the structure of the meta-logical proof of m < n (in terms of the above axioms of ordering) can be directly reflected in a type term of kind LT m̂ n̂. The inverse direction is shown by examining the structure of closed type terms of this kind in normal form. □

Theorem 1 (Safety of λ_{H}) If ·;·⊢ e : A, then either e ↦^{∗} v and ·;·⊢ v : A, or e diverges (i.e., for each e′, if e ↦^{∗} e′, then there exists e′′ such that e′ ↦ e′′). Proof sketch Follows from Lemmas 4 and 5 (Appendix A). □

Since Cic and TL are more expressive than higher-order predicate logic, adequacy of the representations of meta-proofs does not hold in general; in particular, the ability to eliminate inductive kinds in TL allows analysis of proof derivations to be used in proof construction, a technique not employed in standard meta-reasoning. This issue does not arise for first-order proof representations like LT (where no constructors have parameters of a function kind), and we do not expect it to be a concern in practice. In cases when it does arise, it could be resolved by using the underlying consistent logic of Cic instead of the meta-logic; for instance in our presentation the question of adequacy is raised because the operational semantics of λ_{H} is defined in meta-logical terms, but this question would be moot if λ_{H} and its semantics were defined as Cic terms. To eliminate the interaction with the meta-logic, this approach should be applied all the way down to the hardware specification (as done in some PCC system [3]); we plan to pursue this in the future.

4.4 An example of proof generation

Here we show the type term ltPrf which generates the proof of the proposition LTOrTrue t′ t (lt t′ t), needed in the sumVec example. We first present a Church encoding of the kind term LT and its “constructors” ltzs and ltss.

LT : Nat→Nat→Kind

LT = λt:Nat. λt′:Nat.

ΠR:Nat→Nat→Kind. (Πt:Nat. R zero (succ t))→ (Πt:Nat. Πt′:Nat. R t t′ →R (succ t) (succ t′))→ R t t′

ltzs : Πt:Nat. LT zero (succ t)

ltzs = λt:Nat. λR:Nat→Nat→Kind.

λz:(Πt:Nat. R zero (succ t)). λs:(Πt:Nat. Πt′:Nat. R t t′ →R (succ t) (succ t′)). z t

ltss : Πt:Nat. Πt′:Nat. LT t t′ →LT (succ t) (succ t′)

ltss = λt:Nat. λt′:Nat. λp:LT t t′. λR:Nat→Nat→Kind.

λz:(Πt:Nat. R zero (succ t)). λs:(Πt:Nat. Πt′:Nat. R t t′ →R (succ t) (succ t′)). s t t′ (p R z s)

Next we define dependent conditionals on kinds Nat and Bool.

dep ifez : Πt:Nat. Πk:Nat→Kind. k zero→(Πt′:Nat. k (succ t′))→k t

dep ifez zero = λk:Nat→Kind. λt_{1} :k zero.

λt_{2} :(Πt′:Nat. k (succ t′)). t_{1}

dep ifez (succ t) = λk:Nat→Kind. λt_{1} :k zero.

λt_{2} :(Πt′:Nat. k (succ t′)). t_{2} t

dep if : Πt:Bool. Πk:Bool→Kind. k true→k false→k t

dep if true = λk:Bool→Kind. λt_{1} :k true. λt_{2} :k false. t_{1}
dep if false = λk:Bool→Kind. λt_{1} :k true. λt_{2} :k false. t_{2}

Finally, some abbreviations, and then the proof generator itself.

LTcond : Nat→Nat→Kind

LTcond = λt′:Nat. λt:Nat. LTOrTrue t′ t (lt t′ t)

LTimp : Nat→Nat→Bool→Kind

LTimp = λt′:Nat. λt:Nat. λt′′:Bool.

LTOrTrue t′ t t′′ →LTOrTrue (succ t′) (succ t) t′′

ltPrf : Πt′:Nat. Πt:Nat. LTcond t′ t

ltPrf = λt′:Nat.

Elim[Nat, λt′_{1} :Nat. Πt_{1} :Nat. LTcond t′_{1} t_{1}](t′){ λt_{1} :Nat. dep ifez t_{1} (LTcond zero) id ltzs; λt′_{1} :Nat. λt_{P} :(Πt_{1} :Nat. LTcond t′_{1} t_{1}). λt_{1} :Nat.

dep ifez t_{1} (LTcond (succ t′_{1})) id (λt_{1} :Nat. dep if (lt t′_{1} t_{1}) (LTimp t′_{1} t_{1}) (ltss t′_{1} t_{1}) (id True) (t_{P} t_{1}))}

5 CPS Conversion

In this section we show how to perform CPS conversion on λ_{H} while still preserving proofs represented in the type system. This stage transforms all unconditional control transfers, including function invocation and return, to function calls and gives explicit names to all intermediate computations. The basics of our approach, i.e. the target language and the transformation of types, are shown in this section. The static semantics of the target language and the transformation of terms are given in Appendix B.

We call the target calculus for this phase λ_{K}, with syntax:

(val) v ::={x | \overline{n} | tt | ff | ⟨X =A, v:A′⟩ | ⟨v_{0}, … v_{n−1}⟩ \atop | fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e}

(exp) e ::= v[A_{1}, … A_{n}](v′) | let x = v in e | let ⟨X, x⟩ = open v in e | let x = sel[A](v, v′) in e | let x = v aop v′ in e | let x = v cop v′ in e | if[A, A′](v, X_{1}. e_{1}, X_{2}. e_{2})

Expressions in λ_{K} consist of a series of let bindings followed by a function application or a conditional branch. There is only one abstraction mechanism, fix, which combines type and value abstraction. Multiple arguments may be passed by packing them in a tuple.

λ_{K} shares the TL type language with λ_{H}. The types for λ_{K} all have kind Ω_{K} which, as in λ_{H}, is an inductive kind defined in TL. The Ω_{K} kind has all the constructors of Ω plus one more (func). Since functions in CPS do not return values, the function type constructor of Ω_{K} has a different kind:

→ → : Ω_{K} →Ω_{K}

We use the more conventional syntax A →⊥ for → → A. The new constructor func forms the types of function values:

func : Ω_{K} →Ω_{K}

Every function value is implicitly associated with a closure environment (for all the free variables), so the func constructor is useful in the closure-conversion phase (see Section 6).

Typed CPS conversion involves translating both types and computation terms. Existing algorithms [21, 28] require traversing and transforming every term in the type language (which would include all the proofs in our setting). This is impractical because proofs are large in size, and transforming them can alter their meanings and break the sharing among different intermediate languages.

To see the actual problem, let us convert the λ_{H} expression ⟨X = A, e: B⟩ to CPS, assuming that it has type ∃X : A′. B. We use K_{typ} to denote the meta-level translation function for the type language and K_{exp} for the computation language. Under existing algorithms, the translation also transforms the witness A:

K_{exp}[[⟨X =A, e:B⟩]] =
λk:K_{typ}[[∃X:A′. B]].
K_{exp}[[e]] (λx:K_{typ}[[[A/X]B]].
k ⟨X =K_{typ}[[A]], x:K_{typ}[[B]]⟩)

Here we CPS-convert e and apply it to a continuation, which puts the result of its evaluation in a package and hands it to the return continuation k. With proper definition of K_{typ} and assuming that K_{typ}[[X]] = X on all variables X, we can show that the two types K_{typ}[[[A/X]B]] and [K_{typ}[[A]]/X](K_{typ}[[B]]) are equivalent (under =_{βηι}). Thus the translation preserves typing.

But we do not want to touch the witness A, so the translation function should be defined as follows:

K_{exp}[[⟨X =A, e:B⟩]] =
λk:K_{typ}[[∃X:A′. B]].
K_{exp}[[e]] (λx:K_{typ}[[[A/X]B]].
k ⟨X =A, x:K_{typ}[[B]]⟩)

To preserve typing, we have to make sure that the two types K_{typ}[[[A/X]B]] and [A/X](K_{typ}[[B]]) are equivalent. This seems impossible to achieve if K_{typ} is defined at the meta level.

Our solution is to internalize the definition of K_{typ} in our type language. We replace K_{typ} by a type function K of kind Ω → Ω_{K}. For readability, we use the pattern-matching syntax, but it can be easily coded using the Elim construct.

K (snat t)  = snat t
K (sbool t) = sbool t
K (t_{1} → t_{2}) = func ((K(t_{1}) × K_{c}(t_{2}))→⊥)
K (tup t_{1} t_{2}) = tup t_{1} (λt:Nat. K(t_{2} t))
K (∀ ∀_{Kind} k t) = func (∀ ∀_{Kind} k (λt_{1} :k. K_{c}(t t_{1})→⊥))
K (∃∃_{Kind} k t) = ∃∃_{Kind} k (λt_{1} :k. K(t t_{1}))
K (∀ ∀_{Kscm} z t) = func (∀ ∀_{Kscm} z (λk:z. K_{c}(t k)→⊥))
K (∃∃_{Kscm} z t) = ∃∃_{Kscm} z (λk:z. K(t k))
K_{c}  ≡ λt:Ω. func (K(t)→⊥)

The definition of K is in the spirit of the interp function of Crary and Weirich [14]. However interp cannot be used in defining a similar CPS conversion, because its domain does not cover (nor is there an injection to it from) all types appearing in type annotations. In λ_{H} these types are in the inductive kind Ω and can be analyzed by K. We can now prove K ([A/X]B) =_{βηι} [A/X](K (B)) by first reducing B to the normal form B′. Clearly, K ([A/X]B) =_{βηι} K ([A/X]B′) and [A/X](K (B′)) =_{βηι} [A/X](K (B)). We then prove K ([A/X]B′) =_{βηι} [A/X](K (B′)) by induction over the structure of the normal form B′. The complete CPS-conversion algorithm is given in Appendix B.

6 Closure Conversion

In this section we address the issue of how to make closures explicit for all the CPS terms in λ_{K}. This stage rewrites all functions so that they contain no free variables. Any variables that appear free in a function value are packaged in an environment, which together with the closed code of the function form a closure. When a function is applied, the closed code and the environment are extracted from the closure and then the closed code is called with the environment as an additional parameter. Again, the basics of our approach are shown in this section and more details are given in Appendix C.

Our approach to closure conversion is based on Morrisett et al. [28], who adopt a type-erasure interpretation of polymorphism. We use the same idea for existential types. The language that we use for this phase is called λ_{C} with syntax:

(val) v ::={x | \overline{n} | tt | ff | fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e \atop | v[A] | ⟨v_{0}, … v_{n−1}⟩ | ⟨X =A, v:A′⟩}

(exp) e ::= v v′ | let x = v in e | let x = sel[A](v, v′) in e | let ⟨X, x⟩ = open v in e | let x = v aop v′ in e | let x = v cop v′ in e | if[B, A](v, X_{1}. e_{1}, X_{2}. e_{2})

λ_{C} is similar to λ_{K}, the main difference being that type application and value application are again separate. Type applications are values in λ_{C} reflecting the fact that they have no runtime effect in a type-erasure interpretation. We use the same kind of types Ω_{K} as in λ_{K}. We define the transformation of types as a function Cl:Ω_{K} →Ω_{K} →Ω_{K}, the second argument of which represents the type of the environment. As in CPS conversion, we write Cl as a TL function so that the closure-conversion algorithm does not have to traverse proofs represented in the type system.

Cl (snat t)  = λt′:Ω_{K}. snat t
Cl (sbool t) = λt′:Ω_{K}. sbool t
Cl (t→⊥)  = λt′:Ω_{K}. (t′ × Cl (t) ⊥)→⊥
Cl (func t)  = λt′:Ω_{K}. ∃t_{1} :Ω_{K}. (Cl (t) t_{1} × t_{1})
Cl (tup t_{1} t_{2}) = λt′:Ω_{K}. tup t_{1} (λt′′:Nat. Cl (t_{2} t′′) t′)
Cl (∀ ∀_{Kind} k t) = λt′:Ω_{K}. ∀ ∀_{Kind} k (λt_{1} :k. Cl (t t_{1}) t′)
Cl (∃∃_{Kind} k t) = λt′:Ω_{K}. ∃∃_{Kind} k (λt_{1} :k. Cl (t t_{1}) t′)
Cl (∀ ∀_{Kscm} z t) = λt′:Ω_{K}. ∀ ∀_{Kind} z (λk:z. Cl (t k) t′)
Cl (∃∃_{Kscm} z t) = λt′:Ω_{K}. ∃∃_{Kscm} z (λk:z. Cl (t k) t′)

7 Related Work

Our type language is a variant of the calculus of constructions [11] extended with inductive definitions (with both small and large elimination) [35, 41]. We omitted parameterized inductive kinds and dependent large elimination to simplify our presentation, however, all our meta-theoretic proofs carry over to a language that includes them. We support η-reduction in our language while the official Coq system does not. The proofs for the properties of TL are adapted from Geuvers [17] and Werner [41] (which in turn borrows ideas from Altenkirch [1]); the main difference is that our language has kind-schema variables and a new product formation rule (Ext, Kind) which are not in Werner’s system.

The Coq proof assistant provides support for extracting programs from proofs [35]. It separates propositions and sets into two distinct universes Prop and Set. We do not distinguish between them because we are not aiming to extract programs from our proofs, instead, we are using proofs as specifications for our computation terms.

Burstall and McKinna [7] proposed the notion of deliverables, which is essentially the same as our notion of certified binaries. They use dependent strong sums to model each deliverable and give its categorical semantics. Their work does not support programs with effects and has all the problems mentioned in Section 2.3.

Xi and Pfenning’s DML [44] is the first language that nicely combines dependent types with programs that may involve effects. Our ideas of using singleton types and lifting the level of the proof language are directly inspired by their work. Xi’s system, however, does not support arbitrary propositions and explicit proofs. It also does not define the Ω kind as an inductive definition so it is unclear how it interacts with intensional type analysis [39] and how it preserves proofs during compilation.

We have discussed the relationship between our work and those on PCC, typed assembly languages, and intensional type analysis in Section 1. Inductive definitions subsume and generalize earlier systems on intensional type analysis [22, 14, 39]; the type-analysis construct in the computation language can be eliminated using the technique proposed by Crary et al. [16].

Concurrently with our work, Crary and Vanderwaart [12] recently proposed a system called LTT which also aims at adding explicit proofs to typed intermediate languages. LTT uses Linear LF [8] as its proof language. It shares some similarities with our system in that both are using singleton types [44] to circumvent the problems of dependent types. However, since LF does not have inductive definitions and the Elim construct, it is unclear how LTT can support intensional type analysis and type-level primitive recursive functions [15]. In fact, to define Ω as an inductive kind [39], LTT would have to add proof-kind variables and proof-kind polymorphism, which could significantly complicate the meta-theory of its proof language. LTT requires different type languages for different intermediate languages; it is unclear whether it can preserve proofs during CPS and closure conversion. The power of linear reasoning in LTT is desirable for tracking ephemeral properties that hold only for certain program states; we are working on adding such support into our framework.

8 Conclusions

We presented a general framework for explicitly representing propositions and proofs in typed intermediate or assembly languages. We showed how to integrate an entire proof system into our type language and how to perform CPS and closure conversion while still preserving proofs represented in the type system. Our work is a first step toward the goal of building realistic infrastructure for certified programming and certifying compilation.

Our type system is fairly concise and simple with respect to the number of syntactic constructs, yet it is powerful enough to express all the propositions and proofs in the higher-order predicate logic (extended with induction principles). In the future, we would like to use our type system to express advanced program invariants such as those involved in low-level mutable recursive data structures.

Our type language is not designed around any particular programming language. We can use it to typecheck as many different computation languages as we like; all we need is to define the corresponding Ω kind as an inductive definition. We hope to evolve our framework into a realistic typed common intermediate format.

Acknowledgment

We would like to thank Thorsten Altenkirch, Gilles Barthe, Thierry Coquand, Antony Courtney, Karl Crary, Christopher League, Zhaohui Luo, Christine Paulin-Mohring, Stefan Monnier, Henrik Nilsson, Walid Taha, and anonymous referees for discussions and comments on an earlier version of this paper. Benjamin Werner helped us understand the intricacies in the strong-normalization proof for the core calculus of inductive constructions.

References

[1] T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, UK, 1993.

[2] A. W. Appel and E. W. Felten. Models for security policies in proofcarrying code. Technical Report CS-TR-636-01, Princeton Univ., Dept. of Computer Science, March 2001.

[3] A. W. Appel and A. P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Proc. 27th ACM Symp. on Principles of Prog. Lang., pages 243–253. ACM Press, 2000.

[4] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science (volume 2). Oxford Univ. Press, 1991.

[5] H. P. Barendregt and H. Geuvers. Proof-assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Sci. Pub. B.V., 1999.

[6] G. Barthe, J. Hatcliff, and M. Sorensen. CPS translations and applications: the cube and beyond. Higher Order and Symbolic Computation, 12(2):125–170, September 1999.

[7] R. Burstall and J. McKinna. Deliverables: an approach to program development in constructions. Technical Report ECS-LFCS-91-133, Univ. of Edinburgh, UK, 1991.

[8] I. Cervesato and F. Pfenning. A linear logical framework. In Proc. 11th IEEE Symp. on Logic in Computer Science, pages 264–275, July 1996.

[9] C. Colby, P. Lee, G. C. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for Java. In Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pages 95–107, New York, 2000. ACM Press.

[10] R. Constable. Constructive mathematics as a programming logic I: Some principles of theory. Ann. of Discrete Mathemathics, 24, 1985.

[11] T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

[12] K. Crary and J. Vanderwaart. An expressive, scalable type theory for certified code. Technical Report CMU-CS-01-113, School of Computer Science, Carnegie Mellon Univ., Pittsburg, PA, May 2001.

[13] K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th ACM Symp. on Principles of Prog. Lang., pages 262–275. ACM Press, 1999.

[14] K. Crary and S. Weirich. Flexible type analysis. In Proc. 1999 ACM SIGPLAN Int’l Conf. on Functional Prog., pages 233–248. ACM Press, Sept. 1999.

[15] K. Crary and S. Weirich. Resource bound certification. In Proc. 27th ACM Symp. on Principles of Prog. Lang., pages 184–198. ACM Press, 2000.

[16] K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proc. 1998 ACM SIGPLAN Int’l Conf. on Functional Prog., pages 301–312. ACM Press, Sept. 1998.

[17] H. Geuvers. Logics and Type Systems. PhD thesis, Catholic University of Nijmegen, The Netherlands, 1993.

[18] J.-Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures dans l’Arithmétique d’Ordre Supérieur. PhD thesis, University of Paris VII, 1972.

[19] R. Harper. The practice of type theory. Talk presented at 2000 Alan J. Perlis Symposium, Yale University, New Haven, CT, April 2000.

[20] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.

[21] R. Harper and M. Lillibridge. Explicit polymorphism and CPS conversion. In Proc. 20th ACM Symp. on Principles of Prog. Lang., pages 206–219. ACM Press, 1993.

[22] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proc. 22nd ACM Symp. on Principles of Prog. Lang., pages 130–141. ACM Press, 1995.

[23] S. Hayashi. Singleton, union and intersection types for program extraction. In A. R. Meyer, editor, Proc. International Conference on Theoretical Aspects of Computer Software, pages 701–730, 1991.

[24] W. A. Howard. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism. Academic Press, 1980.

[25] G. Huet, C. Paulin-Mohring, et al. The Coq proof assistant reference manual. Part of the Coq system version 6.3.1, May 2000.

[26] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proc. 23rd ACM Symp. on Principles of Prog. Lang., pages 271– 283. ACM Press, 1996.

[27] S. Monnier, B. Saha, and Z. Shao. Principled scavenging. In Proc. 2001 ACM Conf. on Prog. Lang. Design and Impl., pages 81–91, New York, 2001. ACM Press.

[28] G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Prog. Lang., pages 85–97. ACM Press, Jan. 1998.

[29] G. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang., pages 106–119, New York, Jan 1997. ACM Press.

[30] G. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proc. 2nd USENIX Symp. on Operating System Design and Impl., pages 229–243. USENIX Assoc., 1996.

[31] G. Necula and P. Lee. The design and implementation of a certifying compiler. In Proc. 1998 ACM Conf. on Prog. Lang. Design and Impl., pages 333–344, New York, 1998. ACM Press.

[32] G. C. Necula. Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ., Sept. 1998.

[33] B. Nordstrom, K. Petersson, and J. Smith. Programming in Martin-Löf’s type theory. Oxford University Press, 1990.

[34] C. Paulin-Mohring. Extracting F_{ω}’s programs from proofs in the Calculus of Constructions. In Proc. 16th ACM Symp. on Principles of Prog. Lang., pages 89–104, New York, Jan 1989. ACM Press.

[35] C. Paulin-Mohring. Inductive definitions in the system Coq—rules and properties. In M. Bezem and J. Groote, editors, Proc. TLCA. LNCS 664, Springer-Verlag, 1993.

[36] Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation, June 1997.

[37] Z. Shao, C. League, and S. Monnier. Implementing typed intermediate languages. In Proc. 1998 ACM SIGPLAN Int’l Conf. on Functional Prog., pages 313–323. ACM Press, 1998.

[38] M. A. Sheldon and D. K. Gifford. Static dependent types for first class modules. In 1990 ACM Conference on Lisp and Functional Programming, pages 20–29, New York, June 1990. ACM Press.

[39] V. Trifonov, B. Saha, and Z. Shao. Fully reflexive intensional type analysis. In Proc. 2000 ACM SIGPLAN Int’l Conf. on Functional Prog., pages 82–93. ACM Press, September 2000.

[40] D. Walker. A type system for expressive security policies. In Proc. 27th ACM Symp. on Principles of Prog. Lang., pages 254–267. ACM Press, 2000.

[41] B. Werner. Une Théorie des Constructions Inductives. PhD thesis, A L’Université Paris 7, Paris, France, 1994.

[42] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

[43] H. Xi and R. Harper. A dependently typed assembly language. In Proc. 2001 ACM SIGPLAN Int’l Conf. on Functional Prog., to appear.

[44] H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. 26th ACM Symp. on Principles of Prog. Lang., pages 214–227. ACM Press, 1999.

A Properties of λ_{H}

The proof of the following lemma is by induction on the structure of typing derivations.

Lemma 2 If Δ, X:B; Γ ⊢ e : A′ and Δ ⊢ A : B, then Δ; Γ ⊢ [A/X]e : [A/X]A′.

We also need a proposition guaranteeing that equivalence of constructor applications implies equivalence of their arguments; it is a corollary of the confluence of TL (Theorem 76).

Lemma 3 If Ctor (i, I) A⃗ =_{βηι} Ctor (i′, I′) A⃗′, then i = i′ and I =_{βηι} I′ and A⃗ =_{βηι} A⃗′.

Lemma 4 (Progress) If ·;·⊢ e : A, then either e is a value, or there exists e′ such that e ↦ e′.

Proof sketch By standard techniques [42] using induction on computation terms. Due to the transitivity of =_{βηι} any derivation of Δ; Γ ⊢ e : A can be converted to a standard form in which there is an application of rule E-conv at its root, whose first premise ends with an instance of a rule other than E-conv, all of whose term derivation premises are in standard form.

We omit the proofs for the cases of standard constructs and the induction on the structure of evaluation contexts. The interesting case is that of the dependently typed sel.

If e = sel[A′](v, v′), by inspection of the typing rules the derivation of ·;· ⊢ e : A in standard form must have an instance of rule E-sel in the premise of its root. Hence the subderivation for v must assign to it a tuple type, and the whole derivation has the form

{D \atop ·;·⊢ v : tup A_{2} A′′} {D′ \atop ·;·⊢ v′ : snat A_{1}} {E \atop · ⊢ A′ : LT A_{1} A_{2}}
·;·⊢ sel[A′](v, v′) : A′′ A_{1}
·;·⊢ sel[A′](v, v′) : A

where A =_{βηι} A′′ A_{1}. By inspection of the typing rules, rules other than E-conv assign to all values types which are applications of constructors of Ω. Since the derivation D is in standard form, it ends with an E-conv, in the premise of which another rule assigns v a type βηι-equivalent to tup A_{2} A′′. Then by Lemma 3 this type must be an application of tup, and again by inspection the only rule which applies is E-tup, which implies v = ⟨v_{0}, … v_{n−1}⟩, and the derivation D must have the form

{∀i < n {D_{i} \atop ·;·⊢ v_{i} : A′′_{1} î} \atop ·;·⊢ ⟨v_{0}, … v_{n−1}⟩ : tup n̂ A′′_{1}}

Also by Lemma 3 A_{2} =_{βηι} n̂. Similarly the only rule assigning to a value a type convertible to that in the conclusion of D′ is Enat, hence A_{1} =_{βηι} m̂ for some m ∈ ℕ, and v′ = \overline{m}. Then, by adequacy of LT (Lemma 1(3)), the conclusion of E implies that m < n. Hence by rule R-sel e ↦ v_{m}. □

Lemma 5 (Subject Reduction) If ·;·⊢ e : A and e ↦ e′, then ·;·⊢ e′ : A.

Proof sketch Since evaluation contexts bind no variables, it suffices to prove subject reduction for ↪ and a standard term substitution lemma. We show only some cases of redexes involving sel and if.

• The derivation for e = sel[A′](⟨v_{0}, … v_{n−1}⟩, \overline{m}) in standard form has the shape

{∀i < n {D_{i} \atop ·;·⊢ v_{i} : A′′_{1} î} \atop ·;·⊢ ⟨v⃗⟩ : tup n̂ A′′_{1}} ; ·;·⊢ ⟨v⃗⟩ : tup A_{2} A′′

{D′ \atop ·;·⊢ \overline{m} : snat m̂}

·;·⊢ \overline{m} : snat A_{1}

{E \atop · ⊢ A′ : LT A_{1} A_{2}}

·;·⊢ sel[A′](⟨v_{0}, … v_{n−1}⟩, \overline{m}) : A′′ A_{1}
·;·⊢ sel[A′](⟨v_{0}, … v_{n−1}⟩, \overline{m}) : A

where A =_{βηι} A′′ A_{1}, A′′_{1} =_{βηι} A′′, and A_{1} =_{βηι} m̂. Since e ↦ e′ only by rule R-sel, we have m < n and e′ = v_{m}, so from D_{m} and A′′_{1} m̂ =_{βηι} A′′ m̂ =_{βηι} A′′ A_{1} =_{βηι} A we obtain a derivation of ·;·⊢ e′ : A.

• In the case of if the standard derivation D of

·;·⊢ if[B, A′](tt, X_{1}. e_{1}, X_{2}. e_{2}) : A

ends with an instance of E-conv, preceded by an instance of E-if. Using the notation from Figure 5, from the premises of this rule it follows that we have a derivation E of · ⊢ A′ : B A′′, and A′′ =_{βηι} true (since rule E-true assigns sbool true to tt), hence we have · ⊢ A′ : B true by conv. By Lemma 2 from E and the derivation of X_{1} : B true; · ⊢ e_{1} : A (provided as another premise), since X_{1} is not free in A (ensured by the premise · ⊢ A : Ω) we obtain a derivation of ·;·⊢ [A′/X_{1}]e_{1} : A. □

B CPS Conversion (Details)

We start by defining a version of λ_{H} using type-annotated terms. By f̄and ē we denote the terms without annotations. Type annotations allow us to present the CPS transformation based on syntactic instead of typing derivations.

(exp) e ::= ē^{A}
ē ::= x | \overline{n} | tt | ff | f | fix x:A. f | e e′ | e[A] | ⟨X =A, e:A′⟩ | open e as ⟨X, x⟩ in e′ | ⟨e_{0}, … e_{n−1}⟩ | sel[A](e, e′) | e aop e′ | e cop e′ | if[A, A′](e, X_{1}. e_{1}, X_{2}. e_{2})

(fun) f ::= f̄^{A}
f̄::= λx:A. e | ΛX:A. f

The target language λ_{K} of the CPS conversion stage has been defined in Section 5. We use the following syntactic sugar to denote non-recursive function definitions and value applications in λ_{K}(here x′ is a fresh variable):

λx:A. e ≡ fix x′[](x:A). e
v v′ ≡ v[](v′)

ΛX_{1} :A_{1}…. ΛX_{n}:A_{n}. λx:A. e

≡ fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e

In the static semantics of λ_{K} we use two forms of judgments. As in λ_{H}, the judgment Δ; Γ ⊢_{K} v : A indicates that the value v is well formed and of type A in the type and value contexts Δ and Γ respectively. Moreover, Δ; Γ ⊢_{K} e indicates that the expression e is well formed in Δ and Γ. In both forms of judgments, we omit the subscript from ⊢_{K} when it can be deduced from the context.

The static semantics of λ_{K} is specified by the following formation rules (we omit the rules for environment formation, variables, constants, tuples, packages, and type conversion on values, which are the same as in λ_{H}):

for all i ∈ {1 … n} Δ ⊢ A_{i} : s_{i}

Δ, X_{1} :A_{1} …, X_{n}:A_{n} ⊢ A : Ω Δ, X_{1} :A_{1} …, X_{n}:A_{n}; Γ, x′:A′, x:A ⊢ e

Δ; Γ ⊢ fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e : A′ where A′ = func (∀_{s_{1}}X_{1} :A_{1}…. ∀_{s_{n}}X_{n}:A_{n}. A→⊥)

(K-fix)

for all i ∈ {1 … n} Δ ⊢ A_{i} : B_{i} Δ; Γ ⊢ v′: func(∀_{s_{1}}X_{1} :B_{1}…. ∀_{s_{n}}X_{n}:B_{n}. A→⊥)

Δ; Γ ⊢ v : [A_{1}/X_{1}] … [A_{n}/X_{n}]A

Δ; Γ ⊢ v′[A_{1}, … A_{n}](v)

(K-app)

Δ; Γ ⊢ v : A Δ; Γ, x:A ⊢ e Δ; Γ ⊢ let x = v in e

(K-val)

Δ; Γ ⊢ v : tup A′′ B Δ; Γ ⊢ v′ : snat A′ Δ ⊢ A : LT A′ A′′ Δ; Γ, x:B A′ ⊢ e

Δ; Γ ⊢ let x = sel[A](v, v′) in e

(K-sel)

\begin{matrix}Δ; Γ ⊢ v : ∃_{s}Y :B. A \\ Δ, X:B; Γ, x:[X/Y]A ⊢ e \end{matrix} Δ; Γ ⊢ let ⟨X, x⟩ = open v in e (\begin{matrix}X ∉ Δ \\ s ≠ Ext \end{matrix})  (K-open)

Δ; Γ ⊢ v : snat A Δ; Γ ⊢ v′ : snat A′ Δ; Γ, x:snat (plus A A′) ⊢ e

Δ; Γ ⊢ let x = v + v′ in e

(K-add)

Δ; Γ ⊢ v : snat A Δ; Γ ⊢ v′ : snat A′ Δ; Γ, x:sbool (lt A A′) ⊢ e

Δ; Γ ⊢ let x = v < v′ in e (K-lt)

Δ ⊢ B : Bool→Kind Δ ⊢ A : B A′
Δ; Γ ⊢ v : sbool A′

Δ, X_{1} :B true; Γ ⊢ e_{1} Δ, X_{2} :B false; Γ ⊢ e_{2}

Δ; Γ ⊢ if[B, A](v, X_{1}. e_{1}, X_{2}. e_{2})

(K-if)

Except for the rules K-fix and K-app, which must take into account the presence of func, the static semantics for λ_{K} is a natural consequence of the static semantics for λ_{H}.

The definition of the CPS transformation for computation terms of λ_{H} to computation terms of λ_{K} is given in Figure 6, where we use the abbreviations introduced in Section 5.

Proposition 2 (Type Correctness of CPS Conversion) If ·;·⊢_{H} e : A, then ·;·⊢_{K} K_{exp}[[ē^{A}]] : func (K_{c}(A)→⊥).

C Closure Conversion (Details)

The main difference in the static semantics between λ_{K} and λ_{C} is that in the latter the body of a function must not contain free type or term variables. This is formalized in the rule C-fix below. The rules C-tapp and C-app corresponding to the separate type and value application in λ_{C} are standard.

for all i < n · ⊢ A_{i} : s_{i}
·, X_{1} :A_{1} …, X_{n}:A_{n} ⊢ A : Ω

·, X_{1} :A_{1} …, X_{n}:A_{n}; ·, x′:B, x:A ⊢ e

Δ; Γ ⊢ fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e : B

where B = ∀_{s_{1}}X_{1} :A_{1}…. ∀_{s_{n}}X_{n}:A_{n}. A→⊥

(C-fix)

{Δ; Γ ⊢ v : ∀_{s}X:A′. B  Δ ⊢ A : A′ \atop Δ; Γ ⊢ v[A] : [A/X]B}  (C-tapp)

{Δ; Γ ⊢ v_{1} : A→⊥  Δ; Γ ⊢ v_{2} : A \atop Δ; Γ ⊢ v_{1} v_{2}}  (C-app)

The definition of the closure transformation for the computation terms of λ_{K} is given in Figure 7.

Proposition 3 (Type Correctness of Closure Conversion) If ·;·⊢_{K} v : A, then ·;·⊢_{C} C_{val}[[v]] : Cl (A) ⊥.

D Formalization of TL (Details)

In this appendix we prove the meta-theoretic properties of our type language TL. The proofs are based on the methods in Werner [41]. We formalize the language in Section D.1. In Section D.2 we prove subject reduction, in Section D.3 we prove the strong normalization, in Section D.4 we prove the Church-Rosser property, in Section D.5 we prove the consistency of the underlying logic.

D.1 Syntax and semantics

The syntax for the pseudoterms is:

(ctxt) Δ ::= · | Δ, X:A
(sort) s ::= Kind | Kscm | Ext
(var) X ::= z | k | t
(ptm) A, B ::= s | X | λX:A. B | A B | ΠX:A. B | Ind(X:Kind){A⃗} | Ctor (i, A) | Elim[A′, B′](A){B⃗}

K_{fval}[[(λx:A. e^{B})^{A→B}]] = λx_{arg} :K(A) × K_{c}(B). let x = sel[ltPrf ˆ0 ˆ2](x_{arg}, \overline{0}) in

let k = sel[ltPrf ˆ1 ˆ2](x_{arg}, \overline{1}) in
K_{exp}[[e^{B}]] k

K_{fval}[[(ΛX:A. f^{B})^{∀_{s}X:A. B}]] =

ΛX:A. λk:K_{c}(B). k (K_{fval}[[f^{B}]])
K_{exp}[[ē^{A}]]  = λk:K_{c}(A). k (ē)

for ē^{A} one of x^{A}, \overline{n}^{snat n̂}, tt^{sbool true}, ff^{sbool false}

K_{exp}[[f^{A}]]  = λk:K_{c}(A). k (K_{fval}[[f^{A})]]

K_{exp}[[(fix x:A. f^{A})^{A}]] = λk:K_{c}(A). k (fix x[](k:K_{c}(A)). k (K_{fval}[[f^{A}]]))

K_{exp}[[(e_{1}^{A→B} e_{2}^{A})^{B}]] = λk:K_{c}(B).

K_{exp}[[e_{1}^{A→B}]] (λx_{1} :K(A → B).

K_{exp}[[e_{2}^{A}]] (λx_{2} :K(A).
x_{1} ⟨x_{2}, k⟩))

K_{exp}[[(e^{∀ ∀_{s} A′ B}[A])^{B A}]] = λk:K_{c}(B A).

K_{exp}[[e^{∀ ∀_{s} A′ B}]] (λx:K(∀ ∀_{s} A′ B).

x[A](k))

K_{exp}[[⟨e_{0}^{A_{0}}, … e_{n−1}^{A_{n−1}}⟩^{A}]] = λk:K_{c}(A).

K_{exp}[[e_{0}^{A_{0}} ]] (λx_{0} :K(A_{0}).

⋮

K_{exp}[[e_{n−1}^{A_{n−1}} ]] (λx_{n−1} :K(A_{n−1}).

k ⟨x_{0}, … x_{n−1}⟩) …)

K_{exp}[[sel[A](e_{1}^{tup A′′ B}, e_{2}^{snat A′})^{B A′}]] = λk:K_{c}(B A′). K_{exp}[[e_{1}^{tup A′′ B}]] (λx_{1} :K(tup A′′ B). K_{exp}[[e_{2}^{snat A′}]] (λx_{2} :K(snat A′). let x′ = sel[A](x_{1}, x_{2}) in k x′))

K_{exp}[[⟨X =A, e^{[A/X]B}:B⟩^{A′}]] =

λk:K_{c}(A′). \begin{matrix}K_{exp}[[e^{[A/X]B}]] (λx:K([A/X]B). \\ k ⟨X =A, x:K(B)⟩) \end{matrix}

K_{exp}[[(open e_{1}^{∃_{s}Y:A′. B} as ⟨X, x⟩ in e_{2}^{A})^{A}]] = λk:K_{c}(A). K_{exp}[[e_{1}^{∃_{s}Y:A′. B}]] (λx_{1} :K(∃_{s}Y :A′. B). let ⟨X, x⟩ = open x_{1} in K_{exp}[[e_{2}^{A}]] k)

K_{exp}[[(e_{1}^{snat A} + e_{2}^{snat A′})^{snat (plus A A′)} ]] = λk:K_{c}(snat (plus A A′)). K_{exp}[[e_{1}^{snat A}]] (λx_{1} :K(snat A). K_{exp}[[e_{2}^{snat A′}]] (λx_{2} :K(snat A′). let x′ = x_{1} + x_{2} in k x′))

K_{exp}[[(e_{1}^{snat A} < e_{2}^{snat A′})^{sbool (lt A A′)} ]] = λk:K_{c}(sbool (lt A A′)). K_{exp}[[e_{1}^{snat A}]] (λx_{1} :K(snat A). K_{exp}[[e_{2}^{snat A′}]] (λx_{2} :K(snat A′). let x′ = x_{1} < x_{2} in k x′))

K_{exp}[[(if[B, A](e^{sbool A′′}, X_{1}. e_{1}^{A′}, X_{2}. e_{2}^{A′}))^{A′}]] = λk:K_{c}(A′). K_{exp}[[e^{sbool A′′}]] (λx:K(sbool A′′). if[B, A](x, X_{1}. K_{exp}[[e_{1}^{A′}]] k, X_{2}. K_{exp}[[e_{2}^{A′}]] k))

Figure 6: CPS conversion: from λ_{H} to λ_{K}.

In addition to the symbols defined in the syntax, we will also use C to denote general terms, Y and Z for variables, and I for inductive definitions. We use A⃗ to denote a sequence of terms A_{1},…, A_{n}. Also, we distinguish between A and A⃗ since every element in A⃗ would be referred as A_{i} anyway.

TL has the following PTS specification which will be used to

C_{val}[[v]]  = v,  for v one of x, \overline{n}, tt, ff
C_{val}[[⟨v_{0}, … v_{n−1}⟩]]  = ⟨C_{val}[[v_{0} ]], … C_{val}[[v_{n−1} ]]⟩
C_{val}[[⟨X =A, v:B⟩]]  = ⟨X =A, C_{val}[[v]]:Cl (B) ⊥⟩
C_{val}[[fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e]] =
⟨X =A_{env}, ⟨v_{code}[Y_{1}] … [Y_{m}], v_{env}⟩:A_{X}⟩

where

A_{X} = A′_{X} × X

A′_{X} = ∀_{s_{1}}X_{1} :A_{1}…. ∀_{s_{n}}X_{n}:A_{n}. (X × Cl (A) ⊥)→⊥ {x_{0}^{A′_{0}}, … x_{k−1}^{A′_{k−1}}} = FV (e) − {x, x′} {Y_{1}^{B′_{1}}, … Y_{m}^{B′_{m}}} =

FTV (fix x′[X_{1} :A_{1}, … X_{n}:A_{n}](x:A). e)

A_{env} = Cl (tup k̂ (nth (A′_{0}:: … A′_{k−1}::nil))) ⊥

v_{env} = ⟨x_{0} … x_{k−1}⟩

v_{code} = fix v_{fix}[Y_{1} :B′_{1}, … Y_{m}:B′_{m}, X_{1} :A_{1}, … X_{n}:A_{n}] (x_{arg} :A_{env} × Cl (A) ⊥). let x_{env} = sel[ltPrf ˆ0 ˆ2](x_{arg}, \overline{0}) in let x = sel[ltPrf ˆ1 ˆ2](x_{arg}, \overline{1}) in let x′ = ⟨\begin{matrix}X =A_{env}, \\ ⟨v_{fix}[Y_{1}] … [Y_{m}], x_{env}⟩:A_{X}⟩ in \end{matrix} let x_{0} = sel[ltPrf ˆ0 k̂](x_{env}, \overline{0}) in … let x_{k−1} = sel[ltPrf { \atop k − 1} k̂](x_{env}, \overline{k − 1}) in C_{exp}[[e]]

C_{exp}[[v_{1}[A_{1}, … A_{n}](v_{2})]] = let ⟨X_{env}, x_{arg}⟩ = open C_{val}[[v_{1} ]] in

let x_{code} = sel[ltPrf ˆ0 ˆ2](x_{arg}, \overline{0}) in
let x_{env} = sel[ltPrf ˆ1 ˆ2](x_{arg}, \overline{1}) in
x_{code}[A_{1}] … [A_{n}] ⟨x_{env}, C_{val}[[v_{2} ]]⟩
C_{exp}[[let x = v in e]]  = let x = C_{val}[[v]] in C_{exp}[[e]]
C_{exp}[[let x = sel[A](v, v′) in e]] =
let x = sel[A](C_{val}[[v]], C_{val}[[v′]]) in C_{exp}[[e]]
C_{exp}[[let ⟨X, x⟩ = open v in e]] =
let ⟨X, x⟩ = open C_{val}[[v]] in C_{exp}[[e]]
C_{exp}[[let x = v_{1} + v_{2} in e]] = let x = C_{val}[[v_{1} ]] + C_{val}[[v_{2} ]] in C_{exp}[[e]]
C_{exp}[[let x = v_{1} < v_{2} in e]] = let x = C_{val}[[v_{1} ]] < C_{val}[[v_{2} ]] in C_{exp}[[e]]
C_{exp}[[if[B, A](v, X_{1}. e_{1}, X_{2}. e_{2})]] =
if[B, A](C_{val}[[v]], X_{1}. C_{exp}[[e_{1} ]], X_{2}. C_{exp}[[e_{2} ]])

Figure 7: Closure conversion: from λ_{K} to λ_{C}.

derive its typing rules:

S = Kind, Kscm, Ext
A = Kind:Kscm, Kscm:Ext
R = (Kind, Kind), (Kscm, Kind), (Ext, Kind)

(Kind, Kscm), (Kscm, Kscm)

In order to ensure that the interpretation of inductive definitions remains consistent, and they can be interpreted as terms closed under their introduction rules, we impose positivity constraints on the constructors of an inductive definition. The positivity constraints are defined in Definition 4 and 5.

Definition 4 A term A is strictly positive in X if A is either X or ΠY : B. A′, where A′ is strictly positive in X, X does not occur free in B, and X ≠ Y.

Definition 5 A term C is a well-formed constructor kind for X (written wfc_{X}(C)) if it has one of the following forms:

1. X; 2. ΠY : B. C′, where Y ≠ X, X is not free in B, and C′ is a

well-formed constructor kind for X; or

3. A → C′, where A is strictly positive in X and C′ is a wellformed constructor kind for X.

Note that in the definition of wfc_{X}(C), the second clause covers the case where C is of the form A → C′, and X does not occur free in A. Therefore, we only allow the occurrence of X in the non-dependent case.

In the rest of this paper we often write the well-formed constructor kind for X as ΠY⃗ : B⃗. X. We also denote terms that are strictly positive in X by ΠY⃗ :B⃗. X, where X is not free in B⃗.

Definition 6 Let C be a well-formed constructor kind for X. Then C is of the form ΠY⃗ : A⃗. X. If all the Y ’s are t’s, that is, C is of the form Πt⃗: A⃗. X, then we say that C is a small constructor kind (or just small constructor when there is no ambiguity) and denote it as small(C).

Our inductive definitions reside in Kind, whereas a small constructor does not make universal quantification over objects of type Kind. Therefore, an inductive definition with small constructors is a predicative definition. While dealing with impredicative inductive definitions, we must forbid projections on universes equal to or bigger than the one inhabited by the definition. In particular, we restrict large elimination to inductive definitions with only small constructors.

Next, we define the set of reductions on our terms. The definition of β- and η-reduction is standard. The ι-reduction defines primitive recursion over inductive objects.

Definition 7 Let C be a well-formed constructor kind for X and let A′, B′, and I be pseudoterms. We define Φ_{X,I,B′}(C, A′) recursively based on the structure of C:

Φ_{X,I,B′}(X, A′)  =^{def} A′
Φ_{X,I,B′}(ΠY :B. C′, A′) =^{def} λY :B. Φ_{X,I,B′}(C′, A′ Y)

Φ_{X,I,B′}((ΠY⃗ :B⃗. X)→C′, A′) =^{def}

λZ:(ΠY⃗ :B⃗. I). Φ_{X,I,B′}(C′, A′ Z (λY⃗ :B⃗. B′ (Z Y⃗)))

Definition 8 The reduction relations on our terms are defined as:

(λX:A. B) A′ ⇝_{β} [A′/X]B
λX:A. (B X) ⇝_{η} B, if X ∉ FV (B)
Elim[I, A′′](Ctor (i, I) A⃗){B⃗} ⇝_{ι} (Φ_{X,I,B′}(C_{i}, B_{i})) A⃗

where

I = Ind(X:Kind){C⃗}
B′ = λY :I. (Elim[I, A′′](Y){B⃗})

By ⊳_{β}, ⊳_{η}, and ⊳_{ι} we denote the relations that correspond to the rewriting of subterms using the relations ⇝_{β}, ⇝_{η}, and ⇝_{ι} respectively. We use ⇝ and ⊳ for the unions of the above relations. We also write ⊳^{∗} and ⊳^{+} (respectively ⊳_{β}^{∗} etc.) for the reflexive-transitive and transitive closures of ⊳ (respectively ⊳_{β} etc.) and =_{βηι} for the reflexive-symmetric-transitive closure of ⊳. We say that a sequence of terms A_{1},…, A_{n}, such that A ⊳ A_{1} ⊳ A_{2} … ⊳ A_{n}, is a chain of reductions starting from A.

Let us examine the ι-reduction in detail. In Elim[I, A′′](A){B⃗}, the term A of type I is being analyzed. The sequence B⃗ contains the set of branches for Elim, one for each constructor of I. In the case when C_{i} = X, which implies that A is of the form Ctor (i, I), the Elim just selects the B_{i} branch:

Elim[I, A′′](Ctor (i, I)){B⃗} ⇝_{ι} B_{i}

In the case when C_{i} = ΠY⃗ : B⃗. X where X does not occur free in B⃗, then A must be in the form Ctor (i, I) A⃗ with A_{i} of type B_{i}. None of the arguments are recursive. Therefore, the Elim should just select the B_{i} branch and pass the constructor arguments to it. Accordingly, the reduction yields (by expanding the Φ macro):

Elim[I, A′′](Ctor (i, I) A⃗){B⃗} ⇝_{ι} B_{i} A⃗

The recursive case is the most interesting. For simplicity assume that the i-th constructor has the form ΠY⃗ :B⃗′. X → ΠY⃗′:B⃗′′. X. Therefore, A is of the form Ctor (i, I) A⃗ with A_{1} being the recursive component of type ΠY⃗ : B⃗′. X, and A_{2} … A_{n} being nonrecursive. The reduction rule then yields:

Elim[I, A′′](Ctor (i, I) A⃗){B⃗} ⇝_{ι} B_{i} A_{1} (λY⃗ :B⃗′. Elim[I, A′′](A_{1} Y⃗){B⃗}) A_{2} … A_{n}

The Elim construct selects the B_{i} branch and passes the arguments A_{1},…, A_{n}, and the result of recursively processing A_{1}. In the general case, it would process each recursive argument.

Definition 9 defines the Ψ macro which represents the type of the large Elim branches. Definition 10 defines the ζ macro which represents the type of the small elimination branches. The different cases follow from the ι-reduction rule in Definition 8.

Definition 9 Let C be a well-formed constructor kind for X and let A′ and I be two terms. We define Ψ_{X,I}(C, A′) recursively based on the structure of C:

Ψ_{X,I}(X, A′)  =^{def} A′
Ψ_{X,I}(ΠY :B. C′, A′) =^{def} ΠY :B. Ψ_{X,I}(C′, A′)
Ψ_{X,I}(A→C′, A′) =^{def} [I/X]A→[A′/X]A→Ψ_{X,I}(C′, A′)

where X is not free in B and A is strictly positive in X.

Definition 10 Let C be a well-formed constructor kind for X and let A′, I, and B′ be terms. We define ζ_{X,I}(C, A′, B′) recursively based on the structure of C:

ζ_{X,I}(X, A′, B′)  =^{def} A′ B′
ζ_{X,I}(ΠY :B. C′, A′, B′)  =^{def} ΠY :B. ζ_{X,I}(C′, A′, B′ Y)

ζ_{X,I}(ΠY⃗ :B⃗. X → C′, A′, B′) =^{def}

ΠZ:(ΠY⃗ :B⃗. I). ΠY⃗ :B⃗. (A′ (Z Y⃗)) → ζ_{X,I}(C′, A′, B′ Z)

where X is not free in B and B⃗.

Definition 11 We use Δ|_{t,k} to denote that the environment does not contain any z variables.

Here are the complete typing rules for TL. The three weakening rules make sure that all variables are bound to the right classes of terms in the context. There are no separate context-formation rules; a context Δ is well-formed if we can derive the judgment Δ ⊢ Kind : Kscm (notice we can only add new variables to the context via the weakening rules).

· ⊢ Kind : Kscm  (ax1)

· ⊢ Kscm : Ext  (ax2)

Δ ⊢ C : Kind Δ ⊢ A : B t ∉ Dom(Δ)

Δ, t:C ⊢ A : B (weak1)

Δ ⊢ C : Kscm Δ ⊢ A : B k ∉ Dom(Δ)

Δ, k:C ⊢ A : B (weak2)

{Δ ⊢ C : Ext Δ ⊢ A : B z ∉ Dom(Δ) \atop Δ, z:C ⊢ A : B}  (weak3)

Δ ⊢ Kind : Kscm X ∈ Dom(Δ)

Δ ⊢ X : Δ(X) (var)

{Δ, X:A ⊢ B : B′  Δ ⊢ ΠX:A. B′ : s \atop Δ ⊢ λX:A. B : ΠX:A. B′}  (fun)

\begin{matrix}Δ ⊢ A : ΠX:B′. A′ & Δ ⊢ B : B′ \\ Δ ⊢ A B : [B/X]A′ \end{matrix}  (app)

\begin{aligned}Δ ⊢ A : s_{1} & Δ, X:A ⊢ B : s_{2} & (s_{1}, s_{2}) ∈ R \\ & Δ ⊢ ΠX:A. B : s_{2} \end{aligned}  (prod)

for all i Δ, X:Kind ⊢ C_{i} : Kind wfc_{X}(C_{i})

Δ ⊢ Ind(X:Kind){C⃗} : Kind

(ind)

Δ ⊢ I : Kind where I = Ind(X:Kind){C⃗} Δ ⊢ Ctor (i, I) : [I/X]C_{i}

(con)

Δ ⊢ A : I Δ ⊢ A′ : I → Kind for all i Δ ⊢ B_{i} : ζ_{X,I}(C_{i}, A′, Ctor (i, I))

Δ ⊢ Elim[I, A′](A){B⃗} : A′ A where I = Ind(X:Kind){C⃗}

(elim)

Δ ⊢ A : I Δ|_{t,k} ⊢ A′ : Kscm

for all i small(C_{i}) Δ ⊢ B_{i} : Ψ_{X,I}(C_{i}, A′)

Δ ⊢ Elim[I, A′](A){B⃗} : A′ where I = Ind(X:Kind){C⃗}

(l-elim)

\begin{matrix}Δ ⊢ A : B \\ Δ ⊢ B′ : s Δ ⊢ B : s B =_{βηι} B′ \end{matrix} ; Δ ⊢ A : B′  (conv)

D.2 Subject Reduction

The proof is structured as follows:

• We first define a calculus of unmarked terms. These are terms with no annotations at lambda abstractions. We show that this language is confluent.

• We then prove Geuvers’ lemma – a weak form of confluence. It says that a term that is equal to one in head normal form can be reduced to an η-expanded version of this head normal form.

• From Geuvers’ lemma, we are able to prove the inversion lemma which relates the structure of a term to its typing derivation.

• We are then able to prove the uniqueness of types and subject reduction for βι reduction.

• We are then able to prove that the system preserves sorts – that is, if two terms are convertible and well sorted, then they have the same sort.

• Finally, we prove the strengthening lemma and then subject reduction for η reduction.

D.2.1 Unmarked terms

The PTS language is non-confluent. Nederpelt gave the following counterexample – let A be the term defined by λX : A_{1}. (λY :A_{2}. Y)X. Then we have that A ⊳_{β} λX : A_{1}. X and A ⊳_{η} λY : A_{2}. Y. For our proofs we want to operate in a language that is confluent. We will therefore introduce the notion of unmarked terms. As non-confluence is due to the presence of type annotations in λ abstractions, the unmarked terms are obtained by erasing the type annotations.

The set of unmarked terms ∥ A ∥ are defined below. We are given a marked variable that can not be used elsewhere.

∥s∥ = s
∥X ∥ = X
∥A_{1} A_{2} ∥ = ∥A_{1} ∥ ∥A_{2} ∥
∥λX:A_{1}. A_{2} ∥ = λX: . ∥A_{2} ∥
∥ΠX:A_{1}. A_{2} ∥ = ΠX:∥A_{1} ∥ . ∥A_{2} ∥
∥Ind(X:Kind)\{A⃗\}∥ = Ind(X:Kind)\{\overrightarrow{∥A∥}\}
∥Ctor (i, A_{1})∥ = Ctor (i, ∥A_{1} ∥)
∥Elim[I, A_{2}](A_{1})\{A⃗\}∥ = Elim[∥I ∥, ∥A_{2} ∥](∥A_{1} ∥)\{\overrightarrow{∥A∥}\}

Lemma 6 For all terms A, B, A′, B′, and for all variables X and Y, we have that [λY :A′. B/X]A =_{βηι} [λY :B′. B/X]A.

Proof Consider A_{2} = [λZ : A′. (λY :B′. B) Z/X]A. Then A_{2} ⊳_{β} [(λZ : A′. [Z/Y]B)/X]A and A_{2} ⊳_{η} [λY : B′. B/X]A. Alpha converting the first reduct leads to the required result. □

Lemma 7 For all terms A, we have A =_{βη}∥A∥.

Proof Follows from lemma 6. □

Definition 12 (ι_{0} reduction) We say that A⊳_{ι_{0}} ∥A′ ∥ iff A⊳_{ι} A′ and ∥A∥≠∥A′ ∥.

Proposition 13 For all terms A and A′, if A ⊳_{β} A′, then ∥ A ∥ ⊳_{β} ∥A′ ∥ or ∥A∥=∥A′ ∥. Similarly, if we have that A ⊳_{ι} A′, then ∥A∥ ⊳_{ι_{0}} ∥A′ ∥ or ∥A∥=∥A′ ∥. Moreover, if ∥A∥ ⊳_{βι_{0}} ∥A′ ∥, then there exists a A′′ such that A ⊳_{βι} A′′ and ∥A′′ ∥=∥A′ ∥.

Lemma 8 (Confluence for unmarked terms) For all unmarked terms ∥A∥, the βηι_{0} reduction is confluent.

The proof is based on the method of parallel reductions due to Tait and Martin-Löf.

Definition 14 (Parallel reduction) Define → → on unmarked terms as below, in which we assume that A → → A′, B → → B′, etc:

A → → A
A B → → A′ B′
λX: . A → → λX: . A′
ΠX:A. B → → ΠX:A′. B′
Ind(X:Kind){A⃗} → → Ind(X:Kind){A⃗′}
Ctor (i, I) → → Ctor (i, I′)
Elim[A, C](I){A⃗} → → Elim[A′, C′](I′){A⃗′}
(λX: . A) B → → [B′/X]A′
λX: . A X → → A′ if X ∉ FV (A)
Elim[I, C]((Ctor (i, I) B⃗)){A⃗} → → (Φ_{X,I′,B′}(C′_{i}, A′_{i})) B⃗′
where I = Ind(X:Kind){C⃗}
B′ = λY : . (Elim[I′, C′](Y){A⃗′})

The parallel reduction commutes with respect to substitution.

Lemma 9 If A → → A′ and B → → B′, then [B/X]A → → [B′/X]A′.

Proof By induction over the fact that A → → A′. □

The parallel reduction also has the following properties with respect to terms such as products and inductive definitions. The proof in each case is immediate and follows by induction over the structure of the term.

Proposition 15 Suppose A = ΠX: B⃗. Y C⃗. If A can be reduced to A′ through a reduction relation (→ →, ⊳_{β}, etc.), then A′ = ΠX: B⃗′. Y C⃗′ where all the B⃗ and C⃗ can be reduced to B⃗′ and C⃗′ by the same reduction relation.

Proposition 16 Suppose A = ΠX : B⃗. Y C⃗ and A′ = ΠX : B⃗′. Y C⃗′ be two terms such that both can be reduced to A′′ through a reduction relation (→ →, ⊳_{β}, etc.). Then A′′ = ΠX : B⃗′′. Y C⃗′′ where B⃗ and B⃗′ can be reduced to B⃗′′ by the same relation and C⃗ and C⃗′ can be reduced to C⃗′′ by the same relation.

The parallel reduction is important because it subsumes the single step reduction; that is, if A ⊳ A′, then we have that A → → A′ which also implies that A⊳^{∗}A′. From here, to show the confluence of ⊳, it suffices to show the confluence of parallel reduction.

Lemma 10 For all unmarked terms D, D′, D′′, we have that if D → → D′ and D → → D′′, then there exists a D′′′ such that D′ → → D′′′ and D′′ → → D′′′.

Proof The proof is by induction over the structure of D. We will only show one case here.

• Suppose D = Elim[I, C]((Ctor (i, I) B⃗)){A⃗}.

– We can then have D′ = (Φ_{X,I′,B′}(C′_{i}, A′_{i})) B⃗′ and D′′ = (Φ_{X,I′′,B′}(C′′_{i}, A′′_{i})) B⃗′′. We have that I′ = Ind(X : Kind){C⃗′} and I′′ = Ind(X : Kind){C⃗′′}. This implies that C_{i} → → C′_{i} and C_{i} → → C′′_{i}. By applying the induction hypothesis to the subterms, we get that I′ → → I′′′ and I′′ → → I′′′ and so on for the other subterms. From here and proposition 16, it follows that we can take D′′′ = (Φ_{X,I′′′,B′}(C′′′_{i}, A′′′_{i})) B⃗′′′.

– Suppose D′ = Elim[I′, C′]((Ctor (i, I′) B⃗′)){A⃗′} and D′′ = (Φ_{X,I′′,B′}(C′′_{i}, A′′_{i})) B⃗′′. As above we can again define I′′′, C′′′_{i}, etc. and take D′′′ = (Φ_{X,I′′′,B′}(C′′′_{i}, A′′′_{i})) B⃗′′′.

– Also D′ = Elim[I′, C′]((Ctor (i, I′) B⃗′)){A⃗′} and D′′ = Elim[I′′, C′′]((Ctor (i, I′′) B⃗′′)){A⃗′′}. In this case, we can again take that D′′′ = Elim[I′′′, C′′′]((Ctor (i, I′′′) B⃗′′′)){A⃗′′′}.

□

As a corollary of the confluence of unmarked terms we get the following:

Corollary 17 If A and B are two distinct sorts or two distinct variables or a variable and a sort, then we have that A ≠ B.

We will need another lemma – that of the delay of η reduction. But before that, we have to define another variant of the ι reduction. This essentially says that a ι reduction that would appear only after a series of eta reductions can be reduced straightaway without going through the eta reductions. For well typed terms, this is equivalent to ι reduction, but it also allows us to retain the property of delay of η reduction for ill-typed terms.

Elim[I, A′′](λX⃗:A⃗′. (Ctor (i, I) A⃗)C⃗′){B⃗} ⊳_{ι′}
(Φ_{X,I,B′}(C_{i}, B_{i})) A⃗
whereI = Ind(X:Kind){C⃗}
B′ = λY :I. (Elim[I, A′′](Y){B⃗})
C_{i}′ ⊳_{η} X_{i} and X_{i} ∉ FV (A⃗) ∪ FV (I)

Proposition 18 For all terms A_{1} and A_{2}, we have that A_{1} =_{βηι} A_{2} if and only if A_{1} =_{βηι′} A_{2}.

Lemma 11 If A ⊳_{η} A′ ⊳_{βι′} A′′, then either A ⊳_{βι′}^{∗} A′′, or there exists a A′′′ such that A ⊳_{βι′} A′′′ ⊳_{η}^{∗} A′′.

Proof The proof is by induction over the structure of A. We will consider only the cases that do not follow directly from the induction hypothesis.

• A = C D. There are two cases.

– If C ⊳_{η} C′, then it follows immediately from the induction hypothesis.

– If D⊳_{η} D′ and C = λX:B. B′ and A′′ = [D′/X]B′, then take A′′′ = [D/X]B′. The other cases follow from the induction hypothesis.

• A = λX : C. B X. Suppose A′′ = B′ where B ⊳_{βι′} B′. But then we also have that A ⊳_{βι′} λX: C. B′ X. Since the reduction does not introduce new free variables, this term can now η-reduce to B′.

□

Lemma 12 (Delay of η reduction) For all terms A and A′, if A ⊳^{∗} A′, then there exists a term A′′ such that A ⊳_{βι′}^{∗} A′′ ⊳_{η}^{∗} A′.

Proof Follows from lemma 11. □ We will next prove Geuvers’ lemma which is essentially a weak form of confluence. This is enough to prove the uniqueness of types and subject reduction. But before that we need to define the counterpart of the ι′ reduction for unmarked terms. We define it in the obvious way

Definition 19 (ι′_{0} reduction) We say that A⊳_{ι′_{0}} ∥A′ ∥ iff A⊳_{ι′} A′ and ∥A∥≠∥A′ ∥.

As before it has the following property:

Proposition 20 Suppose A ⊳_{ι′} A′. Then either ∥ A ∥=∥ A′ ∥, or ∥A∥ ⊳_{ι′_{0}} ∥A′ ∥. Moreover, if ∥A∥ ⊳_{ι′_{0}} ∥A′ ∥, then A ⊳_{ι′} A′.

Lemma 13 (Geuvers lemma)

• If A =_{βηι} X A⃗, then

A ⊳_{βι′}^{∗} λY⃗ :A⃗′. (X B⃗ C⃗)
where for all i, A_{i} =_{βηι} B_{i} and for all j, C_{j} ⊳_{η}^{∗} Y_{j}.

• If A =_{βηι} ΠX:A_{1}. A_{2}, then

A ⊳_{βι′}^{∗} λY⃗ :A⃗′. ((ΠX:A_{3}. A_{4}) B⃗)
where A_{1} =_{βηι} A_{3} and A_{2} =_{βηι} A_{4} and for all i, B_{i} ⊳_{η}^{∗} Y_{i}.

• If A =_{βηι} Ctor (i, I) C⃗, then

A ⊳_{βι′}^{∗} λY⃗ :A⃗′. ((Ctor (i, I′) C⃗′) B⃗)

where for all i, C_{i} =_{βηι} C′_{i} and for all j, B_{j} ⊳_{η}^{∗} Y_{j}, and I =_{βηι} I′.

• If A =_{βηι} Ind(X:Kind){A⃗} C⃗, then

A ⊳_{βι′}^{∗} λY⃗ :A⃗′. ((Ind(X:Kind){A⃗′′}) C⃗′) B⃗

where for all i, A_{i} =_{βηι} A′′_{i} and for all j, C_{j} =_{βηι} C′_{j}, and for all k, B_{k} ⊳_{η}^{∗} Y_{k}.

• If A =_{βηι} Elim[I, A_{2}](A_{1}){A⃗′′} C⃗, then

A ⊳_{βι′}^{∗} λY⃗ :A⃗′. (Elim[I′, B′](B){B⃗} C⃗′) B⃗′

where A_{1} =_{βηι} B, and A_{2} =_{βηι} B′, and I =_{βηι} I′, and for all i, A′′_{i} =_{βηι} B_{i} and for all j, C_{j} =_{βηι} C′_{j} and for all k, B′_{k} ⊳_{η}^{∗} Y_{k}.

Proof The proof for each of the cases is similar and is by induction over the length of the equivalence relation. We will show only one case here.

• Suppose A =_{βηι} X A⃗. By the induction hypothesis, there exists an A′′ such that

A′′ ⊳_{βι′}^{∗} λY⃗ :A⃗′. (X B⃗ C⃗)

and A ⊳_{βι} A′′ or A′′ ⊳_{βι} A.

– The case where A ⊳_{βι} A′′ is immediate.

– The case where A ⊳_{η} A′′ follows from the lemma of delay of η-reduction.

– If A′′ ⊳_{βι} A, then the required result follows from the confluence of βι′ reduction.

– Suppose A′′ ⊳_{η} A. Then from the confluence of βηι′_{0} reduction on unmarked terms, we get that ∥ A ∥ ⊳^{∗}X D⃗ where ∥ B_{i} ∥ ⊳_{βηι′_{0}} D_{i}. From the lemma of delay of η-reduction, we get that

∥A∥ ⊳_{βι′_{0}}^{∗}λY⃗ : . X D⃗′F⃗ ⊳_{η}^{∗} X D⃗

From proposition 20 we can deduce the existence of a term A_{1} such that A ⊳_{βι′}^{∗} A_{1} and ∥ A_{1} ∥= λY⃗ : . X D⃗′F⃗. The required result follows from here.

□

D.2.2 Classification of terms

Definition 21 We partition the set of terms into four classes: the set of types Ty, the set of kinds Ki, the set of kind schemas Sc, and Ex. The class of a term is defined as follows:

Cls(Kind) = Sc
Cls(Kscm) = Ex
Cls(t) = Ty
Cls(k) = Ki
Cls(z) = Sc
Cls(A_{1} A_{2}) = Cls(A_{1})
Cls(λX:A_{1}. A_{2}) = Cls(A_{2})
Cls(ΠX:A_{1}. A_{2}) = Cls(A_{2})
Cls(Ind(X:Kind){A⃗}) = Ki
Cls(Ctor (i, A_{1})) = Ty
Cls(Elim[I, A_{2}](A_{1}){A⃗}) = Ty if Cls(A_{2}) = Ki, else Ki

We also define the following function:

lift(Ty) = Ki
lift(Ki) = Sc
lift(Sc) = Ex

Lemma 14 If Δ ⊢ A_{1} : A_{2} is derivable, then we have lift(Cls(A_{1})) = Cls(A_{2}). In particular, A_{1} ≠ Ext. Moreover, for all pairs (X, A) in Δ, we have Cls(A) = lift(Cls(X)).

Proof Immediate by induction over the derivation of the judgment. □

D.2.3 Well typed terms

We now consider the well typed terms. The following lemmas are proved easily by induction over the typing derivations.

Lemma 15 (Substitution) If we can derive Δ_{1}, (X, A), Δ_{2} ⊢ B : C and Δ_{1} ⊢ A_{2} : A, then we can derive Δ_{1}, ([A_{2}/X]Δ_{2}) ⊢ [A_{2}/X]B : [A_{2}/X]C.

Proof Straightforward induction over the structure of the derivation. □

Lemma 16 If we can derive Δ_{1}, (X, A), Δ_{2} ⊢ B : C, then we also have that Δ_{1} ⊢ A : s for some sort s. Moreover, we also have that Δ_{1}, (X, A), Δ_{2} ⊢ A : s.

Proof The proof is by induction over the structure of the derivation. □

Lemma 17 If we have that Δ ⊢ ΠX:A. B : s, then we have that Δ, X:A ⊢ B : s.

Proof The only interesting case is for the conv case which follows from Corollary 17. □

Lemma 18 If the judgment Δ ⊢ A : B is derivable, then either B = Ext, or Δ ⊢ B : s for some sort s.

Proof The proof is a straightforward induction over the structure of the derivation. □

Lemma 19 (Inversion) If the judgment Δ ⊢ A : B is derivable, then

A = t  ⇒ \begin{matrix}t ∈ Δ \\ B =_{βηι} Δ(t) \\ Δ ⊢ B : Kind \end{matrix}

A = k  ⇒ \begin{matrix}k ∈ Δ \\ B =_{βηι} Δ(k) \\ Δ ⊢ B : Kscm \end{matrix}

A = z  ⇒ \begin{matrix}z ∈ Δ \\ B =_{βηι} Δ(z) \\ Δ ⊢ B : Ext \end{matrix}

A = Kind  ⇒ B =_{βηι} Kscm
A = Kscm  ⇒ B = Ext

A = ΠX:A_{1}. A_{2} ⇒ Δ ⊢ A_{1} : s_{1} Δ, X:A_{1} ⊢ A_{2} : s_{2} B =_{βηι} s_{2}

where s_{1} is any sort and

s_{2} = Kind, or s_{1} ∈ {Kind, Kscm} and s_{2} = Kscm

A = λX:A_{1}. A_{2}  ⇒ \begin{matrix}Δ ⊢ A_{1} : s_{1} \\ Δ, X:A_{1} ⊢ A_{2} : A_{3} \\ Δ ⊢ A_{3} : s_{2} \\ B =_{βηι} ΠX:A_{1}. A_{3} \\ Δ ⊢ B : s_{2} \end{matrix}

A = A_{1} A_{2}  ⇒ \begin{matrix}Δ ⊢ A_{1} : ΠX:B′. A′ \\ Δ ⊢ A_{2} : B′ \\ B =_{βηι} [A_{2}/X]A′ \end{matrix}

A = Ind(X:Kind){A⃗} ⇒ Δ, X:Kind ⊢ A_{i} : Kind wfc_{X}(A_{i}) B =_{βηι} Kind

A = Ctor (i, I) ⇒ I = Ind(X:Kind){A⃗} same conditions on I B =_{βηι} [I/X]A_{i}

A = Elim[I, A′](A){B⃗} ⇒ I = Ind(X:Kind){A⃗} same conditions on I Δ ⊢ A : I Δ ⊢ A′ : I → Kind Δ ⊢ B : Kind B =_{βηι} A′ A Δ ⊢ B_{i} :

ζ_{X,I}(A_{i}, A′, Ctor (i, I))

A = Elim[I, A′](A){B⃗} ⇒ I = Ind(X:Kind){A⃗} same conditions on I Δ ⊢ A : I Δ ⊢ A′ : Kscm Δ ⊢ B : Kscm and B =_{βηι} A′ Δ ⊢ B_{i} : Ψ_{X,I}(A_{i}, A′) for all i small(A_{i})

Proof By induction over the structure of the derivation. For every case we consider the set of possible typing derivations. □

Lemma 20 (Uniqueness of types) If Δ ⊢ A : A_{1} and Δ ⊢ A : A_{2}, then A_{1} =_{βηι} A_{2}.

Proof By induction over the structure of A. We use the fact that if A_{1} =_{βηι} B and A_{2} =_{βηι} B, then A_{1} =_{βηι} A_{2}. For every case, we use the corresponding clause from lemma 19. □

Corollary 22 Suppose A is a well typed term. If A ⊳_{ι′} A′, then A ⊳_{ι} A′.

D.2.4 Reductions on well typed terms

Lemma 21 (Subject reduction for βι reduction) If the judgment Δ ⊢ A : B is derivable, and if A ⊳_{βι} A′ and Δ ⊳_{βι} Δ′, then we have that

Δ ⊢ A′ : B Δ′ ⊢ A : B

Proof The interesting cases are the app and elim.

• app When only the sub-terms reduce without a reduction at the head, the lemma follows by using the induction hypothesis on the sub-terms. Suppose that

A = λX:A_{1}. A_{2} \begin{matrix}Δ ⊢ A : ΠX:B′. A′ & Δ ⊢ B : B′ \\ Δ ⊢ A B : [B/X]A′ \end{matrix}

and A B ⊳_{β} [B/X]A_{2}. We know from lemma 19 that

Δ, X:A_{1} ⊢ A_{2} : A_{3}
ΠX:A_{1}. A_{3} =_{βηι} ΠX:B′. A′
Δ ⊢ A_{1} : s_{1}
Δ ⊢ B′ : s_{2}

This implies that A_{1} =_{βηι} B′ and A_{3} =_{βηι} A′. Moreover,

Cls(B′) = Cls(A_{1}) = lift(Cls(X))

Therefore, we get from lemma 14 that

Cls(s_{2}) = Cls(s_{1}) ⇒ s_{2} = s_{1}

Applying the conv rule we get that Δ ⊢ B : A_{1}. By lemma 15 we get that Δ ⊢ [B/X]A_{2} : [B/X]A_{3}. We can show in a similar manner as before that Cls(A_{3}) = Cls(A′). This allows us to apply the conv rule again which leads to the required result.

• l-elim We will only consider the case when an ι reduction takes place at the head. The other cases follow easily by structural induction.

Δ ⊢ A : I Δ ⊢ A′ : Kscm
for all i Δ ⊢ B_{i} : Ψ_{X,I}(C_{i}, A′)
Δ ⊢ Elim[I, A′](A){B⃗} : A′
where I = Ind(X:Kind){C⃗}and ∀i. small(C_{i})

The interesting case is when we consider the reduction

Elim[I, A′](Ctor (i, I) A⃗){B⃗} ⊳_{ι} (Φ_{X,I,B′}(C_{i}, B_{i})) A⃗

where I = Ind(X:Kind){C⃗}
B′ = λY :I. (Elim[I, A′](Y){B⃗})

Suppose A′′ = (Φ_{X,I,B′}(C_{i}, B_{i})) A⃗. Suppose that A⃗ = A_{1...n}. We have that Δ ⊢ B_{i} : Ψ_{X,I}(C_{i}, A′). The proof is by induction on the fact that C_{i} is a kind of a constructor and the length of A⃗. We consider the different cases by which C_{i} is a kind of a constructor.

– If C_{i} = X, then A′′ = B_{i}. From definition 9 we can see that in this case, B_{i} has the type A′.

– If C_{i} = ΠY :B. C, then A′′ = (Φ_{X,I,B′}([A_{1}/Y]C, B_{i} A_{1})) A_{2...n}. We have that Δ ⊢ B_{i} A_{1} : Ψ_{X,I}([A_{1}/Y]C, A′). By the induction hypothesis, the reduct has type A′.

– If C_{i} = ΠY⃗ :B⃗. X →C, then

\begin{matrix}A′′ = \\ Φ_{X,I,B′}(C, B_{i} A_{1} (λY⃗ :B⃗. B′ (A_{1} Y⃗))) A_{2...n} \end{matrix}

From Definition 9 we have that

Δ ⊢ B_{i} : [I/X]A → [A′/X]A → Ψ_{X,I}(C′, A′). We also know that Δ ⊢ A_{1} : [I/X]A. From here, we can apply the induction hypothesis and show that the reduct has type A′.

• elim We will only consider the case when an ι reduction takes place at the head. The other cases follow easily by structural induction.

Δ ⊢ A : I Δ ⊢ A′ : I → Kind

for all i Δ ⊢ B_{i} : ζ_{X,I}(C_{i}, A′, Ctor (i, I))

Δ ⊢ Elim[I, A′](A){B⃗} : A′ A‘ where I = Ind(X:Kind){C⃗}

The interesting case is when we consider the reduction

Elim[I, A′](Ctor (i, I) A⃗){B⃗} ⊳_{ι} (Φ_{X,I,B′}(C_{i}, B_{i})) A⃗

where I = Ind(X:Kind){C⃗}
B′ = λY :I. (Elim[I, A′](Y){B⃗})

Suppose A′′ = (Φ_{X,I,B′}(C_{i}, B_{i})) A⃗. Suppose that A⃗ = A_{1...n}. We have that Δ ⊢ B_{i} : ζ_{X,I}(C_{i}, A′, Ctor (i, I)). By using the inversion lemma we can get that Δ ⊢ B′ : ΠX : I. A′ X. By induction on the structure of C_{i} (where C_{i} is a kind of a constructor), we can show that if C_{i} = ΠY⃗ : B⃗. X, then Δ ⊢ Φ_{X,I,B′}(C_{i}, B_{i}) : ΠY⃗ : B⃗. A′ Ctor (i, I) Y⃗. The required result follows from here.

□

Corollary 23 Suppose A is a well formed term. If A⊳_{βι′}^{∗} A′, then A ⊳_{βι}^{∗} A′ and A′ is well formed.

Corollary 24 Suppose A is a well formed term. If A ⊳^{∗} A′, then there exists a well formed term A′′ such that A ⊳_{βι}^{∗} A′′ ⊳_{η}^{∗} A′.

Lemma 22 Let Δ ⊢ A : B and Δ ⊢ A′ : B′ be two derivable judgments. If A =_{βηι} A′, then Cls(A) = Cls(A′).

Proof We know that ∥A∥ and ∥A′ ∥ have a common reduct, say A_{2}. This implies that

∥A∥ ⊳_{βι′_{0}}^{∗}B ⊳_{η}^{∗} A_{2}  and  ∥A′ ∥ ⊳_{βι′_{0}}^{∗}B′ ⊳_{η}^{∗} A_{2}

From here we get that

A ⊳_{βι}^{∗} B_{0} and A′ ⊳_{βι}^{∗} B′_{0} where ∥B_{0} ∥= B and ∥B′_{0} ∥= B′

Eta reduction does not change the class of a term. Moving from marked to unmarked terms also does not change the class of a term. Therefore, we get that

Cls(A) = Cls(B_{0}) = Cls(B) = Cls(A_{2}) and
Cls(A_{2}) = Cls(B′) = Cls(B′_{0}) = Cls(A′)
□

Corollary 25 Let Δ ⊢ A : s_{1} and Δ ⊢ B : s_{2} be two derivable judgments. If A =_{βηι} B, then s_{1} = s_{2}.

Lemma 23 If Δ_{1}, Y :C, Δ_{2} ⊢ A : B and Y ∉ FV (Δ_{2}) ∪ FV (A), then there exists a B′ such that Δ_{1}Δ_{2} ⊢ A : B′. (This also implies that B =_{βηι} B′).

Proof The proof is by induction on the structure of the derivation. We will consider only the important cases.

• case fun. We know that

\begin{matrix}Δ_{1}, Y :C, Δ_{2}, X:A ⊢ B : B′ \\ Δ_{1}, Y :C, Δ_{2} ⊢ ΠX:A. B′ : s \end{matrix}

Δ_{1}, Y :C, Δ_{2} ⊢ λX:A. B : ΠX:A. B′

Applying the induction hypothesis to the formation of B

Δ_{1}Δ_{2}, X:A ⊢ B : C′ B′ =_{βηι} C′

By lemma 18 we have that

Δ_{1}Δ_{2}, X:A ⊢ C′ : s which implies
Δ_{1}Δ_{2} ⊢ ΠX:A. C′ : s

Therefore we get that

Δ_{1}Δ_{2} ⊢ λX:A. B : ΠX:A. C′

• case app We know that

\begin{matrix}Δ_{1}, Y :C, Δ_{2} ⊢ A : ΠX:B′. A′ \\ Δ_{1}, Y :C, Δ_{2} ⊢ B : B′ \end{matrix} ; Δ_{1}, Y :C, Δ_{2} ⊢ A B : [B/X]A′

By applying the induction hypothesis we get that

Δ_{1}Δ_{2} ⊢ A : A_{2} and Δ_{1}Δ_{2} ⊢ B : A_{3} where
A_{2} =_{βηι} ΠX:B′. A′ and A_{3} =_{βηι} B′

From lemma 13, A_{2} ⊳_{βι} λY⃗ : A⃗. (ΠX:B′′. A′′) B⃗. Since βι reduction preserves type, and A_{2} is well formed, we have that A_{2} ⊳_{βι} ΠX : B′′. A′′. This implies that A′′ =_{βηι} A′ and B′′ =_{βηι} B′. We also get that A_{3} =_{βηι} B′′. From corollary 25 we get that A_{3} and B′′ have the same sort. By applying the conv rule we get that

Δ_{1}Δ_{2} ⊢ A : ΠX:B′′. A′′ and Δ_{1}Δ_{2} ⊢ B : B′′

Therefore, we get that

Δ_{1}Δ_{2} ⊢ A B : [B/X]A′′
□

As a corollary we now get that

Lemma 24 (Strengthening) If Δ_{1}, Y :C, Δ_{2} ⊢ A : B and Y ∉ FV (Δ_{2}) ∪ FV (A) ∪ FV (B), then Δ_{1}Δ_{2} ⊢ A : B.

Lemma 25 (Subject reduction for η reduction) If Δ ⊢ A : B, and A ⊳_{η} A′ and Δ ⊳_{η} Δ′, then we have that

Δ ⊢ A′ : B Δ′ ⊢ A : B

Proof The interesting case is that of functions. Suppose that

Δ ⊢ λX:A_{1}. A_{2} X : B X ∉ FV (A_{2}) λX:A_{1}. A_{2} X ⊳_{η} A_{2}

From lemma 19 we know that

Δ, X:A_{1} ⊢ A_{2} X : A_{3} B =_{βηι} ΠX:A_{1}. A_{3} Δ ⊢ B : s

Again applying lemma 19 we get that

Δ, X:A_{1} ⊢ A_{2} : ΠY :B′. A′ B′ =_{βηι} A_{1} A_{3} =_{βηι} [X/Y]A′

By applying the conv rule now, we get that Δ, X:A_{1} ⊢ A_{2} : B. By applying lemma 24 we get that Δ ⊢ A_{2} : B. □

Theorem 26 (Subject reduction) If Δ ⊢ A : B, and A ⊳ A′ and Δ ⊳ Δ′, then we have that: Δ ⊢ A′ : B and Δ′ ⊢ A : B.

Proof Follows from lemma 21 and 25. □

D.3 Strong Normalization

The proof is structured as follows:

• We introduce a calculus of pure terms. This is just the pure λ calculus extended with a recursive filtering operator. We do this so that we can operate in a confluent calculus.

• We define a notion of reducibility candidates. Every schema gives rise to a reducibility candidate. We also show how these candidates can be constructed inductively.

• We then define a notion of well constructed kinds which is a weak form of typing.

• We associate an interpretation to each well formed kind. We show that under adequate conditions, this interpretation is a candidate.

• We show that type level constructs such as abstractions and constructors belong to the candidate associated with their kind.

• We show that the interpretation of a kind remains the same under βη reduction.

• We define a notion of kinds that are invariant on their domain – these are kinds whose interpretation remains the same upon reduction.

• We show that kinds formed with large elimination are invariant on their domain.

• From here we can show the strong normalization of the calculus of pure terms. We show that if a type is well formed, then the pure term derived from it is strongly normalizing.

• We then reduce the strong normalization of all well formed terms to the strong normalization of pure terms.

D.3.1 Notation

The syntax for the language is:

(ctxt) Δ ::= · | Δ, X:A
(sort) s ::= Kind | Kscm | Ext
(var) X ::= z | k | t
(ptm) A, B ::= s | X | λX:A. B | A B | ΠX:A. B | Ind(X:Kind){A⃗} | Ctor (i, A) | Elim[A′, B′](A){B⃗}

The proof of strong normalization uses the stratification in the language shown below.

(ctxt) Δ ::= · | Δ, z:Kscm | Δ, k:u | Δ, t:κ
(kscm) u ::= z | Πt:κ. u | Πk:u_{1}. u_{2} | Kind
(kind) κ ::= k | λt:κ_{1}. κ_{2} | κ[τ] | λk:u. κ | κ_{1} κ_{2} | Πt:κ_{1}. κ_{2} | Πk:u. κ | Πz:Kscm. κ | Ind(k:Kind){κ⃗} | Elim[κ′, u](τ){κ⃗}

(type) τ ::= t | λt:κ. τ | τ_{1} τ_{2} | λk:u. τ | τ[κ] | λz:Kscm. τ | τ[u] | Ctor (i, κ) | Elim[κ′, κ](τ′){τ⃗} | Elim[κ′, κ](τ′){τ⃗}

In this section, the types are also referred to as proof terms. We sometimes use I to refer to an inductive definition.

D.3.2 Pure terms

The pure terms are defined as:

(Λ) a, b, c ::= t | a b | λt.a | Co(n) | match t.{a⃗}

The set of reductions on the pure terms are defined as:

(λt.a) b ⊳_{β} [b/t]a
λt.(a t) ⊳_{η} a if t ∉ FV (a)
match t.{a⃗} (Co(i) b⃗) ⊳_{ι} ([match t.{a⃗}/t]a_{i}) b⃗

The translation from types to pure terms is defined as:

|t| = t
|τ_{1} τ_{2} | = |τ_{1} | |τ_{2} |
|τ[κ]| = |τ |
|τ[u]| = |τ |
|λt:κ. τ | = λt.|τ |
|λk:u. τ | = |τ |
|λz:Kscm. τ | = |τ |
|Ctor (n, κ)| = Co(n)

|Elim[κ, κ′](τ){τ⃗}| = (match t.\{\overrightarrow{Υ(κ_{i}, |τ_{i} |, λt_{2}.t t_{2})}\}) |τ | where κ = Ind(k:Kind){κ⃗} and

Υ(k, a_{1}, a_{2}) = a_{1}
Υ(Πt:κ_{1}. κ_{2}, a_{1}, a_{2}) = λt.Υ(κ_{2}, a_{1} t, a_{2})
Υ(Πk:u. κ, a_{1}, a_{2}) = Υ(κ, a_{1}, a_{2})
Υ(Πz:Kscm. κ, a_{1}, a_{2}) = Υ(κ, a_{1}, a_{2})
Υ(ΠX⃗:A⃗. k → κ, a_{1}, a_{2}) =

λt.Υ(κ, a_{1} t (λ|X⃗ |.a_{2} (t |X⃗ |)), a_{2})

Lemma 26 Let τ and τ′ be two well formed types and let t be a type variable. Then |[τ′/t]τ |= [|τ′ | /t] |τ |.

Proof It is a straightforward proof by induction over the structure of τ. □

The following lemma uses Definitions 9 and 7 in Section D.2 and also the definition of Υ from above.

Lemma 27 |Φ_{X,I,B}(κ, τ)|= [match t.\{\overrightarrow{Υ(κ_{i}, |τ_{i} |, λt_{2}.t t_{2})}\}/t]Υ(κ, |τ |, λt_{2}.t t_{2})

Proof The proof is by induction on the fact that κ is the kind of a constructor. □

Lemma 28 For all well formed proof terms τ_{1} and τ_{2}, if τ_{1} ⊳^{i} τ_{2}, then |τ_{1} | ⊳^{j} |τ_{2} | where j ≤ i.

Proof Follows from lemmas 26 and 27. □

D.3.3 Interpretation of schemas

Definition 27 (Arity) We call ground kind schemas arities denoted as arity(u, Kind). The arities are defined with the following grammar:

(kscm) u ::= Kind | Πk:u_{1}. u_{2} | Πt:κ. u

Definition 28 (Schema map) We define a kind schema mapping K as a function mapping kind schema variables z to arities. We also use K, z:u to say that K has been augmented with the mapping z ↦ u.

Definition 29 We define the function ρ(u)_{K} as:

ρ(u)_{K} = ρ_{0}(K(u)) where

• ρ_{0}(Kind) is the set of sets of pure terms;

• ρ_{0}(Πk:u_{1}. u_{2}) is the set of functions from ρ_{0}(u_{1}) to ρ_{0}(u_{2}); and

• ρ_{0}(Πt:κ. u) is the set of functions from Λ to ρ_{0}(u).

Definition 30 For each kind schema u and mapping K, we define in ρ(u)_{K} the relation of partial equivalence written as ≃_{K(u)} as follows:

• for all C and C′ in ρ_{0}(Kind), we have that C ≃_{Kind} C′ ⟺ C = C′;

• for all C and C′ in ρ_{0}(Πk:u_{1}. u_{2}), we have C ≃_{Πk:u_{1}. u_{2}} C′ ⟺ for all C_{1} and C_{2} in ρ_{0}(u_{1}) with C_{1} ≃_{u_{1}} C_{2} we get that C C_{1} ≃_{u_{2}} C′ C_{2}; and

• for all C and C′ in ρ_{0}(Πt: κ. u), we have that C ≃_{Πt:κ. u} C′ ⟺ for all a and b in Λ such that a =_{βηι} b, we get that C a ≃_{u} C′b.

Definition 31 (Invariant) Given C in ρ(u)_{K}, we say that C is invariant ⟺ C ≃_{K(u)} C.

Definition 32 (Neutral terms) A term is called neutral if it has neither of the following forms – λt.a, Co(i) a⃗, or match t.{a⃗}.

Definition 33 We define CR_{0}(Kind) as consisting of all sets C such that:

• if a ∈ C, then a is strongly normalizing;

• if a_{1} ⊳ a_{2} and a_{1} ∈ C, then a_{2} ∈ C; and

• if a is neutral and for all terms a′ such that a⊳a′ and a′ ∈ C, then a ∈ C.

Definition 34 (Candidates) We define CR(u)_{K} as a subset of ρ(u)_{K} as:

CR(u)_{K} = CR_{0}(K(u)) where

• CR_{0}(Kind) is defined as in Definition 33;

• CR_{0}(Πt: κ. u) is the set of invariant elements C belonging to ρ_{0}(Πt:κ. u) such that C Λ ⊂ CR_{0}(u); and

• CR_{0}(Πk:u_{1}. u_{2}) is the set of invariant elements C belonging to ρ_{0}(Πk:u_{1}. u_{2}) such that C (CR_{0}(u_{1})) ⊂ CR_{0}(u_{2}).

Proposition 35 All reducibility candidates are invariant.

Proposition 36 Let (C_{i})_{i∈I} be a family of reducibility candidates of Kind indexed by a set I. Then ∩_{i∈I}C_{i} is a reducibility candidate of schema Kind.

Lemma 29 Let C ∈ ρ(u)_{K}. If C is invariant, then

C ∈ CR(u)_{K} ⟺ ∀C′ ∈ Dom(CR(u)_{K}).C C′ ∈ CR(Kind)_{K}

Proof Straightforward induction over the structure of K(u). □

Definition 37 Let a_{1} be a strongly normalizing term. Then the length of the longest sequence of reductions to a normal form is denoted as ν(a_{1}).

Lemma 30 Let a_{1} and a_{2} be two terms and let C ∈ CR_{0}(Kind) be a reducibility candidate. If a_{2} is strongly normalizing, and if [a_{2}/t]a_{1} ∈ C, then (λt.a_{1}) a_{2} ∈ C.

Proof By induction over ν(a_{1}) + ν(a_{2}). □

Corollary 38 Let a_{1} be a pure term and let C be a reducibility candidate of schema Kind. Let t⃗ and a⃗′ be respectively a sequence of variables and terms of the same length. If for all i, a′_{i} is strongly normalizing, and if [a⃗′/t⃗]a_{1} ∈ C, then (λt⃗.a_{1}) a⃗′ ∈ C.

Lemma 31 For all reducibility candidates C of kind Kind, for all sequences of strongly normalizing a⃗ and b⃗ and for all i less than the length of a⃗, we have that

match t.{a⃗} (Co(i) b⃗) ∈ C ⟺ ([match t.{a⃗}/t]a_{i}) b⃗ ∈ C

Proof Follows by induction over ν(a_{i}) + ν(b_{i}) (for all i). □

Definition 39 (Canonical candidates) Define Can(u)_{K} as:

Can(u)_{K} = Can_{0}(K(u)) where

• Can_{0}(Kind) is the set of all strongly normalizing terms;

• Can_{0}(Πt : κ. u) is the function mapping all pure terms to Can_{0}(u); and

• Can_{0}(Πk : u_{1}. u_{2}) is the function mapping all elements of ρ_{0}(u_{1}) to Can_{0}(u_{2}).

D.3.4 Properties of candidates

In this section, we state some properties of the reducibility candidates. The properties with respect to the union and the intersection of a family of candidates will be used for the inductive constructions of candidates.

Definition 40 (Order over candidates) For each kind schema u and mapping K, we define in ρ(u)_{K} the relation <_{K(u)} as follows:

• for all C and C′ in ρ_{0}(Kind), we have that C <_{Kind} C′ ⟺ C ⊂ C′;

• for all C and C′ in ρ_{0}(Πk:u_{1}. u_{2}), we have C <_{Πk:u_{1}. u_{2}} C′ ⟺ for all C_{1} in ρ_{0}(u_{1}), we get that C C_{1} <_{u_{2}} C′ C_{1}; and

• for all C and C′ in ρ_{0}(Πt: κ. u), we have that C <_{Πt:κ. u} C′ ⟺ for all a in Λ, we get that C a <_{u} C′ a.

Definition 41 For all schemas u and mapping K, for all families of elements in ρ(u)_{K}, we define ⋀_{i∈I} C_{i} as:

• for all C_{i} ∈ ρ_{0}(Kind), ⋀_{i∈I} C_{i} = ∩_{i∈I}C_{i};

• for all C_{i} ∈ ρ_{0}(Πt: κ. u), ⋀_{i∈I} C_{i} = b ∈ Λ ↦ ⋀_{i∈I} C_{i} b; and

• for all C_{i} ∈ ρ_{0}(Πk : u_{1}. u_{2}), ⋀_{i∈I} C_{i} = C′ ∈ ρ_{0}(u_{1}) ↦ ⋀_{i∈I} C_{i} C′.

Lemma 32 Let u be a schema and K a mapping and C_{i} a family of elements of ρ(u)_{K}. Then ∀j ∈ I, ⋀_{i∈I} C_{i} <_{K(u)} C_{j}.

Proof It follows in a straightforward way by induction over the structure of K(u). □

The following two propositions also follow easily by induction over the structure of K(u).

Proposition 42 Let u be a schema and K a mapping and C_{i} a family of elements of ρ(u)_{K}. If all C_{i} are invariants, then the same holds for ⋀_{i∈I} C_{i}.

Proposition 43 Let u be a schema and K a mapping and C_{i} a family of elements of CR(u)_{K}. Then we also have that ⋀_{i∈I} C_{i} ∈ CR(u)_{K}.

Corollary 44 We get that (CR(u)_{K}, <_{K(u)}) is an inf-semi-lattice for all schema u and mapping K. We use min(K(u)) to denote the smallest element.

Definition 45 For all schemas u and mapping K, for all families of elements in ρ(u)_{K}, we define ⋁_{i∈I} C_{i} as:

• for all C_{i} ∈ ρ_{0}(Kind), ⋁_{i∈I} C_{i} = ∪_{i∈I}C_{i};

• for all C_{i} ∈ ρ_{0}(Πt: κ. u), ⋁_{i∈I} C_{i} = b ∈ Λ ↦ ⋁_{i∈I} C_{i} b; and

• for all C_{i} ∈ ρ_{0}(Πk : u_{1}. u_{2}), ⋁_{i∈I} C_{i} = C′ ∈ ρ_{0}(u_{1}) ↦ ⋁_{i∈I} C_{i} C′.

Lemma 33 Let u be a schema and K be a mapping. Let (C_{i})_{i∈I} and (C′_{i})_{i∈I} be two families of elements of ρ(u)_{K}. If for all elements i of I we have that C_{i} ≃_{K(u)} C′_{i}, then we also have that ⋁_{i∈I} C_{i} ≃_{K(u)} ⋁_{i∈I} C′_{i}.

Proof Straightforward induction over the structure of K(u). □

Corollary 46 Let u be a schema and K be a mapping. Let (C_{i})_{i∈I} be a family of elements of ρ(u)_{K}. If all C_{i} are invariant, then ⋁_{i∈I} C_{i} is also invariant.

Lemma 34 Let u be a schema and K be a mapping. Let (C_{i})_{i∈I} be a family of elements of ρ(u)_{K} and C ∈ ρ(u)_{K}. If for all i, C_{i} <_{K(u)} C, then ⋁_{i∈I} C_{i} <_{K(u)} C.

Proof The proof is by induction over the structure of K(u). □

Lemma 35 Let (C_{i})_{i∈I} be a totally ordered family of elements of CR(u)_{K}. Then ⋁_{i∈I} C_{i} ∈ CR(u)_{K}.

Proof The proof is by induction over the structure of K(u). Suppose ⋁_{i∈I} C_{i} = C′.

• K(u) = Kind. We have to make sure that all three conditions in Definition 33 are satisfied. The first two conditions follow obviously. For the third case, assume that a is neutral and for all terms a_{i} such that a ⊳ a_{i}, we have that a_{i} ∈ C′. This implies that a_{i} ∈ C_{j} for some j. Since there are finitely many such C_{j} and they are totally ordered, we can choose a C_{k} among them that contains all the C_{j}s. Since this C_{k} is also a candidate, it contains a. Therefore, a ∈ ⋁_{i∈I} C_{i}.

• K(u) = Πt: κ. u. Since all the C_{i} are invariant, it follows from Definitions 30 and 31 that for a term a ∈ Λ, we have that C_{i} a is invariant. Again from Definition 40, it is clear that the C_{i} a are totally ordered. Also from Corollary 46 we get that ⋁_{i∈I} C_{i} a is invariant. Applying the induction hypothesis we get that ⋁_{i∈I} C_{i} a ∈ CR_{0}(u). From Definition 34, it follows that ⋁_{i∈I} C_{i} ∈ CR_{0}(Πt:κ. u).

• K(u) = Πk:u_{1}. u_{2}. Similar to the previous case.

□

Definition 47 (Schema interpretation) A schema interpretation U is a function that maps a kind variable k to an element of ρ(u)_{K}. We also use U, k : C to say that U has been augmented with the mapping k ↦ C.

Definition 48 (Well formed kinds) Let u be a schema, κ be a kind, K be a mapping, and U be an interpretation. We say that κ is a well formed kind of schema K(u) under K and U iff :

1. κ = k and U(k) = ρ(u)_{K};

2. κ = Πt : κ_{1}. κ_{2} with K(u) =_{βηι} Kind and κ_{1} and κ_{2} are both well constructed of schema Kind under K and U;

3. κ = Πk : u′. κ′ with K(u) =_{βηι} Kind and κ′ is well constructed of schema Kind under K and U, k:ρ(u′)_{K};

4. κ = Πz: Kscm. κ′ with K(u) =_{βηι} Kind and for all u′ such that u′ ∈ arity(u_{1}, Kind), we have that κ′ is well constructed of schema Kind under K, z:u′ and U;

5. κ = κ_{1} κ_{2} if there exists two schemas u_{1} and u_{2} with κ_{2} well constructed of schema K(u_{2}) under K and U, also κ_{1} well constructed of schema K(Πk : u_{2}. u_{1}) under K and U, and ρ(u)_{K} = ρ([κ_{2}/k]u_{1})_{K};

6. κ = κ_{1} τ_{1} if there exists a schema u_{2} and kind κ_{2} such that κ_{1} is well constructed of schema K(Πt:κ_{2}. u_{2}) under K and U and ρ(u)_{K} = ρ([τ_{1}/t]u_{2})_{K};

7. κ = λk : u_{1}. κ_{1} if there exists a u_{2} such that κ_{1} is well constructed of schema K(u_{2}) under K and U, k:ρ(u_{1})_{K} and ρ(u)_{K} = ρ(Πk:u_{1}. u_{2})_{K};

8. κ = λt : κ_{1}. κ_{2} if there exists a u_{2} such that κ_{2} is well constructed of schema K(u_{2}) under K and U and ρ(u)_{K} = ρ(Πt:κ_{1}. u_{2})_{K};

9. κ = Ind(k : Kind){κ⃗} if all κ_{i} are kinds of constructors and well constructed of schema Kind under K and U, k : ρ_{0}(Kind), and ρ(u)_{K} = ρ_{0}(Kind); and

10. κ = Elim[κ′, u′](τ){κ⃗} if κ′ = Ind(k : Kind){κ⃗′}, and κ′ is well constructed of schema Kind under K and U, also u′ is a schema and K(u) =_{βηι} u′, and κ_{i} is well constructed of schema K(Ψ_{k,κ′}(κ′_{i}, u′)) under K and U.

Definition 49 We define compatible mappings and interpretation as:

1. A mapping K is compatible with a context Δ if for all z ∈ Δ, we have K(z) = arity(u, Kind).

2. An interpretation U is compatible with a context Δ and a compatible mapping K if for all pairs (k, u) ∈ Δ, we have U(k) ∈ ρ(u)_{K}.

Lemma 36 If Δ ⊢ κ : u, then for all compatible K and U, we have that κ is well constructed of schema K(u).

Proof By induction over the structure of κ. □

D.3.5 Inductive constructions

Consider an increasing function F in ρ_{0}(Kind) for the order <_{Kind}. Denote the smallest element of ρ_{0}(Kind) as ⊥. Since ρ_{0}(Kind) is closed under ∩, and (ρ_{0}(Kind), <_{Kind}) is an inf-semi-lattice, the function F has a least fixed point (lfp). We will construct this least fixed point inductively. We first define the transfinite iteration of F.

Definition 50 Let C ∈ ρ_{0}(Kind) and o be an ordinal. We define the iteration of order o of F over C as:

• F^{0}(C) = C;

• F^{o+1}(C) = F (F^{o}(C)); and

• F^{lim(U)} = ∪_{o∈U}F^{o}(C).

Lemma 37 Let o be an ordinal; we have F^{o}(⊥) <_{Kind} lfp(F).

Proof The proof is by induction over o. If o = 0, then it follows immediately. Otherwise,

• o = o′ + 1 Then we have that F^{o}(⊥) = F (F^{o′}(⊥)). By the induction hypothesis, we get that F (F^{o′}(⊥)) <_{Kind} F (lfp(F)). This implies that F (F^{o′}(⊥)) <_{Kind} lfp(F).

• o = lim(U) Follows immediately from the induction hypothesis and lemma 34.

□

Remark 51 Since we do not consider the degenerate case of F (⊥) = ⊥, it follows from lemma 37 that for some ordinal o, we have that lfp(F) = F^{o}(⊥).

Lemma 38 Suppose S is a subset of ρ_{0}(Kind) satisfying:

• if (C_{i})_{i∈I} is a totally ordered family of elements of S, then ∪_{i∈I}C_{i} ∈ S;

• F (⊥) ∈ S; and

• for all C in S, F (C) ∈ S.

Then lfp(F) ∈ S.

Proof Follows from the fact that lfp(F) = F^{o}(⊥) for some ordinal o. □

Definition 52 Let a ∈ lfp(F). We define deg(a) as the smallest ordinal such that a ∈ F^{deg(a)}(⊥).

Definition 53 To all a ∈ lfp(F), we associate pred(a) defined as F^{deg(a)−1}(⊥).

Lemma 39 For all a, deg(a) is an ordinal successor.

Proof Suppose it is the limit of the set U. From Definition 50, there exists some o ∈ U for which a ∈ F^{o}(⊥). This leads to a contradiction. □

Definition 54 (Partial order) Suppose C and C′ are two elements of CR_{0}(Kind). We say that C <_{F} C′ if C = F^{o}(⊥) and C′ = F^{o′}(⊥), and o < o′.

D.3.6 Interpretation of kinds

In this section we interpret kinds as members of reducibility candidates. First we augment the schema interpretation

Definition 55 We augment U so that it maps a kind variable to an element of ρ(u)_{K}, and a type variable to a pure term a.

Definition 56 We denote the interpretation of a type τ as C_{U}^{K}(τ). To form this, we first construct the corresponding pure term |τ | and then substitute the type variables by the corresponding pure terms in U. This is equivalent to U(|τ |).

Definition 57 (Interpreting kinds) Consider a kind κ, a schema u, a mapping K, and an interpretation U. Suppose κ is well constructed of schema K(u) under K and U. We define by recursion on κ:

1. C_{U}^{K}(k) = U(k)

2. C_{U}^{K}(Πt : κ_{1}. κ_{2}) = {a ∈ Λ, ∀a_{1} ∈ C_{U}^{K}(κ_{1}), a a_{1} ∈ C_{U,t:a_{1}}^{K}(κ_{2})}

3. C_{U}^{K}(Πk:u_{1}. κ_{1}) = ∩_{C∈CR(u_{1})_{K}}C_{U,k:C}^{K}(κ_{1})

4. C_{U}^{K}(Πz:Kscm. κ_{1}) = ∩_{u_{1}∈arity(u,Kind)}C_{U}^{K,z:u_{1}}(κ_{1})

5. C_{U}^{K}(κ_{1} τ) = C_{U}^{K}(κ_{1}) C_{U}^{K}(τ)

6. C_{U}^{K}(κ_{1} κ_{2}) = C_{U}^{K}(κ_{1}) C_{U}^{K}(κ_{2})

7. C_{U}^{K}(λt:κ_{1}. κ_{2}) = a ∈ Λ ⟼ C_{U,t:a}^{K}(κ_{2})

8. C_{U}^{K}(λk:u_{1}. κ_{1}) = C ∈ CR(u_{1})_{K} ⟼ C_{U,k:C}^{K}(κ_{1})

9. C_{U}^{K}(Ind(k: Kind){κ⃗}) = the least fixed point of the function F from ρ_{0}(Kind) to ρ_{0}(Kind) defined as : for all S ∈ ρ_{0}(Kind), for all C′ in CR(I → Kind)_{K} (where I = Ind(k : Kind){κ⃗}), for all sequences of pure terms b_{i}, with for all i,

b_{i} ∈ C_{U,k:S,A′:C′,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′))

F (S) is the union of min(Kind) with the set of pure terms a such that

(match t.\{\overrightarrow{C_{U,a_{i}:b_{i}}^{K}(Υ(κ_{i}, a_{i}, λt_{2}.t t_{2}))}\}) a ∈ C′ a
10. C_{U}^{K}(Elim[κ, u](τ){κ⃗′}) = G(C_{U}^{K}(κ))

where κ = Ind(k : Kind){κ⃗} is well constructed of schema Kind under K and U and G(C) ∈ ρ(u)_{K} is defined for all C ∈ dom(<_{κ}) as follows (<_{κ} is the order induced by the inductive definition κ):

• If C_{U}^{K}(τ) has a normal form b = Co(i) a⃗ such that b ∈ C

G(C) = C_{U,t_{1}:G(pred(b))}^{K}(Φ_{k,I,t_{1}}(κ_{i}, κ′_{i})) (a⃗)

• Can(u)_{K} otherwise

Lemma 40 The function F in Definition 57.9 is monotonic.

Proof We must prove that if C_{1} <_{Kind} C_{2}, then

C_{U,k:C_{2},A′:C′,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′)) <_{Kind} C_{U,k:C_{1},A′:C′,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′))

The proof is by induction on the fact that κ_{i} is the kind of a constructor.

• If κ_{i} = k, then both sides reduce to C′ Co(i).

• If κ_{i} = ΠX:A_{1}. A_{2}, then it follows directly from the induction hypothesis and because k does not occur in A_{1}.

• If κ_{i} = ΠX⃗:A⃗. k → A_{2}, then

\begin{matrix}ζ_{k,I}(κ_{i}, A′, B′) = \\ ΠZ:(ΠX⃗:A⃗. k). ΠX⃗′:A⃗. (A′ (Z X⃗′)) → ζ_{k,I}(A_{2}, A′, B′ Z) \end{matrix}

Suppose U′ = U, k : C′′, A′ : C′, B′ : Co(i) where C′′ is either C_{1} or C_{2}. The required set is then

a ∈ Λ, such that ∀a_{1} ∈ C_{U′}^{K}(ΠX⃗:A⃗. k), ∀a_{2} ∈ C_{U′,Z:a_{1}}^{K}(ΠX⃗′:A⃗. A′ (Z X⃗′)) a a_{1} a_{2} ∈ C_{U′,Z:a_{1}}^{K}(ζ_{k,I}(A_{2}, A′, B′ Z))

The set of a_{1} and a_{2} is larger for the LHS. By the induction hypothesis, the result a a_{1} a_{2} must occur in a smaller set for the LHS. The required result follows from this.

□

Remark 58 The previous lemma ensures that the interpretation of an inductive type sets up a well defined order. This ensures that the interpretation of large elimination (Definition 57.10) is well formed.

We get a bunch of substitution lemmas. The proof for each of these is similar and follows directly by induction over the structure of κ. We state them below:

Proposition 59 Let κ be a well constructed kind of schema u under K and U. Let t be a type variable, and τ a type. We have that

C_{U}^{K}([τ/t]κ) = C_{U,t:C_{U}^{K}(τ)}^{K}(κ)

Proposition 60 Let κ be a well constructed kind of schema u under K and U. Let k be a kind variable and κ_{1} a kind such that κ_{1} is well constructed under K and U of the same schema as U(k). We have that

C_{U}^{K}([κ_{1}/k]κ) = C_{U,k:C_{U}^{K}(κ_{1})}^{K}(κ)

Proposition 61 Let κ be a well constructed kind of schema u under K and U. Let z be a schema variable, and u_{1} be a schema such that K(u_{1}) is an arity. We have that

C_{U}^{K}([u_{1}/z]κ) = C_{U}^{K,z:K(u_{1})}(κ)

D.3.7 Candidate interpretation of kinds

Definition 62 We say that U and U′ are equivalent interpretations if for all k, we have that U(k) ≃ U′(k) and for all t we have that U(t) =_{βηι} U′(t).

Lemma 41 Let u be a schema, K be a mapping, and U and U′ be two equivalent interpretations. Suppose κ is well constructed of schema K(u) under K and both U and U′. Then C_{U}^{K}(κ) ≃_{K(u)} C_{U′}^{K}(κ).

Proof The proof is by induction over the structure of κ. Most of the cases follow directly from the induction hypothesis.

• κ = Elim[κ′, u](τ){κ⃗′}. Here κ′ = Ind(k : Kind){κ⃗}. First note that C_{U}^{K}(κ′) = C_{U′}^{K}(κ′). Therefore, the function F whose lfp generates the inductive definition is the same. Moreover, C_{U}^{K}(τ) =_{βηι} C_{U′}^{K}(τ). Since the set of pure terms is confluent, C_{U}^{K}(τ) and C_{U′}^{K}(τ) have the same normal form. We can now do induction on the structure of κ_{i} to prove that

C_{U,t_{1}:G(pred(b))}^{K}(Φ_{k,I,t_{1}}(κ_{i}, κ′_{i})) ≃
C_{U′,t_{1}:G(pred(b))}^{K}(Φ_{k,I,t_{1}}(κ_{i}, κ′_{i}))

□

Lemma 42 Let K be a mapping, U a candidate interpretation, κ be a kind and u be a schema such that κ is a well constructed kind of schema K(u). Then C_{U}^{K}(κ) ∈ CR(u)_{K}.

Proof The proof is by induction over the structure of κ. Most of the cases follow in a direct way.

• κ = Ind(k : Kind){κ⃗}. We will use lemma 38 to prove this. For S ∈ CR_{0}(Kind), the first condition is satisfied by lemma 35.

– Suppose S = ⊥. If none of the branches is recursive then the function F is a constant function and the proof is similar to the non-bottom case. Suppose the ith branch is recursive. Then it is easy to see that the b_{i} defined as:

b_{i} ∈ C_{U,k:⊥,A′:C,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′))

includes the set of all terms, including non-normalizing ones. Therefore, there are no terms a that would satisfy the condition that:

(match t.\{\overrightarrow{C_{U,a_{i}:b_{i}}^{K}(Υ(κ_{i}, a_{i}, λt_{2}.t t_{2}))}\}) a ∈ C a

This implies that F (⊥) = ⊥ and we know that ⊥ ∈ CR_{0}(Kind).

– Consider any other S. We will show that F (S) satisfies the conditions in Definition 33 and hence belongs to CR_{0}(Kind). F (S) is defined as the union of min(Kind) with the set of pure terms a such that

(match t.\{\overrightarrow{C_{U,a_{i}:b_{i}}^{K}(Υ(κ_{i}, a_{i}, λt_{2}.t t_{2}))}\}) a ∈ C a

Since C is a candidate, the terms a must be strongly normalizing. To see that the set is closed under reduction, suppose a ⊳ a′. Since C is a candidate we have that (match t.{… }) a′ ∈ C a. Moreover, we have that C a = C a′. Therefore, a′ is also in the generated set. Suppose a is a neutral term and for all a′ such that a ⊳ a′, we have that a′ belongs to this set. We have to prove that a belongs to this set. This implies that we must prove:

(match t.\{\overrightarrow{C_{U,a_{i}:b_{i}}^{K}(Υ(κ_{i}, a_{i}, λt_{2}.t t_{2}))}\}) a ∈ C a

Since a is a neutral term, the above term does not have a redex at the head. From the induction hypothesis, we get that C_{U,k:S,A′:C,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′)) is a candidate and therefore closed under reduction. Moreover, the b_{i} are strongly normalizing. We can now consider all possible redices and prove by induction over ν(b_{i}) that the above condition is satisfied.

• κ = Elim[κ′, u](τ){κ⃗′} where κ′ = Ind(k: Kind){κ⃗}. First note that C_{U}^{K}(κ′) is a candidate by induction and gives rise to a well founded order on CR_{0}(Kind). We will do induction on this order. Suppose C_{U}^{K}(κ) = G(C_{U}^{K}(κ′)). We will show that for all sets S belonging to the order generated by κ′, and for all pure terms b, we have that G(S) ∈ CR(u)_{K}. For the nonrecursive case, the proof is immediate. For the recursive case, consider C_{U,t_{1}:G(pred(b))}^{K}(Φ_{k,κ′,t_{1}}(κ_{i}, κ′_{i})). Note that pred(b) belongs to the same order. The required result follows now by doing induction over the structure of κ_{i} and applying the induction hypothesis to G(pred(b)).

□

Definition 63 Suppose Δ is a context and K and U are a mapping and an interpretation. We say that K and U are adapted to Δ if:

• ∀z ∈ Δ, we have that K(z) is an arity and · ⊢ K(z) : Kscm.

• ∀k ∈ Δ, we have that U(k) ∈ CR(Δ(k))_{K}.

• ∀t ∈ Δ, we have that U(t) ∈ C_{U}^{K}(Δ(t)).

D.3.8 Interpretation of abstractions

We get a bunch of lemmas that state that an abstraction at the type level belongs to the corresponding kind. The proof of each of these lemmas is straightforward and follows in a similar way. We will show the proof for only one of the lemmas.

Lemma 43 Let Δ ⊢ λt:κ. τ : Πt:κ. κ_{1} be a judgment and K and U be a mapping and a candidate interpretation adapted to Δ. We have C_{U}^{K}(λt:κ. τ) ∈ C_{U}^{K}(Πt:κ. κ_{1}) if and only if for all pure terms a ∈ C_{U}^{K}(κ), we have that C_{U,t:a}^{K}(τ) ∈ C_{U,t:a}^{K}(κ_{1}).

Lemma 44 Let Δ ⊢ λk:u. τ : Πk:u. κ be a judgment and K and U be a mapping and a candidate interpretation adapted to Δ. We have C_{U}^{K}(λk:u. τ) ∈ C_{U}^{K}(Πk:u. κ) if and only if for all reducibility candidates C ∈ CR(u)_{K} we have that C_{U,k:C}^{K}(τ) ∈ C_{U,k:C}^{K}(κ) .

Lemma 45 Let Δ ⊢ λz:Kscm. τ : Πz:Kscm. κ be a judgment and K and U be a mapping and a candidate interpretation adapted to Δ. We have C_{U}^{K}(λz:Kscm. τ) ∈ C_{U}^{K}(Πz:Kscm. κ) if and only if for all u ∈ arity(u′, Kind) we have that C_{U}^{K}(τ) ∈ C_{U}^{K,z:u}(κ).

Proof By definition C_{U}^{K}(λz : Kscm. τ) = C_{U}^{K}(τ). Similarly C_{U}^{K}(Πz : Kscm. κ) = ∩_{u_{1}∈arity(u,Kind)}C_{U}^{K,z:u_{1}}(κ). The if part follows directly from the definition.

For the only if, suppose that C_{U}^{K}(τ) ∈ C_{U}^{K,z:u}(κ) for all arities u. This implies that C_{U}^{K}(τ) ∈ ∩_{u_{1}∈arity(u,Kind)}C_{U}^{K,z:u_{1}}(κ). This implies that C_{U}^{K}(τ) ∈ C_{U}^{K}(Πz:Kscm. κ). □

D.3.9 Interpretation of weak elimination

For this section κ = Ind(k : Kind){κ⃗}. Suppose also that C ∈ CR(κ → Kind)_{K} and τ_{i} ∈ C_{U,A′:C,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′)).

Lemma 46 Suppose a ∈ C_{U}^{K}(κ). We have then

(match t.\{\overrightarrow{Υ(κ_{i}, τ_{i}, λt_{2}.t t_{2})}\}) a ∈ C a

Proof Follows immediately from the definition of C_{U}^{K}(κ). □

Lemma 47 Let Δ ⊢ Elim[κ, κ_{1}](τ){τ⃗′} : κ_{1} be a derivable judgment where κ_{1} is a kind. Suppose K is a mapping and U is a candidate interpretation adapted to Δ. If C_{U}^{K}(τ) ∈ C_{U}^{K}(κ) and C_{U}^{K}(τ′_{i}) ∈ C_{U}^{K}(ζ_{k,I}(κ_{i}, κ_{1}, Ctor (i, κ))), then we have

C_{U}^{K}(Elim[κ, κ_{1}](τ){τ⃗′}) ∈ C_{U}^{K}(κ_{1})

Proof Follows now from the previous lemma. □

D.3.10 Interpretation of constructors

For this section, suppose I = κ = Ind(k : Kind){κ⃗}. Also, suppose C ∈ CR(I → Kind)_{K}.

Lemma 48 For all i, Co(i) ∈ C_{U}^{K}(κ_{i}).

Proof We know that κ_{i} is of the form ΠX⃗: A⃗. k. Suppose B⃗ ∈ C_{U,k:C_{U}^{K}(I)}^{K}(X⃗:A⃗). Then we need to prove that Co(i) B⃗ ∈ C_{U}^{K}(I). This means that we need to prove that

(match t.\{\overrightarrow{Υ(κ_{i}, a_{i}, λt_{2}.t t_{2})}\}) (Co(i) B⃗) ∈ C (Co(i) B⃗)

where a_{i} belongs to the appropriate candidate. This implies that we need to prove that

Υ(κ_{i}, a_{i}, λt_{2}.match t.{… } t_{2}) B⃗ ∈ C (Co(i) B⃗)

This follows directly by an induction over the structure of κ_{i}. □

D.3.11 Invariance under β reduction

In this section, we show that the interpretation of kinds remains invariant under β reduction.

Lemma 49 Let κ be a well constructed kind of schema u under a mapping K and candidate interpretation U. If κ ⊳_{β} κ′, then κ′ is well constructed of schema u under K and U, and C_{U}^{K}(κ) = C_{U}^{K}(κ′).

Proof The proof is by induction over the structure of κ. Most of the cases follow directly from the induction hypothesis. We will only consider β reductions at the head.

• κ = (λt:κ_{1}. κ_{2}) τ. By definition,

C_{U}^{K}((λt:κ_{1}. κ_{2}) τ) = C_{U}^{K}(λt:κ_{1}. κ_{2}) C_{U}^{K}(τ)

Again by definition this is equal to C_{U,t:C_{U}^{K}(τ)}^{K}(κ_{2}). By propo-

sition 59 this is equal to C_{U}^{K}([τ/t]κ_{2})

• κ = (λk:u_{1}. κ_{1}) κ_{2}. By definition,

C_{U}^{K}((λk:u_{1}. κ_{1}) κ_{2}) = C_{U}^{K}(λk:u_{1}. κ_{1}) C_{U}^{K}(κ_{2})

By lemma 42 we have that C_{U}^{K}(κ_{2}) ∈ CR(u_{1})_{K}. Therefore, we get that

C_{U}^{K}((λk:u_{1}. κ_{1}) κ_{2}) = C_{U,k:C_{U}^{K}(κ_{2})}^{K}(κ_{1})

By proposition 60 this is equal to C_{U}^{K}([κ_{2}/k]κ_{1}).

□

D.3.12 Invariance under η reduction

In this section, we show that the interpretation remains the same under η reduction. The unmarked terms ∥ κ ∥ are defined in Section D.2.1.

Lemma 50 Let κ be a well constructed kind of schema u under a mapping K and candidate interpretation U. If κ ⊳_{η} κ′, then κ′ is well constructed of schema u under K and U, and C_{U}^{K}(κ) = C_{U}^{K}(κ′).

Proof The proof is again by induction over the structure of κ. We will consider only the cases where the reduction occurs at the head.

• κ = λt:κ_{1}. (κ_{2} t). By definition C_{U}^{K}(κ) is equal to:

a ∈ Λ ⟼ C_{U,t:a}^{K}(κ_{2}) C_{U,t:a}^{K}(t)

Since t does not occur free in κ_{2}, this is equivalent to

a ∈ Λ ⟼ C_{U}^{K}(κ_{2}) a

Since a does not occur free now in C_{U}^{K}(κ_{2}), we get that this is equivalent to C_{U}^{K}(κ_{2}). Note from Definition 34 that the domain of C_{U}^{K}(κ_{2}) is Λ.

• κ = λk:u_{1}. (κ_{2} k). By definition C_{U}^{K}(κ) is equal to:

C ∈ CR(u_{1})_{K} ⟼ C_{U,k:C}^{K}(κ_{2}) C_{U,k:C}^{K}(k)

Since k does not occur free in κ_{2}, this is equivalent to

C ∈ CR(u_{1})_{K} ⟼ C_{U}^{K}(κ_{2}) C

Since C does not occur free now in C_{U}^{K}(κ_{2}), we get that this is equivalent to C_{U}^{K}(κ_{2}). Note from Definition 34 that the domain of C_{U}^{K}(κ_{2}) is CR(u_{1})_{K}.

□

Lemma 51 For all well constructed kinds κ of schema u under K and U, we have C_{U}^{K}(κ) = C_{U}^{K}(∥κ∥).

Proof Follows from the fact that κ =_{βη}∥κ∥. □

D.3.13 Invariance under ι reduction

In this section we essentially show that interpretation remains the same under large elimination.

Lemma 52 Let Elim[κ, u](τ){κ⃗′} be well constructed of schema K(u) under K and U. Suppose κ = Ind(k:Kind){κ⃗}. Suppose G is the function used for the interpretation of the large elimination. If C_{U}^{K}(τ) ∈ C_{U}^{K}(κ), then for all C ∈ CR_{0}(Kind) with C_{U}^{K}(τ) ∈ C, we have that G(C_{U}^{K}(κ)) = G(C).

Proof The proof is immediate. □

Lemma 53 Suppose I = κ = Ind(k:Kind){κ⃗}. Suppose the constructors of I are all small. Suppose the mth constructor of I has the form ΠY⃗ :B⃗. k and we have a sequence of terms b⃗ such that Co(m) b⃗ ∈ C_{U}^{K}(I). Then we have that b_{i} ∈ C_{U,∀k<i.Y_{k}:b_{k},k:pred(Co(m) b⃗)}^{K}(B_{i}).

Proof We can have two cases.

• pred(Co(m) b⃗) ≠ ⊥ This implies that pred(Co(m) b⃗) ∈ CR_{0}(Kind). Suppose S = C_{U,∀k<i.Y_{k}:b_{k},k:pred(Co(m) b⃗)}^{K}(B_{i}). Then we have that S is a candidate of schema Kind. Suppose also that C′ belongs to CR(I → Kind)_{K} and maps elements in the domain of I → Kind to S. Then for all indices i′, we have that C_{U,k:pred(Co(m) b⃗),A′:C′}^{K}(ζ_{k,I}(κ_{i′}, A′, Ctor (i′, I))) is a reducibility candidate of Kind. To prove the lemma we need to show that if for all indices i

τ_{i} ∈ C_{U,k:pred(Co(m) b⃗),A′:C′}^{K}(ζ_{k,I}(κ_{i}, A′, Ctor (i, I)))

then we have that Φ_{k,I,B′}(κ_{m}, τ_{m}) can reduce to b_{i} by a head reduction. To have this, for the indices i ≠ m choose τ_{i} as some variable. For τ_{m} choose the term that returns the ith argument of the constructor.

• pred(Co(m) b⃗) = ⊥ We can show that the constructors now are not recursive. Hence k does not occur free in any of the B_{i}s. The proof for the previous case can be reused here.

□

Lemma 54 Let Δ ⊢ Elim[κ, u](τ){κ⃗′} : u be a derivable judgment. Let K be a mapping and U be an interpretation adapted to Δ. Suppose I = κ = Ind(k:Kind){κ⃗}. Suppose C_{U}^{K}(τ) ∈ C_{U}^{K}(κ) and τ ⊳^{∗} Ctor (i, κ) A⃗. Also suppose B′ = λt:I. Elim[κ, u](t){κ⃗′}. We then have that C_{U}^{K}(Elim[κ, u](τ){κ⃗′}) = C_{U}^{K}(Φ_{k,I,B′}(κ_{i}, κ′_{i}) (A⃗)).

Proof Let G be the function used for interpreting large elimination. Suppose Co(i) a⃗ is the normal form of C_{U}^{K}(τ). Then given the assumptions we have that:

C_{U}^{K}(Elim[κ, u](τ){κ⃗′}) =
C_{U,B′:G(pred(Co(i) a⃗))}^{K}(Φ_{k,I,B′}(κ_{i}, κ′_{i})) (a⃗)

We therefore have to prove that

C_{U,B′:G(pred(Co(i) a⃗))}^{K}(Φ_{k,I,B′}(κ_{i}, κ′_{i})) (a⃗) =

C_{U}^{K}(Φ_{k,I,B′}(κ_{i}, κ′_{i}) (A⃗))

• κ_{i} = k it follows directly.

• κ_{i} = Πt:κ_{1}. κ_{2} We have to prove that

C_{U,B′:G(pred(Co(i) a⃗)),t:a_{1}}^{K}(Φ_{k,I,B′}(κ_{2}, κ′_{i} t)) (a_{2..n}) =

C_{U,t:a_{1}}^{K}(Φ_{k,I,B′}(κ_{2}, κ′_{i} t) (A_{2..n}))

Applying the induction hypothesis leads to the result.

• κ_{i} = Πt⃗:κ⃗. k → κ_{2} The LHS becomes

C_{U′}^{K}(Φ_{k,I,B′}(κ_{2}, κ′_{i}t(λY⃗ :κ⃗. B′(tY⃗)))) (a_{2..n})
where U′ = U, B′ : G(pred(Co(i) a⃗)), t : a_{1}

By lemma 53, a_{1} belongs to C_{U,k:pred(Co(i) a⃗)}^{K}(Πt⃗:κ⃗. k). This implies that a_{1} Y⃗ ∈ pred(Co(i) a⃗). Moreover, by lemma 52 G(pred(Co(i) a⃗))(a_{1} Y⃗) is equal to G(C_{U}^{K}(κ))(a_{1} Y⃗) and which is in turn equal to C_{U}^{K}(Elim[κ, u](A_{1} Y⃗){κ⃗′}). The required result follows directly from here by performing one head reduction on the RHS and applying the induction hypothesis.

□

D.3.14 Kinds invariant on their domain

Definition 64 Let Δ ⊢ κ : u be a derivable judgment and K and U be a mapping and an interpretation adapted to Δ. We say (κ, u, Δ, K, U) is invariant if:

• u = Kind and for all κ′ such that κ ⊳^{∗} κ′, we have that C_{U}^{K}(κ) = C_{U}^{K}(κ′);

• u = Πt:κ_{1}. u_{1} then for all derivable judgments Δ ⊢ τ : κ_{1} and C_{U}^{K}(τ) ∈ C_{U}^{K}(κ_{1}), we have that (κ τ, [τ/t]u_{1}, Δ, K, U) is invariant;

• u = Πk: u_{1}. u_{2} then for all derivable judgments Δ ⊢ κ_{1} : u_{1}, we have that (κ κ_{1}, [κ_{1}/k]u_{2}, Δ, K, U) is invariant.

• u = z and we have that (K(κ), K(u), K(Δ), K, U) is invariant.

Lemma 55 Let Δ ⊢ κ_{1} : Kind and Δ ⊢ κ_{2} : Kind be two derivable judgments and K and U be a mapping and an interpretation adapted to Δ. If (κ_{1}, Kind, Δ, K, U) and (κ_{2}, Kind, Δ, K, U) are invariant and κ_{1} =_{βηι} κ_{2}, then C_{U}^{K}(κ_{1}) = C_{U}^{K}(κ_{2}).

Proof We know that there exists a B such that ∥ κ_{1} ∥ ⊳^{∗}B and ∥κ_{2} ∥ ⊳^{∗}B. This implies that there exists a κ′_{1} and a κ′_{2} (lemma 13 and 12) such that κ_{1} ⊳_{βι} κ′_{1} and ∥κ′_{1} ∥ ⊳_{η}^{∗}B. Similarly, κ_{2} ⊳_{βι} κ′_{2} and ∥κ′_{2} ∥ ⊳_{η}^{∗}B. From here we get that

C_{U}^{K}(κ_{1}) = C_{U}^{K}(κ′_{1}) = C_{U}^{K}(B) = C_{U}^{K}(κ′_{2}) = C_{U}^{K}(κ_{2})
□

Proposition 65 If ([τ/t]κ, u, Δ, K, U) is invariant, and also Δ ⊢ (λt:κ_{1}. κ) τ : u, then ((λt:κ_{1}. κ) τ, u, Δ, K, U) is invariant.

D.3.15 Interpretation of large elimination

Lemma 56 Let Δ ⊢ Elim[κ, u](τ){κ⃗′} : u be a judgment. Suppose I = κ = Ind(k:Kind){κ⃗}. Let K and U be a mapping and an interpretation adapted to Δ. Suppose

1. C_{U}^{K}(τ) ∈ C_{U}^{K}(κ).

2. for all i, (κ′_{i}, Ψ_{k,I}(κ_{i}, u), Δ, K, U) is invariant.

Then we have that (Elim[κ, u](τ){κ⃗′}, u, Δ, K, U) is invariant.

Proof Suppose κ_{1} = Elim[κ, u](τ){κ⃗′}. Suppose we are given a sequence of terms A⃗ of the proper type so that κ_{1} A⃗ is in Kind. To show the invariance, we have to show that if κ_{1} A⃗ ⊳^{∗} κ_{2}, then C_{U}^{K}(κ_{1} A⃗) = C_{U}^{K}(κ_{2}). We will reason by induction on C_{U}^{K}(τ) over the order defined by I.

• If the term C_{U}^{K}(τ) can not be reduced to a term of the form Co(i)a⃗, then it is minimal with respect to the order defined by I. Then κ_{2} is necessarily of the form Elim[κ′, u′](τ′){κ⃗′′} A⃗′ and we have that the interpretation of both κ_{1} A⃗ and κ_{2} is Can_{0}(Kind).

• Suppose the term C_{U}^{K}(τ) can be reduced to a term of the form Co(i)a⃗, but τ is not reduced to a term of the form Ctor (i, I)C⃗. Then κ_{2} is again of the form Elim[κ′′′, u′](τ′){κ⃗′′} A⃗′. By definition, we have that

\begin{matrix}B_{1} = C_{U}^{K}(κ_{1} A⃗) = C_{U,t⃗:a⃗}^{K}(Φ_{k,I,B′}(κ_{i}, κ′_{i}) (t⃗)A⃗) \\ B_{2} = C_{U}^{K}(κ_{2}) = C_{U,t⃗:a⃗}^{K}(Φ_{k,I′,B′′}(κ⃗′′′_{i}, κ⃗′′_{i}) (t⃗)A⃗′) \end{matrix}

where B′ = λY : I. Elim[κ, u](τ){κ⃗′}, and B′′ = λY : I′. Elim[κ′′′, u′](τ′){κ⃗′′}. It is evident that B_{2} is a reduct of B_{1}, and therefore we need to prove that (B_{1}, Kind, Δ, K, U) is invariant. This follows by an induction over the structure of κ_{i} and by using the condition 2. The non-recursive cases follow directly. For the recursive case, we use lemma 53 to show that B′ is applied to a smaller argument with respect to the order defined by I.

• We are left with the case when τ reduces to a term of the form Ctor (i, I)C⃗. In going from κ_{1} A⃗ to κ_{2}, we will now have a ι reduction. The sequence of reductions is now

κ_{1} A⃗ ⊳^{∗} Elim[κ, u](Ctor (i, I)A⃗){κ⃗′}
⊳_{ι} (Φ_{k,I,κ′_{i}}(κ_{i}, B′) (B⃗))A⃗
⊳^{∗} κ_{2}

The first reduction does not change the interpretation since we are reducing only a type. By lemma 54, the second does not change the interpretation. Finally, as above, we can prove that the result of the ι reduction is invariant over Kind.

□

D.3.16 Instantiation of contexts

Definition 66 Let Δ be a well formed context. Let Θ be a context and ϕ be a mapping from variables to terms such that ∀X ∉ Δ, ϕ(X) = X.

We say that (Θ, ϕ) is an instantiation of Δ if for all variables X ∈ Δ, we have that Θ ⊢ ϕ(X) : ϕ(Δ(X)).

Lemma 57 Let Δ ⊢ A : B be a derivable judgment and (Θ, ϕ) an instantiation of Δ. Then Θ ⊢ ϕ(A) : ϕ(B).

Proof By induction over the structure of A. □

Definition 67 (Adapted instantiation) We say that an instantiation (Θ, ϕ) is adapted to a context Δ if:

• for all t ∈ Δ, ϕ(t) ∈ C_{Can_{0}(Θ)}^{∅}(ϕ(Δ(t)));

• for all k ∈ Δ, (ϕ(k), ϕ(Δ(k)), Θ, ∅, Can_{0}(Θ)) is invariant;

• for all z ∈ Δ, (ϕ(z), Kscm, Θ, ∅, Can_{0}(Θ)) is invariant and ϕ(z) is an arity.

Definition 68 Suppose Δ ⊢ κ : u is a derivable judgment. We say that all instantiations of (κ,u, Δ) are invariant if for all instantiations (Θ, ϕ) adapted to Δ and for all interpretations U adapted to Θ, we have that (ϕ(κ), ϕ(u), Θ, ∅, U) is invariant.

D.3.17 Kind schema invariant on their domain

Definition 69 Let Δ ⊢ u : Kscm be a derivable judgment and K and U be a mapping and an interpretation adapted to Δ. We say that (u, Kscm, Δ, K, U) is invariant:

• if u = Kind, then (u, Kscm, Δ, K, U) is invariant;

• if u = Πt : κ_{1}. u_{1}, then it is invariant if and only if (κ_{1}, Kind, Δ, K, U) is invariant and for all terms τ such that Δ ⊢ τ : κ_{1} is derivable and C_{U}^{K}(τ) ∈ C_{U}^{K}(κ_{1}), we have that ([τ/t]u_{1}, Kscm, Δ, K, U) is invariant; • if u = Πk : u_{1}. u_{2}, then it is invariant if and only if

(u_{1}, Kscm, Δ, K, U) is invariant, and for all kinds κ such that Δ ⊢ κ : u_{1} is derivable and (κ, u_{1}, Δ, K, U) is invariant, we have that ([κ/k]u_{2}, Kscm, Δ, K, U) is invariant;

• if u = z, then it is invariant iff (K(z), Kscm, Δ, K, U) is invariant.

Lemma 58 Let Δ ⊢ κ : u and Δ ⊢ u′ : Kscm be derivable judgments. Let K and U be a mapping and an interpretation adapted to Δ. Suppose u =_{βηι} u′, and (u, Kscm, Δ, K, U) and (u′, Kscm, Δ, K, U) are invariant. If (κ, u, Δ, K, U) is invariant, then (κ, u′, Δ, K, U) is also invariant.

Proof The proof is by induction over the structure of u and u′.

• if u = u′ = Kind, then it is trivially true.

• if u = u′ = z, then again it is trivially true.

• if u = Πt : κ_{1}. u_{1} and u′ = Πt : κ_{2}. u_{2}, then we have that κ_{1} =_{βηι} κ_{2} and u_{1} =_{βηι} u_{2}. By assumption, we know that (κ_{1}, Kind, Δ, K, U) and (κ_{2}, Kind, Δ, K, U) are invariant. This means that C_{U}^{K}(κ_{1}) = C_{U}^{K}(κ_{2}). Moreover, Δ ⊢ τ : κ_{1} is true iff Δ ⊢ τ : κ_{2} is true. Applying the induction hypothesis now leads to the required result.

• if u = Πk: u_{1}. u_{2} and u′ = Πk: u′_{1}. u′_{2}, the proof is similar to the previous case.

□

Definition 70 Suppose Δ ⊢ u : Kscm is a derivable judgment. We say that all instantiations of (u,Kscm, Δ) are invariant if for all instantiations (Θ, ϕ) adapted to Δ and for all interpretations U adapted to Θ, we have that (ϕ(u), Kscm, Θ, ∅, U) is invariant.

D.3.18 Strong normalization of pure terms

Theorem 71 Let Δ ⊢ τ : κ be a derivable judgment and K and U be a mapping and an interpretation adapted to Δ. Then C_{U}^{K}(τ) ∈ C_{U}^{K}(κ).

Proof The proof is by induction over the length of the derivation. The induction hypothesis are as follows:

• if Δ ⊢ τ : κ and K and U be a mapping and an interpretation adapted to Δ, then C_{U}^{K}(τ) ∈ C_{U}^{K}(κ);

• if Δ ⊢ κ : u, then all instantiations of (κ,u, Δ) are invariant;

• if Δ ⊢ u : Kscm, then all instantiations of (u,Kscm, Δ) are invariant;

type formation rules This paragraph deals with rules of the form Δ ⊢ τ : κ.

• abstractions – Follows directly from the induction hypothesis and lemmas 43 and 44 and 45.

• var – Follows because the interpretation U is adapted to the context Δ.

• weak elimination – Follows from lemma 47.

• constructor – Follows from lemma 48.

• weakening – Follows directly from the induction hypothesis since the mapping and interpretation remain adapted for a smaller context.

• conv – Follows from the recursion hypothesis and lemma 55.

• app – All three cases of app are proved similarly. We will show only one case here.

– Δ ⊢ τ[u′] : κ. Then we know that Δ ⊢ τ : Πz : Kscm. κ_{1} and Δ ⊢ u′ : Kscm and [u′/z]κ_{1} = κ. By the induction hypothesis

C_{U}^{K}(τ) ∈ ∩_{u_{1}∈arity(u,Kind)}C_{U}^{K,z:u_{1}}(κ_{1})

Suppose u′_{1} = K(u′). Then we know that C_{U}^{K}(τ) ∈ C_{U}^{K,z:u′_{1}}(κ_{1}). By proposition 61 we know that C_{U}^{K}(τ) ∈ C_{U}^{K}([u′/z]κ_{1}). But C_{U}^{K}(τ[u′]) = C_{U}^{K}(τ).

kind formation rules This paragraph deals with rules of the form Δ ⊢ κ : u.

• product – All the product formation rules are proved in the same way. We show only one case here.

– Consider the following formation rule

Δ, z:Kscm ⊢ κ : Kind Δ ⊢ Πz:Kscm. κ : Kind

We have to prove that for all instantiations (Θ, ϕ) we have that (Πz:Kscm. ϕ(κ), Kind, Θ, ∅, U) is invariant. This implies that we must prove that if κ ⊳ κ′, then C_{U}^{∅}(Πz : Kscm. ϕ(κ)) = C_{U}^{∅}(Πz : Kscm. ϕ(κ′)). By the induction hypothesis, for all instantiations (Θ, ϕ; z: arity(u, Kind)) we have that

(ϕ; z:arity(u, Kind)(κ), Kind, Θ, ∅, U)

is invariant. This implies that if κ ⊳ κ′ then

C_{U}^{,z:arity(u,Kind)}(κ) = C_{U}^{,z:arity(u,Kind)}(κ′)

The required result follows from here.

• var – follows since the instantiation is adapted.

• conv – follows from lemma 58.

• application – Both of the applications are proved similarly and follow directly from the induction hypothesis. We will show only one case here.

– If Δ ⊢ κ_{1} κ_{2} : [κ_{2}/k]u, then given Θ, ϕ, and U, we must prove that (ϕ(κ_{1} κ_{2}), ϕ([κ_{2}/k]u), Θ, ∅, U) is invariant. But by the induction hypothesis we know that (ϕ(κ_{1}), ϕ(Πk : u_{1}. u), Θ, ∅, U) is invariant and Δ ⊢ κ_{2} : u_{1}. By lemma 57 Θ ⊢ ϕ(κ_{2}) : ϕ(u_{1}). This leads to the required result.

• ind – Suppose I = Ind(k : Kind){κ⃗}. Note that C_{U}^{K}(I) depends only on C_{U,k:S,A′:C,B′:Co(i)}^{K}(ζ_{k,I}(κ_{i}, A′, B′)) where S ∈ ρ_{0}(Kind) and C ∈ CR(I → Kind)_{K}. By induction on the structure of κ_{i}, we can show that this is invariant. This implies that if κ_{i} ⊳ κ′_{i} then the interpretation remains the same. If I ⊳ I′, then for some i, κ_{i} ⊳ κ′_{i}. From here we can deduce that if I ⊳ I′, then C_{U}^{K}(I) = C_{U}^{K}(I′).

• large elim – Follows from lemma 56.

• abstraction – Both of the abstractions are proved similarly. So we will show only one of the cases.

– Δ ⊢ λt : κ_{1}. κ_{2} : Πt : κ_{1}. u. We must prove that (ϕ(λt : κ_{1}. κ_{2}), ϕ(Πt : κ_{1}. u), Θ, ∅, U) is invariant, given Θ, ϕ, and U. This implies that if Θ ⊢ τ : ϕ(κ_{1}) and τ belongs to the appropriate candidate, then we must have (ϕ(λt: κ_{1}. κ_{2}) τ, [τ/t]ϕ(u), Θ, ∅, U) is invariant. By proposition 65 we must prove that

([τ/t]ϕ(κ_{2}), [τ/t]ϕ(u), Θ, ∅, U)

is invariant. But (ϕ, t : τ) is an instantiation that is adapted to (Δ, t : κ_{1}). Applying the induction hypothesis now leads to the result.

schema formation rules This paragraph deals with rules of the form Δ ⊢ u : Kscm.

• u = Kind follows directly.

• u = z follows since the instantiation is adapted.

• u = Πk : u_{1}. u_{2} Given Θ, ϕ, and U we have to prove that (ϕ(Πk : u_{1}. u_{2}), Kscm, Θ, ∅, U) is invariant. By the induction hypothesis, we know that (ϕ(u_{1}), Kscm, Θ, ∅, U) is invariant. The induction hypothesis also says that ([ϕ, k : κ](u_{2}), Kscm, Θ, ∅, U) is invariant. We also know that Δ ⊢ κ : ϕ(u_{1}) and (κ, ϕ(u_{1}), Θ, ∅, U) is invariant since the instantiation is adapted. This implies that (ϕ([κ/k]u_{2}), Kscm, Θ, ∅, U) is invariant.

• u = Πt:κ_{1}. u_{1} the proof is very similar to the above case.

□

Corollary 72 If τ is a well formed type, |τ | is strongly normalizing.

Proof Since τ is well formed we have that Δ ⊢ τ : κ. We only need to construct an interpretation and a mapping. For the interpretation, let U(t) = t for every type variable. Then we get C_{U}^{K}(τ) =|τ |.

We can build the rest of U and K as:

• if Δ = · then U(k) = Can_{0}(Kind) and K(z) = Kind for all variables k and z;

• if Δ = Δ′, t : κ then return the U′ and K′ associated with Δ′;

• if Δ = Δ′, k : u then U = U′, k : C and K = K′, where C ∈ CR(u)_{K′} and K′ and U′ are associated with Δ′;

• if Δ = Δ′, z : Kscm then K = K′, z : Kind and U = U′ where K′ and U′ are associated with Δ′.

□

D.3.19 Normalization of terms

In this section, we use an encoding that maps all well formed terms to types. This encoding preserves the number of reductions. The idea is similar to that of Harper et al [20].

The encoding uses two constants. A is a kind and B is a type.

∗ is a variable that is never used, it is a wild-card.

A :Kind
B :Πk:Kind. k
∗ unused variable

The encoding for Kscm is as follows:

S(Kscm) = Kscm
U(Kscm) = Kind
K(Kscm) = A

The encoding for schemas is as follows:

U(Kind) = Kind
U(Πt:κ. u) = Πt:K(κ). U(u)
U(Πk:u_{1}. u_{2}) = Πk:U(u_{1}). Πt_{k}:K(u_{1}). U(u_{2})
U(z) = z
K(Kind) = A
K(Πt:κ. u) = Πt:K(κ). K(u)
K(Πk:u_{1}. u_{2}) = Πk:U(u_{1}). Πt_{k}:K(u_{1}). K(u_{2})
K(z) = k_{z}
T (Kind) = B A
T (Πt:κ. u) = B[A → Πt:K(κ). A → A]
T (κ)(λt:K(κ). T (u))
T (Πk:u_{1}. u_{2}) = B[A → Πk:U(u_{1}). Πt_{k}:K(u_{1}). A → A]
T (u_{1})(λk:U(u_{1}). λt_{k}:K(u_{1}). T (u_{2}))
T (z) = t_{z}

The encoding for kinds is as follows:

K(k) = k
K(Πt:κ_{1}. κ_{2}) = Πt:K(κ_{1}). K(κ_{2})
K(Πk:u. κ) = Πk:U(u). Πt_{k}:K(u). K(κ)
K(Πz:Kscm. κ) = Πz:Kscm. Πk_{z}:Kind. Πt_{z}:A. K(κ)
K(λk:u. κ) = λk:U(u). λt_{k}:K(u). K(κ)
K(λt:κ_{1}. κ_{2}) = λt:K(κ_{1}). K(κ_{2})
K(κ τ) = K(κ) T (τ)
K(κ_{1} κ_{2}) = K(κ_{1}) K(κ_{2})T (κ_{2})
K(Ind(k:Kind)\{κ⃗\}) = Ind(k:Kind)\{\overrightarrow{K(κ)}\}
K(Elim[κ, u](τ)\{κ⃗′\}) = Elim[K(κ), U(u)](T (τ))\{\overrightarrow{K(κ′)}\}

T (k) = t_{k}
T (Πt:κ_{1}. κ_{2}) = B[A → Πt:K(κ_{1}). A → A]
T (κ_{1})(λt:K(κ_{1}). T (κ_{2}))
T (Πk:u. κ) = B[A → Πk:U(u). Πt_{k}:K(u). A → A]

T (u)(λk:U(u). λt_{k}:K(u). T (κ))

T (Πz:Kscm. κ) =
B[Πz:Kscm. Πk_{z}:Kind. Πt_{z}:A. A → A]

(λz:Kscm. λk_{z}:Kind. λt_{z}:A. T (κ))

T (λk:u. κ) =
λk:U(u). λt_{k}:K(u). (λ∗:A. T (κ))T (u)
T (λt:κ_{1}. κ_{2}) = λt:K(κ_{1}). (λ∗:A. T (κ_{2}))T (κ_{1})
T (κ τ) = T (κ) T (τ)
T (κ_{1} κ_{2}) = T (κ_{1})[K(κ_{2})]T (κ_{2})
T (Ind(k:Kind){κ⃗}) =
B[(Kind → A → (A → … → A) → A) → A]

(λk:Kind. λt_{k}:A. λY :(A → … → A). (Y \overrightarrow{T (κ_{i})})) T (Elim[κ, u](τ){κ⃗′}) =

Elim[K(κ), (λ∗:K(κ). K(u))](T (τ))

\{\overrightarrow{(λ∗:A. λ∗:A. T (κ′_{i}))T (κ)T (u)}\}

The encoding for types is as follows:

T (t) = t
T (λt:κ. τ) = λt:K(κ). (λ∗:A. T (τ))T (κ)
T (τ_{1} τ_{2}) = T (τ_{1}) T (τ_{2})
T (λk:u. τ) = λk:U(u). λt_{k}:K(u). (λ∗:A. T (τ))T (u)
T (τ[κ]) = T (τ)[K(κ)]T (κ)
T (λz:Kscm. τ) = λz:Kscm. λk_{z}:Kind. λt_{z}:A. T (τ)
T (τ[u]) = T (τ)[U(u)][K(u)] T (u)
T (Ctor (i, κ)) = (λ∗:A. Ctor (i, K(κ)))T (κ)

T (Elim[κ, κ_{1}](τ){τ⃗}) = Elim[K(κ), K(κ_{1})](T (τ))\{\overrightarrow{(λ∗:A. λ∗:A. T (τ_{i}))T (κ)T (κ_{1})}\}

We have to define a similar transformation on contexts:

Γ(·) = ·, A:Kind, B:Πk:Kind. k
Γ(Δ, t:κ) = Γ(Δ), t:K(κ)
Γ(Δ, k:u) = Γ(Δ), k:U(u), t_{k}:K(u)
Γ(Δ, z:Kscm) = Γ(Δ), z:Kscm, k_{z}:Kind, t_{z}:A

D.3.20 Coding and reduction

In this section we state lemmas that prove that the coding preserves the number of reductions. We omit the proofs since they follow by a straightforward induction over the structure of terms.

Lemma 59 For all well typed terms A, if A ⊳_{β} A′, then we have

T (A) ⊳_{β}^{1+} T (A′) K(A) ⊳_{β}^{∗} K(A′) U(A) ⊳_{β}^{∗} U(A′)

Moreover, if ∥A∥ ⊳_{β}A_{1}, then there exists A_{2} such that ∥A_{2} ∥= A_{1} and |T (A)| ⊳^{1+} |T (A_{2})|.

Lemma 60 For all well typed terms A, if A ⊳_{ι} A′, then we have

T (A) ⊳_{ι}^{1+} T (A′) K(A) ⊳_{ι}^{∗} K(A′) U(A) ⊳_{ι}^{∗} U(A′)

Moreover, if ∥A∥ ⊳_{ι_{0}}A_{1}, then there exists A_{2} such that ∥A_{2} ∥= A_{1} and |T (A)| ⊳^{1+} |T (A_{2})|.

Lemma 61 For all well typed terms A, if A ⊳_{η} A′, then we have

T (A) ⊳_{βη}^{1+} T (A′) K(A) ⊳_{βη}^{∗} K(A′) U(A) ⊳_{βη}^{∗} U(A′)

D.3.21 Coding and typing

In this section we show that the coding of a well typed term is also well typed. For this we need to prove that the coding preserves βηι equality. This requires a confluent calculus. Therefore, we use the unmarked terms from Section D.2.1. We extend the coding to unmarked terms by defining:

\begin{aligned}U( ) & = \\ K( ) & = \\ T ( ) & = \end{aligned}

It is now easy to prove by a straightforward induction on the structure of terms that the following lemma holds:

Lemma 62 Suppose Δ ⊢ A : B and B ≠ Ext. Then we have that

Γ(Δ) ⊢ T (A) : K(B) and Γ(Δ) ⊢ K(B) : Kind Γ(Δ) ⊢ K(A) : U(B) and Γ(Δ) ⊢ U(B) : Kscm if defined Γ(Δ) ⊢ U(A) : S(B) and Γ(Δ) ⊢ S(B) : Ext if defined

Corollary 73 Suppose Δ ⊢ A : B and B ≠ Ext. Then | T (A) | is strongly normalizing.

D.3.22 Normalization of unmarked terms

Lemma 63 For all well typed terms A, we have that ∥A∥ is strongly normalizing for βηι_{0} reduction.

Proof Since there can not be an infinite sequence of η reductions and we can delay η reductions, we need to prove the normalization for βι_{0} reductions only. Suppose ∥ A ∥ is not normalizing and there exists a sequence A_{1} … A_{i} … such that A_{i} ⊳_{βι_{0}} A_{i+1} and A_{0} =∥ A ∥. By lemma 59 and 60, we get that there exists a sequence of terms A′_{1} … A′_{i} … such that ∥A′_{i} ∥= A_{i} and |T (A′_{i})| ⊳_{βι}^{1+} | T (A′_{i+1}) | and also | T (A) | ⊳_{βι}^{1+} | T (A′_{1}) |. This implies that | T (A) | is not strongly normalizing which is a contradiction. □

D.3.23 Normalization of all terms

Lemma 64 Suppose A ⊳_{βι} B. Then ∥T (A)∥ ⊳_{βι}^{1+} ∥T (B)∥.

Proof By induction over the derivation of A ⊳_{βι} B. Note that in taking a term A to T (A), all the terms C that appear as annotations at lambda abstractions are duplicated with the corresponding T (C). □

Lemma 65 Suppose Δ ⊢ A : B. Then A is strongly normalizing.

Proof We only have to prove normalization for βι reduction. By lemma 64, if A is not normalizing, then ∥ T (A) ∥ is also not normalizing. But by lemma 62 we have that Γ(Δ) ⊢ T (A) : K(B) which implies ( lemma 63) that ∥ T (A) ∥ is strongly normalizing. □

Theorem 74 (Strong normalization) All well typed terms are strongly normalizing.

Proof Follows from lemma 65. □

D.4 Church-Rosser Property

The proof is structured as follows:

• We first prove that a well typed term A in βι normal form has the same η reductions as ∥A∥.

• From here we know that if A and A′ are in normal form, then ∥A∥ and ∥A′ ∥ are equal. We then show that the annotations in the λ-abstractions are equal.

D.4.1 Structure of normal forms

Lemma 66 All well typed βι normal terms N have the following form:

1. λX:N_{1}. N_{2}.

2. ΠX:N_{1}. N_{2}.

3. s ∈ {Kind, Kscm, Ext}.

4. X N⃗.

5. Ind(X:Kind){N⃗}.

6. Ctor (i, N) N⃗ where N is of the form 5.

7. Elim[N, N_{2}](N_{1}){N⃗} N⃗′ where N is of the form 5 and N_{1} is of the form 4.

Lemma 67 Let Δ, X:C, Δ′ ⊢ A : B be a judgment and A in βι normal form. If X does not occur in FV (B) ∪ FV (Δ′) ∪ FV (∥A∥), then X ∉ FV (A).

Proof The proof is by induction over the size of A. We use lemma 66 to enumerate the different cases.

• The case where A is a variable or a sort is immediate.

• Suppose Δ, X : C, Δ′ ⊢ ΠY : N_{1}. N_{2} : B. It follows directly from the induction hypothesis that X does not occur in N_{1} and N_{2}.

• Suppose Δ, X : C, Δ′ ⊢ λY : N_{1}. N_{2} : B and B = ΠY : N_{1}. A′. We know that Δ, X: C, Δ′ ⊢ N_{1} : s and therefore X ∉ FV (N_{1}). Also B⊳^{∗}ΠY :N′_{1}. A′′ and Δ, X:C, Δ′, Y : N_{1} ⊢ N_{2} : A′′. Since X ∉ FV (A′′) ∪ FV (N_{1}), we can apply the induction hypothesis and therefore X ∉ FV (N_{2}).

• Suppose Δ, X: C, Δ′ ⊢ Y N⃗ : B. This implies that Δ, X: C, Δ′ ⊢ Y : ΠZ : A_{1}. A_{2} and Δ, X : C, Δ′ ⊢ N_{1} : A_{1}. From lemma 23 and 13 we have that Δ, X : C, Δ′ ⊢ Y : ΠZ : A_{3}. A_{4} where X does not occur free in A_{3} and A_{3} =_{βηι} A_{1} and A_{4} =_{βηι} A_{2}. From here we can show that Δ, X : C, Δ′ ⊢ N_{1} : A_{3}. We can now apply the inductive hypothesis to show that X ∉ FV (N_{1}). Iterating in this way, we can show that X ∉ FV (N_{i}).

• Suppose Δ, X : C, Δ′ ⊢ Ind(Y : Kind){N⃗} : B. Follows directly from the induction hypothesis that X ∉ FV (N_{i}).

• Suppose Δ, X:C, Δ′ ⊢ Ctor (i, I) N⃗ : B. Follows directly from the induction hypothesis that X ∉ FV (I). We can then show as above that X ∉ FV (N_{i}).

• Suppose Δ, X : C, Δ′ ⊢ Elim[N, N_{1}](N_{2}){N⃗} N⃗′ : B. Since Δ, X : C, Δ′ ⊢ N : Kind, it follows from the induction hypothesis that X ∉ FV (N). Similarly, since Δ, X : C, Δ′ ⊢ N_{1} : Kscm, or Δ, X:C, Δ′ ⊢ N_{1} : N → Kind, it follows that X ∉ FV (N_{1}). Similarly we can prove directly from the induction hypothesis that X ∉ FV (N_{2}) ∪ FV (N⃗). Finally, as above we can prove that X ∉ FV (N⃗′). □

Corollary 75 Let Δ ⊢ A : B. If A is in normal form, then ∥ A ∥ is also in normal form.

Proof We must show that ∥ A ∥ does not contain any η reductions. The interesting case is when A is of the form λX : N_{1}. N_{2} X. We want to show that if X ∉ FV (∥ N_{2} ∥), then X ∉ FV (N_{2}). Since it is well typed we know that Δ ⊢ λX : N_{1}. N_{2} X : ΠX : N_{1}. C. We have that X ∉ FV (ΠX : N_{1}. C). From here we get that Δ, X : N_{1} ⊢ N_{2} : ΠX : N_{1}. C. This implies that if X ∉ FV (∥N_{2} ∥), then X ∉ FV (N_{2}). □

D.4.2 Church-Rosser

Theorem 76 (Church-Rosser) Let Δ ⊢ A : B and Δ ⊢ A′ : B be two derivable judgments. If A =_{βηι} A′, and if A and A′ are in normal form, then A = A′.

Proof We know that ∥ A ∥ and ∥ A′ ∥ are in normal form. Since the unmarked terms are confluent we have that ∥ A ∥=∥ A′ ∥. The proof is by induction over the structures of A and A′.

• The case when A = A′ = s or A = A′ = a variable is immediate.

• Suppose A = λX:N_{1}. N_{2} and A′ = λX:N′_{1}. N′_{2}. We know that B =_{βηι} ΠX: N_{1}. A_{3} =_{βηι} ΠX: N′_{1}. A′_{3}. This implies that N_{1} =_{βηι} N′_{1} which implies that both of them have the same sort. This implies that N_{1} = N′_{1}. We can now apply the induction hypothesis to N_{2} and N′_{2} to get that N_{2} = N′_{2}.

• Suppose A = ΠX:N_{1}. N_{2} and A′ = ΠX:N′_{1}. N′_{2}. Follows directly from the induction hypothesis.

• Suppose A = X N⃗ and A′ = X N⃗′. We know that in the context Δ, the variable X has the type ΠY⃗ :B⃗. A_{3}. Therefore each of the N_{i} and N′_{i} have the same type. Applying the induction hypothesis to each of them leads to the required result.

• Suppose A = Ind(X : Kind){N⃗} and A′ = Ind(X : Kind){N⃗′}. By the typing rules we know that Δ, X:Kind ⊢ N_{i} : Kind and Δ, X : Kind ⊢ N′_{i} : Kind. Applying the induction hypothesis leads to N_{i} = N′_{i}.

• Suppose A = Ctor (i, N) N⃗ and A′ = Ctor (i, N′)N⃗′. We know that both N and N′ have type Kind. The induction hypothesis directly leads to N = N′. We can then show as above that N_{i} = N′_{i}.

• Suppose A = Elim[N, N_{1}](N_{2}){N⃗} N⃗_{0} and A′ = Elim[N′, N′_{1}](N′_{2}){N⃗′} N⃗′_{0}. Since N and N′ are both of type Kind, it follows that N = N′. From here we get that N_{2} = N′_{2}. Since both N_{1} and N′_{1} have the type Kscm or have the type N → Kind, it follows that N_{1} = N′_{1}. From this we can show that the N_{i} and N′_{i} are equal. Finally as above, we can show that the N_{0i} and the N′_{0i} are equal. □

Theorem 77 (Confluence) Let Δ ⊢ A : B and Δ ⊢ A′ : B be two judgments. If A =_{βηι} A′, then A and A′ have a common reduct – there exists a term C such that A ⊳^{∗} C and A′ ⊳^{∗} C.

Proof We know that both A and A′ reduce to normal forms A_{1} and A′_{1}. Due to subject reduction, both A_{1} and A′_{1} have the same type B. By the previous lemma A_{1} = A′_{1}. □

D.5 Consistency

Theorem 78 (Consistency of the logic) There exists no term A for which · ⊢ A : ΠX:Kind. X.

Proof Suppose there exists a term A for which · ⊢ A : ΠX : Kind. X. By theorem 74, there exists a normal form B for A. By the subject reduction · ⊢ B : ΠX : Kind. X. We can show now that this leads to a contradiction by case analysis of the possible normal forms for the types in the calculus. □