Typed Operational Semantics for Higher Order Subtyping

Adriana Compagnoni

                   abc@dcs.ed.ac.uk

Healfdene Goguen

                                               hhg@dcs.ed.ac.uk

Department of Computer Science, University of Edinburgh The King’s Buildings, Edinburgh, EH9 3JZ, United Kingdom Tel: (+44) (131) 650-1000 Fax: (+44) (131) 667-7209

Abstract

Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce F_{≤}^{ω}, a variant of F_{<:}^{ω} with this feature and with Cardelli and Wegner’s kernel Fun rule for quantifiers. We define a typed operational semantics with subtyping and prove that it is equivalent with F_{≤}^{ω}, using a Kripke model to prove soundness. The typed operational semantics provides a powerful tool to establish the metatheoretic properties of F_{≤}^{ω}, such as Church–Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system.

1 Introduction

During the last decade, object-oriented programming languages such as Smalltalk, C++, Modula 3, and Java have become popular because they encourage and facilitate software reuse and abstract design. In this time, the theoretical community has struggled to achieve a balance between safety and expressiveness of object-oriented programming languages, where safe languages use type systems to restrict the legal programs and thereby prevent errors, and expressive languages provide more constructs to allow the programmer to write programs more clearly or concisely.

A wide variety of language features has been proposed to model constructs from objectoriented programming languages in type systems, for example bounded quantification [21], recursive types [3], and matching [1, 9]. The feature we study in this paper is bounded abstraction on types, also called bounded operator abstraction. Cardelli and Harper are in favor of including this in ML2000 (private communication), the successor of Standard ML. The constructor is amply motivated by many examples due to Kim Bruce [6], including the following, which shows how bounded abstraction on types can be used to define the type of binary search trees with comparable elements:

Comparable = ΛX: ⋆ .[eq : X → X → Bool, lt : X → X → Bool, gt : X → X → Bool]

BinTree = ΛX: ⋆ .ΛY ≤(Comparable X): ⋆ .[ \begin{matrix}find & : & Y → Bool, \\ insert & : & Y → BinTree, \\ isEmpty & : & Bool] \end{matrix}

The calculus we study in this paper, F_{≤}^{ω}, is a minimal type theoretic presentation without all of the features needed to construct this example, such as object and recursive types. However, Abadi and Cardelli’s study of the higher-order object calculus [2] has demonstrated that these object-oriented features do not present difficulties for the metatheory.

The focus of this paper is on the metatheoretic treatment of subtyping. We see the contributions of the paper as the following:

• We develop the metatheory of a particular type theory, F_{≤}^{ω}, which captures important features for the foundations of object-oriented programming languages.

• We introduce a typed operational semantics for a language with subtyping, as an intermediate language for proving syntactic results about the type theory.

• We give a logical relation style interpretation of subtyping, which allows us to study properties of kinding and subtyping simultaneously. Although such a construction was essential in order to be able to use typed operational semantics, it could also form the basis for the study of a system with subtyping directly using an algorithm for subtyping.

The paper is structured as follows. In the remainder of the introduction we give background information to clarify the second and third points above. In Section 2 we introduce the syntax of F_{≤}^{ω}. In Section 3 we introduce the typed operational semantics for this system. In Section 4 we develop the fundamental properties of types and kinds in F_{≤}^{ω}. Section 5 gives the model construction that shows soundness of the typed operational semantics for the typing rules. In Section 6 uses the previous results to prove subject reduction for terms in F_{≤}^{ω}. Section 7 shows the equivalence of the usual and algorithmic presentations of F_{≤}^{ω}. Finally, in Section 8 we summarize related and future work, and Section 9 gives our conclusions.

1.1 Syntactic Properties of Interest

We believe that type-checking for programming languages should be decidable. Decidable type systems prevent basic programming errors by limiting the meaningful programs. While we want the type system to be powerful to allow more expressive programs, the type system should also have a low overhead for the programmer. In particular, the compiler should be able to recognize correct and incorrect programs reliably without help from the programmer. While the decidability of type- and subtype-checking for F_{≤}^{ω} are beyond the scope of this paper, the same technique used by Compagnoni [17] to prove these properties can be applied here.

For type systems with subtyping, an important aspect of decidable type-checking is the ability to eliminate instances of transitivity in subtyping. The transitivity rule leads to significant non-determinism, which in turn leads to infeasible subtyping algorithms. Thus existing algorithms for systems with decidable or semi-decidable subtyping [4, 16, 17, 32, 33] are syntax-directed in their search and only use transitivity in a specific, restricted way.

Another important property of a type system is subject reduction or type preservation, which states that evaluation of programs preserves their type. This is one of the central results of the paper. However, we also focus on the same property at the level of types, as well as showing strong normalization for types, which states that type reduction will always terminate. Both of these properties are needed to show the correctness of the algorithms for type-formation and subtyping.

1.2 Metatheory of Subtyping

Adding bounded operator abstraction to F_{<:}^{ω} leads to complications in studying metatheoretic properties of the system. The new constructor means that subtyping is now needed to check well-formation of types. Because type-checking is also needed in subtyping, this presents a circularity that together with β-equality is not trivial to study. In particular, we now need knowledge about subtyping to show results like subject reduction for types.

Most type systems with subtyping do not have this circularity: for example, F_{<:}^{ω} [11, 13, 12, 31, 14], F_{∧}^{ω} [18], and the systems in Abadi and Cardelli’s book on objects [2] all separate the two judgements. Existing work on systems with such a circularity [4] avoids the interdependency by finding a particular order in which to prove results.

A similar interdependency exists in dependent type theory between the typing judgement and the equality of types. Typed operational semantics was originally developed for type theories with dependent types [24, 25], and gives a uniform treatment of syntactic properties such as substitution and generation lemmas, subject reduction, and strong normalization. By developing the metatheory of F_{≤}^{ω}, this paper demonstrates that the technique can be extended successfully to type theories with subtyping. In particular, our approach of building a typed model for subtyping avoids many problems due to the circularity, by including extra structural information to allow proofs to go through.

Typed operational semantics also gives a clarification of proofs of strong normalization. The traditional proof of strong normalization for type theories builds a model where types are interpreted as sets of strongly normalizing terms. In this proof, details about strong normalization are mixed with the model: for example, such proofs rely on the fact that if e_{1}, e_{2} and e_{1}[x←e_{2}] are strongly normalizing then (λx.e_{1})(e_{2}) is strongly normalizing. In practice, such details are often suppressed, perhaps because they seem incongruous amidst the otherwise model-theoretic reasoning.

Typed operational semantics divides this proof into two conceptually different steps. First, we show results about well-formed terms in the typed operational semantics, such as that they are strongly normalizing. Secondly, we construct a model where types are interpreted as sets of terms of that type in the typed operational semantics. This gives us a type soundness result with respect to the operational semantics, informally similar to that for ML [36], although formally much stronger because the typed operational semantics encodes both type and reduction information. Composing the two results gives us strong normalization for the well-typed terms.

This describes the general approach of using typed operational semantics. However, because our goal is to study the subtyping relation, we build our construction over the language of types and kinds in F_{≤}^{ω}, rather than over terms and types. Indeed, following our discussion above, while it should be possible to add non-terminating reductions to the language of terms, such as those for the object constructors of Abadi and Cardelli [2], it is our intention that the language of types and kinds should have desirable syntactic properties such as strong normalization. We can therefore use traditional approaches from type theory to study these properties.

Previous approaches to the metatheory of subtyping have used strong normalization of types as a basis for further reasoning about the subtyping relation. For example, Compagnoni [17] defines a system for subtyping normal types, and shows that this system is sound for rules of substitution and application, relying on a previous result that every wellformed type is strongly normalizing. In this paper, we instead extend the approach of typed operational semantics by building a logical relation style interpretation of the subtyping relation together with the interpretation of the typing relation. We are then able to study metatheoretic properties of well-formed types and the subtyping relation simultaneously, by reasoning in the typed operational semantics. Again, because we are concentrating on syntactic properties of subtyping, this does not follow the usual interpretation of subtyping in the literature as set inclusion [5, 7, 8, 10, 14, 18, 22, 32].

Our approach has the conceptual benefit of treating the interdependent judgements of kinding and subtyping simultaneously, which means that it is not sensitive to proving results in a specific order. Furthermore, the techniques we use here were originally developed for showing soundness of the semantics for the typing rules in dependent types. This suggests that our proof technique will be well-suited to studying more sophisticated type theories with subtyping, such as the Calculus of Constructions.

We now discuss the two steps of the model construction and the typed operational semantics in more detail, and mention which metatheoretic results follow from each step, with particular attention to the treatment of the subtyping judgement. We refer the reader to the original papers on typed operational semantics [24, 25, 26] for a more complete description of this technique.

1.3 The Typed Operational Semantics

The intermediate system in our proof, the typed operational semantics, offers an alternative induction principle to prove syntactic properties of type theories. We can use this system to prove more properties of types than simply strong normalization. Church–Rosser and subject reduction (Corollary 4.13) are particularly simple to show in the typed operational semantics, and therefore by soundness hold for the original typing system. We can also prove lemmas about replacing equal bounds and kinds in the context (Lemma 4.17) and transitivity elimination (Lemma 4.21) in the typed operational semantics. The power of this technique is still more evident in systems with η-equality [24], because Church–Rosser is only true for the well-typed terms, and therefore cannot be shown by purely syntactic means [30].

Finally, because the typed operational semantics is an algorithmic presentation of the type theory, we are able to use the equivalence of the typed operational semantics with the usual typing rules to prove the generation lemmas in Section 5.4 that are the basis for the metatheory of the term language of F_{≤}^{ω}. This also allows us to prove in Section 7.6 the equivalence with the usual algorithmic presentation of the typechecking and subtyping relations, which include much less intermediate type information than typed operational semantics.

In our treatment, we have only given a typed operational semantics for the language of types and kinds, and the subtyping relation. This is because the full term language is intended to have recursion operators and objects, so the terms will not be strongly normalizing. The analysis of the language of types is still important, because it gives us information about the decomposition of subtyping judgements that allows us to prove subject reduction for terms and to show important properties about the typechecking and subtyping algorithms.

1.4 The Model Construction

The model construction for typed operational semantics is somewhat more complicated than the usual models for strong normalization proofs, because we build a model with well-formed types. We rely on several techniques used in the metatheory of dependent type theory:

• We build a Kripke-style model [20] with contexts as possible worlds: this is necessary to capture adding fresh variables to model the Π- and Λ-binders.

• We introduce a partial interpretation of kinds [34] to ensure that the kinding statement makes sense when modeling the kind ΠX≤A:K_{1}.K_{2}, which is only defined when the type A is well-formed.

• To give a typed treatment of subtyping we need to introduce a logical relation style interpretation of the subtyping judgement as well as the kinding judgement, based on a similar treatment of judgemental equality by Coquand [19].

We shall discuss the technical aspects of these constructions when we define the model in Section 5.

Although this may seem to complicate the proof considerably, these techniques are all well-established in the dependent type theory community. There are several justifications for preferring our approach. First, the extensions to the usual technique seem to be exactly what is required for the proof of soundness for the typed operational semantics. Secondly, we obtain an unexpected benefit by using the typed operational semantics and a model with kinded types: we are able to show the admissibility of the metatheoretic properties in Section 2.3, such as substitution, context replacement, and kind correctness, in the model construction, rather than showing them separately by induction on derivations. Finally, as we discuss in Section 8, using this model has suggested alternatives to the standard presentation of F_{<:}^{ω} that may satisfy transitivity elimination in the algorithm.

There is a simple intuition for why these results follow when we extend the model to kinded types. First, we notice that every proof of strong normalization needs to allow for substitution properties, because it is exactly this that allows us to model β-reduction. Hence, it is not surprising that rules like substitution are sound for what is essentially a model of strongly normalizing types with kind information.

Although we say that the model is built with well-kinded types, the types are wellkinded with respect to the typed operational semantics, a reduction sequence to normal form, not with respect to the kinding rules of F_{≤}^{ω}. Because the reduction includes kinding information, it is possible to prove completeness: that a derivation of the well-formedness of a type in the typed operational semantics gives rise to a derivation of well-formedness in the usual typing system. However, the rules of inference for the typed operational semantics are restricted: there are rules for redices such as β, and structural rules allowing reduction within a type, but as usual for an algorithmic presentation, there are no general substitution rules. Hence, by appealing to soundness (Corollary 5.12), which eliminates uses of substitution in constructing a derivation in the typed operational semantics, and completeness (Proposition 4.6), which reflects the derivation without uses of substitution back into F_{≤}^{ω}, we are able to eliminate all instances of the substitution rules.

We have therefore reduced the metatheory of a type theory to essentially two steps: first, develop some basic results of the system in the typed operational semantics, where syntactic results are relatively easy; and secondly, prove the equivalence of the typed operational semantics with the typing rules, where completeness is direct.

2 Syntax

We now present the rules for kinding, subtyping, and typing in F_{≤}^{ω}. They are organized as proof systems for several interdependent judgement forms:

Γ ⊢ ok  well-formed context
Γ ⊢ K  well-formed kind
Γ ⊢ K = K′  kind equality
Γ ⊢ A : K  well-kinded type
Γ ⊢ A = B : K type equality
Γ ⊢ A ≤ B : K subtype
Γ ⊢ M : A  well-typed term.

We sometimes use the metavariable J to range over statements (right-hand sides of judgements) of any of these judgement forms.

2.1 Syntactic Categories

The kinds of F_{≤}^{ω} are the kind ⋆ of proper types and the kinds ΠX≤A:K_{1}.K_{2} of functions on types (sometimes called type operators).

𝕂 ::= ⋆  types
ΠX≤𝔸:𝕂.𝕂 type operators

The language of types of F_{≤}^{ω} is a straightforward higher-order extension of F_{≤}, Cardelli and Wegner’s second-order calculus of bounded quantification. Like F_{≤}, it includes type variables X; function types A→B; and polymorphic types ∀X≤A:K.B, in which the bound type variable X ranges over all subtypes of the upper bound A. Moreover, like F^{ω}, we allow types to be abstracted on types, but we allow bounds on the abstraction ΛX≤A:K.B. We can also apply types to argument types A B; in effect, these forms introduce a simply typed λ-calculus with subtyping at the level of types. We shall sometimes use the word “types” to mean types and type operators.

The capture-avoiding substitution of A for X in B is written B[X←A]. We identify types that differ only in the names of bound variables. We shall write A(B_{1}, …, B_{n}) for ((A B_{1}) … B_{n}). If A is of the form X(B_{1}, …, B_{n}) then A has head variable X. We write HV(−) for the partial function returning the head variable of a term. We also extend the top type T_{⋆} to any kind K by defining inductively T_{ΠX≤A:K_{1}.K_{2}} = ΛX≤A:K_{1}.T_{K_{2}}.

𝔸 ::= X  type variable
𝔸→𝔸  function type
∀X≤𝔸:𝕂 .𝔸 polymorphic type
ΛX≤𝔸:𝕂 .𝔸 operator abstraction
𝔸 𝔸  operator application
T_{⋆}  top type

The language of terms includes the variables (x), applications (M N), and functional abstractions (λx:A.M) of the simply typed λ-calculus, as well as bounded type abstraction (λX≤A:K.M) and application (M A) of F^{ω}. As in F_{≤}, each type variable is given an upper bound at the point where it is introduced. We use the same notation for capture-avoiding substitution as that for types, and again identify α-equivalent terms.

𝕄 ::= x  variable
λx:𝔸.𝕄  abstraction
𝕄 𝕄  application
λX≤𝔸:𝕂 .𝕄 type abstraction
𝕄 𝔸  type application

The operational semantics of F_{≤}^{ω} is given by the following reduction rules on terms and types.

Definition 2.1 (Untyped Reduction)

1. (λx:A.e_{1})e_{2} →_{β}_{1} e_{1}[x←e_{2}]

2. (λX≤A:K_{1}.e)B →_{β}_{1} e[X←B]

3. (ΛX≤A:K.B)C →_{β}_{2} B[X←C]

Each relation (→_{β}_{1} and →_{β}_{2}) is extended to a compatible relation with respect to term or type formation. The reduction →_{β} is defined by →_{β}_{1} ∪ →_{β}_{2}. We write ↠_{R} for the transitive and reflexive closure of →_{R} and =_{R} for the least equivalence relation containing →_{R}. The β_{2}-normal form of a type A is written nf(A).

2.2 Contexts

A context Γ is a finite sequence of typing and subtyping assumptions for a set of term and type variables.

The empty context is written ∅. Term variable bindings have the form x:A; type variable bindings have the form X≤A:K, where A is the upper bound of X and K is the kind of A.

Γ ::= ∅  empty context
Γ, x:A  term variable declaration
Γ, X≤A:K type variable declaration

We call the set of term and type variables defined in a context Γ the domain of Γ, written dom(Γ). The functions FV(—) gives the set of free term variables and free type variables of a term, type, context, or statement. Since we are careful to ensure that no variable is bound more than once, we sometimes abuse notation and consider contexts as finite functions: Γ(X) yields the bound of X in Γ, where X is implicitly asserted to be in dom(Γ).

We now give the rules of inference for the system F_{≤}^{ω}.

2.3 Structural Rules

This section presents general structural rules for F_{≤}^{ω}. In fact, each of the rules is admissible, which we shall show when we prove the equivalence of this system with the typed operational semantics.

\frac{Γ ⊢ A : ⋆  Γ ⊢ J  x ∉ dom(Γ)}{Γ, x:A ⊢ J}  (Weak)

\frac{Γ ⊢ J  Γ ⊢ A : K  X ∉ dom(Γ)}{Γ, X≤A:K ⊢ J}  (TWeak)

\frac{Γ_{1}, X≤B:K, Γ_{2} ⊢ J  Γ_{1} ⊢ A≤B : K}{Γ_{1}, Γ_{2}[X←A] ⊢ J[X←A]}  (Subst)

\frac{Γ_{1}, x:A, Γ_{2} ⊢ J  Γ_{1} ⊢ A =_{β} B : ⋆}{Γ_{1}, X:B, Γ_{2} ⊢ J}  (Context-EQ)

\frac{Γ_{1}, X≤A:K, Γ_{2} ⊢ J  Γ_{1} ⊢ A =_{β} B : K  Γ_{1} ⊢ K =_{β} K′}{Γ_{1}, X≤B:K′, Γ_{2} ⊢ J}  (Context-T-EQ)

\frac{Γ ⊢ B : K}{Γ ⊢ K}  (Kind-Agreement)

2.4 Context Formation

The context formation rules are:

∅ ⊢ ok  (C-Empty)
\frac{Γ ⊢ A : ⋆  x ∉ dom(Γ)}{Γ, x:A ⊢ ok}  (C-Var)

\frac{Γ ⊢ A : K  X ∉ dom(Γ)}{Γ, X≤A:K ⊢ ok}  (C-TVar)

2.5 Kind Formation

The well-formed kinds are those derived with the following rules.

\frac{Γ ⊢ ok}{Γ ⊢ ⋆}  (K-⋆)
\frac{Γ, X≤A:K_{1} ⊢ K_{2}}{Γ ⊢ ΠX≤A:K_{1}.K_{2}}  (K-Π)

2.6 Kind Equality

The interconvertibility of kinds is the propagation of the interconvertibility of types within kinds.

2 SYNTAX 10

\frac{Γ ⊢ K}{Γ ⊢ K =_{β} K}  (K-Eq-Refl)

\frac{Γ ⊢ K =_{β} K′}{Γ ⊢ K′ =_{β} K}  (T-Eq-Sym)

\frac{Γ ⊢ K =_{β} K′  Γ ⊢ K′ =_{β} K′′}{Γ ⊢ K =_{β} K′′}  (T-Eq-Trans)

\frac{Γ ⊢ ok}{Γ ⊢ ⋆ =_{β} ⋆}  (K-Eq-⋆)

\frac{Γ ⊢ K_{1} =_{β} K′_{1}  Γ ⊢ A =_{β} A′ : K_{1}  Γ, X≤A:K_{1} ⊢ K_{2} =_{β} K′_{2}}{Γ ⊢ ΠX≤A:K_{1}.K_{2} =_{β} ΠX≤A′:K′_{1}.K′_{2}}  (K-Eq-Π)

2.7 Type Formation

For each type constructor, we give a rule specifying how it can be used to build well-formed type expressions. The new rules for type formation are the ones that deal with bounded type abstraction (T-TAbs), type application (T-TApp), and kind conversion (T-Conv).

\frac{Γ ⊢ ok}{Γ ⊢ T_{⋆} : ⋆}  (T-Top)
\frac{Γ_{1}, X≤A:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤A:K, Γ_{2} ⊢ X : K}  (T-TVar)
\frac{Γ ⊢ A_{1} : ⋆  Γ ⊢ A_{2} : ⋆}{Γ ⊢ A_{1}→A_{2} : ⋆}  (T-Arrow)
\frac{Γ, X≤A_{1}:K ⊢ A_{2} : ⋆}{Γ ⊢ ∀X≤A_{1}:K.A_{2} : ⋆}  (T-All)
\frac{Γ, X≤A_{1}:K_{1} ⊢ A_{2} : K_{2}}{Γ ⊢ ΛX≤A_{1}:K_{1}.A_{2} : ΠX≤A_{1}:K_{1}.K_{2}}  (T-TAbs)
\frac{Γ ⊢ A : ΠX≤B:K_{1}.K_{2}  Γ ⊢ C≤B : K_{1}}{Γ ⊢ A C : K_{2}[X←C]}  (T-TApp)

\frac{Γ ⊢ A : K  Γ ⊢ K =_{β} K′}{Γ ⊢ A : K′}  (T-Conv)

2.8 Type Equality

The judgemental type equality is generated by the typed beta-equality rule (T-Eq-Beta). It is a congruence with respect to type formation and incorporates kind equivalence so that equal kinds contain the same equality relation on types.

\frac{Γ, X≤A_{1}:K_{1} ⊢ A_{2} : K_{2}  Γ ⊢ C ≤ A_{1} : K_{1}}{Γ ⊢ (ΛX≤A_{1}:K_{1}.A_{2}) C =_{β} A_{2}[X←C] : K_{2}[X←C]}  (T-Eq-Beta)

2 SYNTAX 11

\frac{Γ ⊢ A : K}{Γ ⊢ A =_{β} A : K}  (T-Eq-Refl)

\frac{Γ ⊢ A =_{β} B : K}{Γ ⊢ B =_{β} A : K}  (T-Eq-Sym)

\frac{Γ ⊢ A =_{β} B : K  Γ ⊢ B =_{β} C : K}{Γ ⊢ A =_{β} C : K}  (T-Eq-Trans)

\frac{Γ ⊢ A_{1} =_{β} B_{1} : ⋆  Γ ⊢ A_{2} =_{β} B_{2} : ⋆}{Γ ⊢ A_{1}→A_{2} =_{β} B_{1}→B_{2} : ⋆}  (T-Eq-Arrow)

\frac{Γ ⊢ A_{1} =_{β} B_{1} : K  Γ, X≤A_{1}:K ⊢ A_{2} =_{β} B_{2} : ⋆  Γ ⊢ K =_{β} K′}{Γ ⊢ ∀X≤A_{1}:K.A_{2} =_{β} ∀X≤B_{1}:K′.B_{2} : ⋆}  (T-Eq-All)

\frac{Γ ⊢ A_{1} =_{β} B_{1} : K_{1}  Γ, X≤A_{1}:K_{1} ⊢ A_{2} =_{β} B_{2} : K_{2}  Γ ⊢ K_{1} =_{β} K′_{1}}{Γ ⊢ ΛX≤A_{1}:K_{1}.A_{2} =_{β} ΛX≤B_{1}:K′_{1}.B_{2} : ΠX≤A_{1}:K_{1}.K_{2}}  (T-Eq-TAbs)

\frac{Γ ⊢ A =_{β} B : ΠX≤E:K_{1}.K_{2}  Γ ⊢ C =_{β} D : K_{1}  Γ ⊢ C ≤ E : K_{1}}{Γ ⊢ A C =_{β} B D : K_{2}[X←C]}  (T-Eq-TApp)

\frac{Γ ⊢ A =_{β} B : K  Γ ⊢ K =_{β} K′}{Γ ⊢ A =_{β} B : K′}  (T-Eq-Conv)

2.9 Subtyping

The subtyping rules are those of F_{<:}^{ω} [11, 13, 12, 31, 14], except for those dealing with bounded type abstraction and type application shown below and the rule for subtyping the quantifier. We chose the Cardelli and Wegner’s kernel Fun rule for quantifiers with equal bounds [15]. The contravariant rule for quantifiers renders the system undecidable, and transitivity elimination in the presence of such a rule in the higher-order case remains an open problem.

\frac{Γ ⊢ A : K}{Γ ⊢ A ≤ T_{K} : K}  (S-Top)
\frac{Γ ⊢ A =_{β} B : K}{Γ ⊢ A ≤ B : K}  (S-Conv)
\frac{Γ ⊢ A ≤ B : K  Γ ⊢ B ≤ C : K}{Γ ⊢ A ≤ C : K}  (S-Trans)
\frac{Γ_{1}, X≤A:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤A:K, Γ_{2} ⊢ X ≤ A : K}  (S-TVar)
\frac{Γ ⊢ B_{1} ≤ A_{1} : ⋆  Γ ⊢ A_{2} ≤ B_{2} : ⋆}{Γ ⊢ A_{1}→A_{2} ≤ B_{1}→B_{2} : ⋆}  (S-Arrow)
\frac{Γ, X≤C:K ⊢ A ≤ B : ⋆}{Γ ⊢ ∀X≤C:K.A ≤ ∀X≤C:K.B : ⋆}  (S-All)

\frac{Γ, X≤C:K_{1} ⊢ A ≤ B : K_{2}}{Γ ⊢ ΛX≤C:K_{1}.A ≤ ΛX≤C:K_{1}.B : ΠX≤C:K_{1}.K_{2}}  (S-TAbs)

\frac{Γ ⊢ A ≤ B : ΠX≤D:K_{1}.K_{2}  Γ ⊢ C ≤ D : K_{1}}{Γ ⊢ A C ≤ B C : K_{2}[X←C]}  (S-TApp)

\frac{Γ ⊢ A ≤ B : K  Γ ⊢ K =_{β} K′}{Γ ⊢ A ≤ B : K′}  (S-K-Conv)

2.10 Term Formation

The term formation rules are those of the second-order calculus of bounded quantification with the difference that we include kind annotations in terms, types, contexts, and subtyping judgements.

\frac{Γ_{1}, x:A, Γ_{2} ⊢ ok}{Γ_{1}, x:A, Γ_{2} ⊢ x : A}  (t-Var)

\frac{Γ, x:A ⊢ M : B}{Γ ⊢ λx:A.M : A→B}  (t-Abs)
\frac{Γ ⊢ M : A→B  Γ ⊢ N : A}{Γ ⊢ M N : B}  (t-App)
\frac{Γ, X≤A:K ⊢ M : B}{Γ ⊢ λX≤A:K.M : ∀X≤A:K.B}  (t-TAbs)

\frac{Γ ⊢ M : ∀X≤A:K.B  Γ ⊢ C ≤ A : K}{Γ ⊢ M C : B[X←C]}  (t-TApp)

\frac{Γ ⊢ M : A  Γ ⊢ A ≤ B : ⋆}{Γ ⊢ M : B}  (t-Sub)

3 The Typed Operational Semantics

The typed operational semantics for F_{≤}^{ω} is organized in five judgement forms.

Γ ⊢_{S} ok  well-formed context
Γ ⊢_{S} K ↠_{n} K′  kind normalization
Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K type reduction
Γ ⊢_{S} A ≤_{W} B : K  weak-head subtyping
Γ ⊢_{S} A ≤ B : K  subtyping

The informal meaning of these judgements is as follows. In Γ ⊢_{S} K ↠_{n} K′, K′ is the normal form of K. In Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K, B is the weak head normal form of A and C its normal form. In Γ ⊢_{S} A ≤_{W} B : K, A and B are in weak head normal form, and in Γ ⊢_{S} A ≤ B : K, A and B are arbitrary types or type operators.

Definition 3.1 (Weak-Head Normal)

T_{⋆}, A_{1}→A_{2}, ∀X≤A:K.B, and ΛX≤A:K.B are weak head normal. X(A_{1}, …, A_{n}) is weak head normal if A_{1}, …, A_{n} are in normal form. In order to prove the admissibility of transitivity in the semantics, we need to consider

a stronger definition of weak head normal form. We consider expressions of the form X(A_{1}, …, A_{n}) weak head normal only if each A_{i} is fully normalized. It may be possible to strengthen the model in Section 5 and use the standard definition of this notion instead.

We use the following notations:

• Γ ⊢_{S} A : K is notation for Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K, for some B, C.

• Γ ⊢_{S} K is notation for Γ ⊢_{S} K ↠_{n} K′, for some K′.

• Γ ⊢_{S} A _{w}↠_{n} B : K is notation for Γ ⊢_{S} A ↠_{w} A _{w}↠_{n} B : K.

• Γ ⊢_{S} A ↠_{w} B : K is notation for Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K, for some C.

• Γ ⊢_{S} A ↠_{n} B : K means Γ ⊢_{S} A ↠_{w} C _{w}↠_{n} B : K, for some C.

• Γ ⊢_{S} A, B ↠_{n} C : K means Γ ⊢_{S} A ↠_{n} C : K and Γ ⊢_{S} B ↠_{n} C : K.

• Γ ⊢_{S} K, K′ ↠_{n} K′′ means Γ ⊢_{S} K ↠_{n} K′′ and Γ ⊢_{S} K′ ↠_{n} K′′. The rules are presented as simultaneously defined inductive relations.

3.1 Context Formation

∅ ⊢_{S} ok  (SC-Empty)
\frac{Γ ⊢_{S} A : ⋆  x ∉ dom(Γ)}{Γ, x:A ⊢_{S} ok}  (SC-Var)
\frac{Γ ⊢_{S} A : K′  Γ ⊢_{S} K ↠_{n} K′  X ∉ dom(Γ)}{Γ, X≤A:K ⊢_{S} ok}  (SC-TVar)

3.2 Kind Normalization

\frac{Γ ⊢_{S} ok}{Γ ⊢_{S} ⋆ ↠_{n} ⋆}  (SK-⋆)
\frac{Γ ⊢_{S} K_{1} ↠_{n} K′_{1}  Γ ⊢_{S} A ↠_{n} B : K′_{1}  Γ, X≤A : K_{1} ⊢_{S} K_{2} ↠_{n} K′_{2}}{Γ ⊢_{S} ΠX≤A:K_{1}.K_{2} ↠_{n} ΠX≤B:K′_{1}.K′_{2}}  (SK-Π)

Context formation and kind normalization rules follow from modifications to the context formation and kind equality rules of the system in Section 2.2. For example, in the type variable rule (ST-TVar) the kind of A and the kind in the declaration of X are β-equal but not necessarily identical.

3 THE TYPED OPERATIONAL SEMANTICS 14

3.3 Type Reduction

\frac{Γ ⊢_{S} ok}{Γ ⊢_{S} T_{⋆} ↠_{w} T_{⋆} _{w}↠_{n} T_{⋆} : ⋆}  (ST-Top)

\frac{Γ ⊢_{S} A : K′  Γ ⊢_{S} K ↠_{n} K′  (X≤A : K) ∈ Γ}{Γ ⊢_{S} X ↠_{w} X _{w}↠_{n} X : K′}  (ST-TVar)

\frac{Γ ⊢_{S} A ↠_{w} D : ΠX≤C:K_{1}.K_{2} Γ ⊢_{S} B ↠_{w} E _{w}↠_{n} F : K_{1}  \begin{matrix}Γ ⊢_{S} E ≤_{W} C : K_{1} \\ Γ ⊢_{S} K_{2}[X←B] ↠_{n} K \end{matrix} D ≠ ΛY ≤G:K_{3}.H}{Γ ⊢_{S} A B ↠_{w} D F _{w}↠_{n} D F : K} (ST-TApp)

\frac{Γ ⊢_{S} A_{1} ↠_{n} B_{1} : ⋆  Γ ⊢_{S} A_{2} ↠_{n} B_{2} : ⋆}{Γ ⊢_{S} (A_{1}→A_{2}) ↠_{w} (A_{1}→A_{2}) _{w}↠_{n} (B_{1}→B_{2}) : ⋆}  (ST-Arrow)

\frac{Γ ⊢_{S} A ↠_{n} C : K′  Γ, X≤A:K ⊢_{S} B ↠_{n} D : ⋆  Γ ⊢_{S} K ↠_{n} K′}{Γ ⊢_{S} ∀X≤A:K.B ↠_{w} ∀X≤A:K.B _{w}↠_{n} ∀X≤C:K′.D : ⋆}  (ST-All)

\frac{Γ ⊢_{S} K_{1} ↠_{n} K′_{1}  Γ ⊢_{S} A ↠_{n} C : K′_{1}  Γ, X≤A:K_{1} ⊢_{S} B ↠_{n} D : K_{2}}{Γ ⊢_{S} ΛX≤A:K_{1}.B ↠_{w} ΛX≤A:K_{1}.B _{w}↠_{n} ΛX≤C:K′_{1}.D : ΠX≤C:K′_{1}.K_{2}}  (ST-TAbs)

\frac{Γ ⊢_{S} B ↠_{w} ΛX≤A:K_{1}.D : ΠX≤A′:K′_{1}.K_{2} Γ ⊢_{S} D[X←C] ↠_{w} E _{w}↠_{n} F : K  \begin{matrix}Γ ⊢_{S} K_{2}[X←C] ↠_{n} K \\ Γ ⊢_{S} C ≤ A : K_{1}′ \end{matrix}}{Γ ⊢_{S} B C ↠_{w} E _{w}↠_{n} F : K}  (ST-Beta)

The rules for type reduction combine kinding information and computational behavior in the form of weak head and β-normal forms. For example, the rule for arrow types says how to obtain the weak head and β-normal form of (A_{1}→A_{2}) in ⋆ knowing those for A_{1} and A_{2} in ⋆ as well.

The beta rule, besides uncovering the outermost redex of the application B C, and contracting it, finds the weak head normal form E and the normal form F. The premise Γ ⊢_{S} K_{2}[X←C] ↠_{w} K ensures that E and F have β-equal kinds, and the subtyping premise Γ ⊢_{S} C ≤ A : K_{1}′ enforces the well-formation of B C.

The subtyping relation is defined using two judgements: one deals with types in weak head normal form (Γ ⊢_{S} A ≤_{W} B : K) and the other with arbitrary types (Γ ⊢_{S} A ≤ B : K).

3.4 Weak Head Subtyping

\frac{Γ ⊢_{S} A _{w}↠_{n} B : ⋆  HV(A) undefined}{Γ ⊢_{S} A ≤_{W} T_{⋆} : ⋆}  (SWS-Top)

\frac{Γ ⊢_{S} X(A_{1}, …, A_{m}) _{w}↠_{n} C : K Γ ⊢_{S} Γ(X) ↠_{n} B : K′ Γ ⊢_{S} B(A_{1}, …, A_{m}) ↠_{w} E : K  \begin{matrix}Γ ⊢_{S} E ≤_{W} A : K \\ A ≠ X(A_{1}, …, A_{m}) \end{matrix}}{Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤_{W} A : K}  (SWS-TApp)

4 METATHEORY FOR F_{≤}^{ω} 15

\frac{Γ ⊢_{S} X(A_{1}, …, A_{m}) _{w}↠_{n} B : K}{Γ ⊢_{S} X(A_{1}, …, A_{m}) ≤_{W} X(A_{1}, …, A_{m}) : K}  (SWS-Refl)

\frac{Γ ⊢_{S} B_{1} ≤ A_{1} : ⋆  Γ ⊢_{S} A_{2} ≤ B_{2} : ⋆}{Γ ⊢_{S} A_{1}→A_{2} ≤_{W} B_{1}→B_{2} : ⋆}  (SWS-Arrow)

\frac{\begin{matrix}Γ, X≤A_{1}:K ⊢_{S} A_{2} ≤ B_{2} : ⋆ \\ Γ ⊢_{S} A_{1}, B_{1} ↠_{n} C : K′′ \end{matrix}  Γ ⊢_{S} K, K′ ↠_{n} K′′}{Γ ⊢_{S} ∀X≤A_{1}:K.A_{2} ≤_{W} ∀X≤B_{1}:K′.B_{2} : ⋆}  (SWS-All)

\frac{Γ, X≤A_{1}:K_{1} ⊢_{S} A_{2} ≤ B_{2} : K_{2}  \begin{matrix}Γ ⊢_{S} K_{1}, K′_{1} ↠_{n} K′′_{1} \\ Γ ⊢_{S} A_{1}, B_{1} ↠_{n} C : K′′_{1} \end{matrix}}{Γ ⊢_{S} ΛX≤A_{1}:K_{1}.A_{2} ≤_{W} ΛX≤B_{1}:K′_{1}.B_{2} : ΠX≤C:K′′_{1}.K_{2}}  (SWS-TAbs)

The weak head subtyping rules are motivated by the algorithmic rules in [17]. The rules SWS-Arrow, SWS-All, and SWS-TAbs are structural. The rule for the maximal type T_{⋆} has a side condition to ensure that the algorithm is deterministic, and applications are only handled by SWS-TApp or SWS-Refl.

A particular instance of SWS-TApp is the rule for type variables. To check if Γ ⊢_{S} X ≤_{W} A : K, we have to check that the bound of X in Γ is a subtype of A, Γ ⊢_{S} Γ(X) ≤ A : K, and since we know that A is in weak head normal form we save a recursive call of SS-Inc and normalize Γ(X) in a premise. The side condition A ≢ X is to ensure determinism; if A ≡ X, it follows by reflexivity.

3.5 Subtyping

\frac{Γ ⊢_{S} A ↠_{w} C : K  Γ ⊢_{S} B ↠_{w} D : K  Γ ⊢_{S} C ≤_{W} D : K}{Γ ⊢_{S} A ≤ B : K}  (SS-Inc)

There is no rule for transitivity of subtyping in the semantic rules, but transitivity is a property of the “operational” subtyping (Lemma 4.21). Moreover, the rule SWS-TApp includes a step of transitivity along the bound of a variable in the context. We interleave weak head normalization steps in the subtyping algorithm via SS-Inc. An alternative formulation would weak head normalize the arguments of the hypothesis.

4 Metatheory for F_{≤}^{ω}

In this section we prove fundamental properties about F_{≤}^{ω}. We begin with results about the typed operational semantics and then show some basic results needed for the soundness proof for the system F_{≤}^{ω}.

4.1 Metatheory for the Typed Operational Semantics

Here, the typed operational semantics is playing the same role as the algorithm in the usual development of the metatheory, but it also allows us to show results such as subject 4 METATHEORY FOR F_{≤}^{ω} 16

reduction and strong normalization for types. Definition 4.1 (Closed)

1. A term M is closed with respect to a context Γ if FV(M) ∪ FTV(M) ⊆ dom(Γ).

2. A type A is closed with respect to a context Γ if FTV(A) ⊆ dom(Γ).

Judgements are closed if each of the terms to the right of the turnstile is closed with respect to the context. Lemma 4.2 (Closure) If Γ ⊢_{S} J then Γ ⊢_{S} J is closed. Lemma 4.3 (Weak Head and Normal Forms)

1. If Γ ⊢_{S} K ↠_{n} K′ then K′ is in normal form.

2. If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K then B is in weak head normal form and C and K are

in normal form. Proof: By simultaneous induction on derivations. □ Lemma 4.4 (Context Formation) If Γ ⊢_{S} J then there is a (not necessarily strict) subderivation of Γ ⊢_{S} ok. Proof: By induction on derivations. □ Lemma 4.5 (Determinacy) If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K and Γ ⊢_{S} A ↠_{w} D _{w}↠_{n} E : K′ then B ≡ D, C ≡ E and K ≡ K′. Proof: By induction on derivations. □

As we mentioned in the introduction, we want to prove completeness with respect to a system without the structural rules in Section 2.3. We shall write Γ ⊢^{−} J for judgements in the restricted system without these rules. Proposition 4.6 (Completeness)

1. Γ ⊢_{S} ok implies Γ ⊢^{−} ok.

2. Γ ⊢_{S} K ↠_{n} K′ implies Γ ⊢^{−} K and Γ ⊢^{−} K =_{β} K′.

3. Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K implies Γ ⊢^{−} A : K, Γ ⊢^{−} A =_{β} B : K, Γ ⊢^{−} A =_{β} C : K, and Γ ⊢^{−} K =_{β} K.

4. Γ ⊢_{S} A ≤_{W} B : K implies Γ ⊢^{−} A ≤ B : K.

5. Γ ⊢_{S} A ≤ B : K implies Γ ⊢^{−} A, B : K, Γ ⊢^{−} A ≤ B : K and Γ ⊢^{−} K =_{β} K.

Proof: By simultaneous induction on derivations. We proceed by case analysis on the last rule of the derivation, presenting here a few representative cases. The hypotheses in each case are left implicit and follow exactly the notation of the rules in Section 3.

1. SC-Empty Immediate by C-Empty.

SC-Var By the induction hypothesis 3, Γ ⊢ A : ⋆ and, by C-Var, the result follows.

SC-TVar By the induction hypothesis 3,Γ ⊢ A : K′, by the induction hypothesis 2, Γ ⊢^{−} K =_{β} K′. By the symmetry of kind equality and T-Conv, Γ ⊢^{−} A : K, and, by C-TVar, the result follows.

2. SK-⋆ By the induction hypothesis 1 Γ ⊢^{−} ok. By K-⋆, Γ ⊢^{−} ⋆, and, by K-Eq-⋆, Γ ⊢^{−} ⋆ =_{β} ⋆.

SK-Π By the induction hypothesis 2, Γ, X≤A:K_{1} ⊢^{−} K_{2}, by the induction hypothesis 3, Γ ⊢^{−} A : K′_{1}. By the induction hypothesis 2, Γ ⊢^{−} K_{1} =_{β} K′_{1}. By the symmetry of kind equality and T-Conv, Γ ⊢^{−} A : K_{1}. Then, by K-Π, Γ ⊢^{−} ΠX≤A:K_{1}.K_{2}. By the induction hypothesis 3, Γ ⊢^{−} A =_{β} B : K_{1}, and by the induction hypothesis 2 Γ, X≤A:K_{1} ⊢^{−} K_{2} =_{β} K′_{2}. By K-Eq-Π, Γ ⊢^{−} ΠX≤A:K_{1}.K_{2} =_{β} ΠX≤B:K′_{1}.K′_{2}.

3. ST-TApp By the induction hypothesis 3, Γ ⊢^{−} A : ΠX≤C:K_{1}.K_{2} and Γ ⊢^{−} B =_{β} E : K_{1}. By the induction hypothesis 5, Γ ⊢^{−} E ≤ C : K_{1}. By S-Conv, Γ ⊢^{−} B ≤ E : K_{1}, and, by S-Trans, Γ ⊢^{−} B ≤ C : K_{1}. By T-TApp, Γ ⊢^{−} A B : K_{2}[X←B]. By the induction hypothesis 2, Γ ⊢^{−} K_{2}[X←B] =_{β} K, and, by T-Conv, Γ ⊢^{−} A B : K. We now have to prove that Γ ⊢^{−} A B =_{β} D F : K. By the induction hypothesis 3, Γ ⊢^{−} A =_{β} D : ΠX≤C:K_{1}.K_{2}. By T-EQ-TApp, Γ ⊢^{−} A B =_{β} D F : K_{2}[X←B], and by T-EQ-Conv, Γ ⊢^{−} A B =_{β} D F : K.

4. SWS-All By inductive hypothesis 5, Γ, X≤A_{1}:K ⊢^{−} A_{2} ≤ B_{2} : ⋆ and Γ, X≤A_{1}:K ⊢^{−} B_{2} : ⋆. Then, by S-All, Γ ⊢^{−} ∀X≤A_{1}:K.A_{2} ≤ ∀X≤A_{1}:K.B_{2} : ⋆. We now want to prove using T-EQ-All that Γ ⊢^{−} ∀X≤A_{1}:K.B_{2} ≤ ∀X≤B_{1}:K′.B_{2} : ⋆. The result then follows by S-Conv and S-Trans. For that we need:

(a) Γ, X≤A_{1}:K ⊢^{−} B_{2} =_{β} B_{2} : ⋆, which follows from T-EQ-Refl.

(b) Γ ⊢^{−} K =_{β} K′, which follows from the induction hypothesis 2, K-EQ-Sym

and K-EQ-Trans.

(c) Γ ⊢^{−} A_{1} =_{β} B_{1} : K. By the induction hypothesis 2 and K-EQ-Sym, Γ ⊢^{−} K′′ =_{β} K. By the induction hypothesis 3, Γ ⊢^{−} A_{1} =_{β} B_{1} : K′′, and

by T-EQ-Conv, Γ ⊢^{−} A_{1} =_{β} B_{1} : K.

5. SS-Inc By the induction hypothesis 3, Γ ⊢ A, B, C, D : K, Γ ⊢^{−} A =_{β} C : K, Γ ⊢^{−} B =_{β} D : K, and Γ ⊢^{−} K =_{β} K. By S-Conv, Γ ⊢^{−} A ≤ C : K and Γ ⊢^{−} D ≤ B : K, and, by the induction hypothesis 4, Γ ⊢^{−} C ≤ D : K. Finally, by S-Trans, Γ ⊢^{−} A ≤ B : K. □

In Section 5 we shall see how Soundness (Corollary 5.12) can be used together with this result to show the admissibility of the structural rules.

The following technique for proving Thinning comes from McKinna and Pollack’s development of the metatheory of Pure Type Systems [29].

Definition 4.7 (Parallel Type Substitution) A parallel type substitution γ for Γ is an assignment of types to type variables in dom(Γ). We write γ[X:=A] to extend γ to assign A to X, γ(X) for the value of the assignment at a variable, and A[γ] for the replacement of variables in A with the values in γ; the value of this is undefined if there is a variable in A not in dom(γ). We say that γ is a type substitution for Γ in Δ if Δ ⊢_{S} γ(X) ≤ A[γ] : K′, where Δ ⊢_{S} K[γ] ↠_{n} K′, for each X with Γ = Γ_{1}, X≤A : K, Γ_{2}. A renaming is a parallel type substitution of variables for variables.

Lemma 4.8 (Renaming) If Γ ⊢_{S} J and δ is a renaming for Γ in Δ then Δ ⊢_{S} J[δ].

Proof: By induction on derivations. □

We write ⊢_{S} Δ ≥ Γ if Δ ⊢_{S} ok, x:A ∈ Γ implies x:A ∈ Δ, and X≤A:K ∈ Γ implies X≤A:K ∈ Δ. Thinning, which says that judgements are monotonic with respect to context extension, now follows as a corollary of Renaming taking δ to be the identity substitution.

Corollary 4.9 (Thinning) If Γ ⊢_{S} J and ⊢_{S} Δ ≥ Γ then Δ ⊢_{S} J.

Lemma 4.10 (Adequacy)

• If Γ ⊢_{S} K ↠_{n} K′ then K ↠_{β}_{2} K′.

• If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K then A ↠_{β}_{2} B ↠_{β}_{2} C.

We use parallel reduction [28, 29] as a tool for proving subject reduction for the typed operational semantics.

Definition 4.11 (Parallel Reduction) Parallel reduction ⇒ is the least relation over types and kinds defined by the following rules of inference.

X ⇒ X  (P-Var)
\frac{A ⇒ A′  K ⇒ K′  B ⇒ B′}{ΛX≤A:K.B ⇒ ΛX≤A′:K′.B′}  (P-Lambda)

\frac{A ⇒ A′  B ⇒ B′}{A B ⇒ A′ B′}  (P-App)
\frac{A ⇒ A′  B ⇒ B′}{(ΛX≤C:K.A)(B) ⇒ A′[X←B′]}  (P-Beta)

plus similar rules, allowing reduction on each of the subterms, for the other type and kind formers.

Parallel reduction extends in the obvious way to contexts.

Parallel reduction is useful because it is closed under the following rule of substitution:

\frac{A ⇒ A′  B ⇒ B′}{A[X←B] ⇒ A′[X←B′]}  (P-Subst)

The following proof uses this and other simple properties about parallel reduction. See Takahashi’s excellent account of parallel reduction [35] for more details.

Lemma 4.12 (Parallel Subject Reduction for Types and Kinds)

• If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K, Γ ⇒ Γ′ and A ⇒ A′, then there is a B′ such that B ⇒ B′ and Γ′ ⊢_{S} A′ ↠_{w} B′ _{w}↠_{n} C : K.

• If Γ ⊢_{S} A ≤_{W} B : K, Γ ⇒ Γ′, A ⇒ A′, and B ⇒ B′ then Γ′ ⊢_{S} A′ ≤_{W} B′ : K.

• If Γ ⊢_{S} A ≤ B : K, Γ ⇒ Γ′, A ⇒ A′, and B ⇒ B′ then Γ′ ⊢_{S} A′ ≤ B′ : K.

Proof: By induction on derivations. We consider several cases:

ST-TVar Suppose Γ ⇒ Γ′ and X ⇒ B. By inversion B ≡ X. Also, clearly if (X ≤ A : K) ∈ Γ then Γ ⇒ Γ′ implies A ⇒ A′, K ⇒ K′′ and (X ≤ A′ : K′) ∈ Γ′. Hence, by inductive hypothesis Γ′ ⊢_{S} A′ : K′ and Γ′ ⊢_{S} K′′ ↠_{n} K′, so Γ′ ⊢_{S} X ↠_{w} X ↠_{n} X : K′.

ST-TApp Suppose Γ ⇒ Γ′ and A B ⇒ E. Clearly if D is not an abstraction then A is not an abstraction, so by inversion E ≡ A′ B′ with A ⇒ A′ and B ⇒ B′. Hence, by inductive hypothesis there is a D′ such that Γ′ ⊢_{S} A′ ↠_{w} D′ ↠_{n} D : ΠX≤C:K_{1}.K_{2} and D ⇒ D′, and because D is not an abstraction and D is weak head normal then D′ is not an abstraction; there is an E′ such that Γ′ ⊢_{S} B′ ↠_{w} E′ ↠_{n} F : K_{1} and E ⇒ E′; Γ′ ⊢_{S} K_{2}[X←B′] ↠_{n} K; and Γ′ ⊢_{S} E′ ≤_{W} C : K_{1}. Hence, Γ′ ⊢_{S} A′ B′ ↠_{w} D′ F ↠_{n} D′ F by ST-TApp.

ST-Beta Suppose Γ ⇒ Γ′ and B C ⇒ G. By inversion of the reduction:

• B ⇒ B′, C ⇒ C′, and G ≡ B′ C′. Then by inductive hypothesis Γ′ ⊢_{S} B′ ↠_{w} ΛX≤A′′:K′′_{1}.D′ : ΠX≤A′:K′_{1}.K_{2} with ΛX≤A:K_{1}.D ⇒ ΛX≤A′′:K′′_{1}.D′, and also Γ′ ⊢_{S} C′ ≤ A′′ : K′_{1}, Γ′ ⊢_{S} K_{2}[X←C′] ↠_{n} K, and there is an E′ such that Γ′ ⊢_{S} D′[X←C′] ↠_{w} E′ ↠_{n} F : K and E ⇒ E′. Hence Γ′ ⊢_{S} B′ C′ ↠_{w} E′ ↠_{n} F : K with E ⇒ E′.

• B ≡ ΛX≤H:K_{3}.I, I ⇒ I′, C ⇒ C′ and B C ⇒ I′[X←C′]. By inversion of the premise for B we know that H ≡ A, K_{3} ≡ K_{1} and I ≡ D. Hence D ⇒ D′ and C ⇒ C′ imply D[X←C] ⇒ D′[X←C′], so by inductive hypothesis there is an E′ such that Γ′ ⊢_{S} D′[X←C′] ↠_{w} E′ ↠_{n} F : K and E ⇒ E′.

SWS-Refl By Lemma 4.3 and the definition of weak head normal, X(A_{1}, …, A_{m}) is normal. Hence, X(A_{1}, …, A_{m}) ⇒ C implies C ≡ X(A_{1}, …, A_{m}), and by inductive hypothesis Γ ⇒ Γ′ implies Γ′ ⊢_{S} X(A_{1}, …, A_{m}) _{w}↠_{n} B : K. Hence, Γ′ ⊢_{S} C ≤_{W} D : K if X(A_{1}, …, A_{m}) ⇒ C and X(A_{1}, …, A_{m}) ⇒ D. □

It is easy to show that →_{β} is included in ⇒, and that ⇒ is included in ↠_{β}, so we have the following corollary:

Corollary 4.13 (Subject Reduction for Types and Kinds)

• If Γ ⊢_{S} ok and Γ →_{β} Γ′ then Γ′ ⊢_{S} ok.

• If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K and A →_{β} A′ then there is a B′ such that B ↠_{β} B′ and Γ ⊢_{S} A′ ↠_{w} B′ _{w}↠_{n} C : K.

• If Γ ⊢_{S} A ≤ B : K, A →_{β} A′ and B →_{β} B′ then Γ ⊢_{S} A′ ≤ B′ : K.

Notice that this corollary incorporates both Subject Reduction and Church–Rosser, because the normal form is preserved by any one-step reduction.

We now prove Strong Normalization, using Subject Reduction to help.

Definition 4.14 (Strong Normalization) Strong normalization for types, written SN(A), is the least relation closed under the following rule of inference:

\frac{for all B.(A →_{β}_{2} B) ⟹ SN(B)}{SN(A)}  (SN-i)

and similarly for kinds.

Strong normalization is easily seen to be closed under →_{β}_{2}-reduction.

Lemma 4.15 (Strong Normalization for Types and Kinds)

1. If Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K then A is strongly normalizing.

2. If Γ ⊢_{S} K ↠_{n} K′ then K is strongly normalizing.

Proof: By induction on derivations.

ST-⋆ By SN-i we need to show that if ⋆ →_{β}_{2} K′ then SN(K′), which follows because ⋆ →_{β}_{2} K′ is impossible.

ST-Π By inductive hypothesis we know that SN(A), SN(K_{1}) and SN(K_{2}). By induction on these premises we show that SN(ΠX≤A:K_{1}.K_{2}). By SN-i we need to show that if ΠX≤A:K_{1}.K_{2} →_{β}_{2} K′ then SN(K′). There are three possible reductions, corresponding to the subterms of ΠX≤A:K_{1}.K_{2}, and each of these cases follows by the appropriate inductive hypothesis.

ST-Top By SN-i and the impossibility of T_{⋆} →_{β}_{2} B.

ST-TVar By SN-i and the impossibility of X →_{β}_{2} B.

ST-TApp By inductive hypothesis we know that SN(A) and SN(B). By induction on these we show that if Γ ⊢_{S} A ↠_{w} D : ΠX≤C:K_{1}.K_{2} and D is not an abstraction then SN(A B). By SN-i we need to show that if A B →_{β}_{2} G then SN(G). Again, if D is not an abstraction then A is not an abstraction, so if A B →_{β}_{2} G then we have two cases:

• A →_{β}_{2} A′. Then by Subject Reduction (Lemma 4.13) there is a D′ such that Γ ⊢_{S} A′ ↠_{w} D′ : ΠX≤C:K_{1}.K_{2} and D ⇒ D′. Clearly if Γ ⊢_{S} A ↠_{w} D : ΠX≤C:K_{1}.K_{2}, D is not an abstraction and D ⇒ D′ then D′ is not an abstraction. Hence, by inductive hypothesis we know SN(A′ B).

• B →_{β}_{2} B′. This follows directly by inductive hypothesis.

ST-Arrow By inductive hypothesis we know SN(A_{1}) and SN(A_{2}). By induction on these we show SN(A_{1}→A_{2}). By SN-i we need to show that if A_{1}→A_{2} →_{β}_{2} C then SN(C). By inversion either A_{1} →_{β}_{2} C_{1} or A_{2} →_{β}_{2} C_{2}, and each case follows by the inductive hypothesis.

ST-TAll Similar to the case for ST-Π.

ST-TAbs Similar to the case for ST-Π.

ST-Beta By inductive hypothesis we know that SN(B), SN(C), and SN(D[X←C]). By induction on SN(B) and SN(C) we show that Γ ⊢_{S} B ↠_{w} ΛX≤A:K_{1}.D : ΠX≤A′:K′_{1}.K_{2} and SN(D[X←C]) imply SN(B C). By SN-i, we need B C →_{β}_{2} G implies SN(G). By inversion of B C →_{β}_{2} G there are three cases:

• B →_{β}_{2} B′. Then by Subject Reduction (Lemma 4.13) there is an H such that Γ ⊢_{S} B′ ↠_{w} H : ΠX≤A′:K′_{1}.K_{2} and ΛX≤A:K_{1}.D ⇒ H. By inversion H ≡ ΛX≤A′′:K′′_{1}.D′ with A ⇒ A′′, K_{1} ⇒ K′′_{1} and D ⇒ D′. Because SN is closed under reduction we know SN(D′[X←C]). Hence SN(B′ C) by inductive hypothesis.

• C →_{β}_{2} C′. Then since SN is closed under reduction SN(D[X←C′]), so by inductive hypothesis SN(B C′).

• B ≡ ΛX≤A′′:K′′_{1}.H and B C →_{β}_{2} H[X←C]. By inversion of Γ ⊢_{S} B ↠_{w} ΛX≤A:K_{1}.D : ΠX≤A′:K′_{1}.K_{2} we know that B ≡ ΛX≤A:K_{1}.D, so in particular H ≡ D. Hence SN(H[X←C]) follows by assumption. □

Definition 4.16 We define conversion of contexts, written ⊢_{S} Γ; Δ ↠_{n} Φ, as the least relation closed under the following rules of inference:

⊢_{S} ∅; ∅ ↠_{n} ∅  (SCN-Empty)
\frac{⊢_{S} Γ; Δ ↠_{n} Φ  Γ ⊢_{S} A, B ↠_{n} C : ⋆  x ∉ dom(Γ)}{⊢_{S} Γ, x:A; Δ, x:B ↠_{n} Φ, x:C}  (SCN-Var)

\frac{⊢_{S} Γ; Δ ↠_{n} Φ  Γ ⊢_{S} K, K′ ↠_{n} K′′  Γ ⊢_{S} A, B ↠_{n} C : K′′ X ∉ dom(Γ)}{⊢_{S} Γ, X≤A:K; Δ, X≤B:K′ ↠_{n} Φ, X≤C:K′′}

(SCN-TVar)

Lemma 4.17 (Context Conversion) If ⊢_{S} Γ, Δ ↠_{n} Φ and Γ ⊢_{S} J then Δ ⊢_{S} J.

Proof: By induction on derivations. We consider two representative cases:

ST-TVar We know that (X≤A : K) ∈ Γ, so by inversion of Γ; Δ ↠_{n} Φ we know that there are Γ_{0}, Γ_{1}, Δ_{0} and Δ_{1} such that Γ ≡ Γ_{0}, X≤A : K, Γ_{1} and Δ ≡ Δ_{0}, X≤B : K′′, Δ_{1}, where Γ_{0} ⊢_{S} A ↠_{n} C : K′′′, Γ_{0} ⊢_{S} K ↠_{n} K′′′, Δ_{0} ⊢_{S} B ↠_{n} C : K′′′, and Δ_{0} ⊢_{S} K′′ ↠_{n} K′′′. By Renaming Γ ⊢_{S} K ↠_{n} K′′′, Δ ⊢_{S} K′′ ↠_{n} K′′′, and Δ ⊢_{S} B ↠_{n} C : K′′′. We have a premise that Γ ⊢_{S} K ↠_{n} K′, so by Determinacy K′ ≡ K′′′, so Δ ⊢_{S} X ↠_{w} X ↠_{n} X : K′.

ST-TAbs By inductive hypothesis Δ ⊢_{S} A ↠_{n} C : K′_{1} and Δ ⊢_{S} K_{1} ↠_{n} K′_{1}. Hence ⊢_{S} Γ, X≤A : K_{1}; Δ, X≤B : K_{1} ↠_{n} Φ, X≤C : K′_{1}, and so by inductive hypothesis Δ, X≤A : K_{1} ⊢_{S} B ↠_{n} D : K_{2}. The result follows by ST-TAbs. □

Lemma 4.18 (Subtyping Conversion)

• Suppose that Γ ⊢_{S} A ≤_{W} B : K. Then:

– If Γ ⊢_{S} A, A′ _{w}↠_{n} C : K then Γ ⊢_{S} A′ ≤_{W} B : K.

– If Γ ⊢_{S} B, B′ _{w}↠_{n} C : K then Γ ⊢_{S} A ≤_{W} B′ : K.

• Suppose that Γ ⊢_{S} A ≤ B : K. Then:

– If Γ ⊢_{S} A, A′ ↠_{n} C : K then Γ ⊢_{S} A′ ≤ B : K.

– If Γ ⊢_{S} B, B′ ↠_{n} C : K then Γ ⊢_{S} A ≤ B′ : K.

Proof: By induction on derivations. We show two interesting cases:

SWS-All We consider the case that Γ ⊢_{S} ∀X≤A_{1}:K.A_{2}, A′ _{w}↠_{n} D : ⋆, where the other case is similar but simpler. By inversion on the derivation for ∀X≤A_{1}:K.A_{2} we know that D ≡ ∀X≤C_{1}:K′′′.C_{2} with Γ ⊢_{S} A_{1} ↠_{n} C_{1} : K′′′, Γ ⊢_{S} K ↠_{n} K′′′ and Γ, X≤A_{1} : K ⊢_{S} A_{2} ↠_{n} C_{2} : ⋆. By Determinacy K′′ ≡ K′′′ and C ≡ C_{1}. By inversion on the derivation that Γ ⊢_{S} A′ _{w}↠_{n} ∀X≤C_{1}:K′′′.C_{2} : ⋆ we know that A′ ≡ ∀X≤A′_{1}:K′′′′.A′_{2}, Γ ⊢_{S} A′_{1} ↠_{n} C_{1} : K′′, Γ ⊢_{S} K′′′′ ↠_{n} K′′ and Γ, X≤A′_{1} : K′′′′ ⊢_{S} A′_{2} ↠_{n} C_{2} : ⋆. By Context Conversion we know that Γ, X≤A_{1} : K ⊢_{S} A′_{2} ↠_{n} C_{2} : ⋆, so by inductive hypothesis Γ, X≤A_{1} : K ⊢_{S} A′_{2} ≤ B_{2} : ⋆. Finally, by Context Conversion again Γ, X≤A′_{1} : K′′′′ ⊢_{S} A′_{2} ≤ B_{2} : ⋆, and the result follows by

SWS-All.

SS-Inc We consider the case that Γ ⊢_{S} A ↠_{w} C′ _{w}↠_{n} E : K and Γ ⊢_{S} A′ ↠_{w} C′′ _{w}↠_{n} E : K, where the other case is similar. We know C ≡ C′ by Determinacy. Furthermore, by Adequacy and Subject Reduction Γ ⊢_{S} C, C′′ _{w}↠_{n} E : K, so by inductive hypothesis Γ ⊢_{S} C′′ ≤_{W} D : K. Hence Γ ⊢_{S} A′ ≤ B : K by SS-Inc. □

Lemma 4.19 If Γ ⊢_{S} A ≤_{W} B : K then there is a C such that Γ ⊢_{S} A _{w}↠_{n} C : K.

Proof: By inversion of Γ ⊢_{S} A ≤_{W} B : K, also using inversion on the premises for

SWS-Arrow, SWS-All and SWS-TAbs. □

Lemma 4.20 (Reflexivity) If Γ ⊢_{S} A ↠_{n} B : K then Γ ⊢_{S} A ≤ A : K.

Proof: We show the stronger property, that if Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K then Γ ⊢_{S} B ≤_{W} B : K and Γ ⊢_{S} A ≤ A : K, by induction on derivations. □

Lemma 4.21 (Transitivity) If Γ ⊢_{S} A ≤ B : K and Γ ⊢_{S} B ≤ C : K then Γ ⊢_{S} A ≤ C : K.

Proof: We show the stronger property that:

• if Γ ⊢_{S} B ≤ C : K then:

1. if Γ ⊢_{S} A ≤ B : K then Γ ⊢_{S} A ≤ C : K, and

2. if Γ ⊢_{S} C ≤ D : K then Γ ⊢_{S} B ≤ D : K, and

• if Γ ⊢_{S} B ≤_{W} C : K then:

1. if Γ ⊢_{S} A ≤_{W} B : K then Γ ⊢_{S} A ≤_{W} C : K, and

2. if Γ ⊢_{S} C ≤_{W} D : K then Γ ⊢_{S} B ≤_{W} D : K.

by induction on derivations. We show several cases:

SWS-Top Case 1 follows by Lemma 4.19 and SWS-Top, and Case 2 follows by inversion on derivations such that Γ ⊢_{S} T_{⋆} ≤_{W} D : ⋆.

SWS-Arrow

1. Suppose Γ ⊢_{S} C ≤_{W} A_{1}→A_{2} : ⋆. By induction on this we show that Γ ⊢_{S} C ≤_{W} B_{1}→B_{2} : ⋆.

SWS-TApp By the second inductive hypothesis and SWS-TApp.

SWS-Arrow We have that C ≡ C_{1}→C_{2} and that Γ ⊢_{S} C ≤_{W} A_{1}→A_{2} : ⋆ by Γ ⊢_{S} A_{1} ≤ C_{1} : ⋆ and Γ ⊢_{S} C_{2} ≤ A_{2} : ⋆. By the first inductive hypothesis Case 2 Γ ⊢_{S} B_{1} ≤ C_{1} : ⋆, and by the first inductive hypothesis Case 1 Γ ⊢_{S} C_{2} ≤ B_{2} : ⋆. Hence Γ ⊢_{S} C_{1}→C_{2} ≤_{W} B_{1}→B_{2} : ⋆ by SWS-Arrow.

4 METATHEORY FOR F_{≤}^{ω} 24

2. Suppose Γ ⊢_{S} B_{1}→B_{2} ≤_{W} C : ⋆. By inversion on this we show that Γ ⊢_{S}

A_{1}→A_{2} ≤_{W} C : ⋆.

SWS-Top Then Γ ⊢_{S} A_{1}→A_{2} _{w}↠_{n} D : ⋆ by Lemma 4.19, so Γ ⊢_{S} A_{1}→A_{2} ≤_{W}

T_{⋆} : ⋆ by SWS-Top.

SWS-Arrow We know that Γ ⊢_{S} C_{1} ≤ B_{1} : ⋆ and Γ ⊢_{S} B_{2} ≤ C_{2} : ⋆. Hence by inductive hypothesis Case 1 Γ ⊢_{S} C_{1} ≤ A_{1} : ⋆, and by the first inductive hypothesis Case 2 Γ ⊢_{S} A_{2} ≤ C_{2} : ⋆, and so Γ ⊢_{S} A_{1}→A_{2} ≤_{W} C_{1}→C_{2} : ⋆

by SWS-Arrow.

SS-Inc Both cases follow by inversion of the assumption, Determinacy, the appropriate inductive hypothesis for ≤_{W} and SS-Inc. □

4.2 Basic Properties For F_{≤}^{ω}

Lemma 4.22 If Γ ⊢ ok then all variables in dom(Γ) are different. Proof: By induction on the structure of Γ. □ Lemma 4.23 If Γ ⊢ J and Γ′ is a prefix of Γ, then Γ′ ⊢ ok. Proof: By induction on the derivation of Γ ⊢ J. □ Lemma 4.24 (Strengthening) If Γ_{1}, y:C, Γ_{2} ⊢ J and y ∉ FV(J) then Γ_{1}, Γ_{2} ⊢ J. Proof: By induction on the derivation of Γ_{1}, y:C, Γ_{2} ⊢ J. Most cases follow by the induction hypothesis and the corresponding rule, and C-Var uses Lemma 4.23. □ Lemma 4.25 If Y ∉ FV(A) then B[X←C][Y ←A[X←C]] = B[Y ←A][X←C]. Proof: By induction on the structure of B. □ Lemma 4.26 (Term Substitution)

1. If Γ_{1}, x:A, Γ_{2} ⊢ M : B and Γ_{1} ⊢ N : A then Γ_{1}, Γ_{2} ⊢ M[x←N] : B.

2. If Γ_{1}, X≤A:K, Γ_{2} ⊢ M : B and Γ_{1} ⊢ C ≤ A then Γ_{1}, Γ_{2}[X←C] ⊢ M[X←C] :

B[X←C]. Proof:

1. By induction on derivations, where for t-Var we use Weakening (Corollary 4.9) and Strengthening (Lemma 4.24), and for t-Abs we use Lemmas 4.23 and 4.22.

2. By induction on derivations, using Lemmas 4.23 and 4.22 in the case t-TAbs; using Lemma 4.25 and the rule Subst in the case t-TApp; and using the rule Subst in the case t-Sub. □

5 Soundness

In this section we show the most important result for the metatheory of F_{≤}^{ω}: that the typed operational semantics is sound for the typing rules in Section 2. As we discussed in Section 1.4, this proof is essentially similar to traditional proofs of strong normalization, although it includes several technical modifications allowing us to prove soundness instead of normalization.

5.1 The Interpretation

We begin by defining the interpretation of kinds K with respect to a type substitution γ in a context Δ. There are two components to the interpretation: the first component is a set of types well-formed in Δ with particular properties, and models the judgement Γ ⊢ A : K; the second component is a relation on types in the first component, and models the judgement Γ ⊢ A ≤ B : K.

Partial interpretations are common in defining the semantics of dependent type theories [24, 34]. In our proof, we need a partial interpretation to guarantee that the bound A is well-formed for each Π-constructor ΠX≤A:K_{1}.K_{2}. This is information that can only be known when the proof itself is carried out, not when we define the interpretation. We prove that the interpretation of a kind K is always defined if K is well-formed according to the typing rules of F_{≤}^{ω}.

We need to include type information in our model, because we are proving soundness with respect to a system with types. Unfortunately, the approach used for simpler type systems, to assume an infinite collection of variables of each type [23], does not easily transfer to our system. The problem is that the kinds cannot be enumerated separately from the variables, because the kind ΠX≤A:K_{1}.K_{2} may include occurrences of variables in the type A. Hence, we build a Kripke-style model following Coquand and Gallier [20], where the possible worlds are valid contexts Δ and ordering is lexicographic, written Δ′ ≥ Δ.

The interpretation satisfies conditions similar to the usual saturated set conditions and properties lifted from the typed operational semantics, such as transitivity elimination (Lemma 5.6); properties about Kripke-style models such as monotonicity (Lemma 5.7); and the substitution property (Lemma 5.8).

Definition 5.1 (Semantic Object) A is a semantic object for Γ and K if Γ ⊢_{S} A ≤ T_{K} : K.

Definition 5.2 (Interpretation of Kinds) We give a partial interpretation of kinds for both judgements, [[−]]_{:}(−, −) for typing and [[−]]_{≤}(−, −) for subtyping:

• The interpretation [[⋆]]γΔ is well-defined if Δ ⊢_{S} ok. The two components are:

– [[⋆]]_{:}γΔ = {A | A is a semantic object for Δ and ⋆}.

– [[⋆]]_{≤}γΔ = {(A, B) | A and B are semantic objects and Δ ⊢_{S} A ≤ B : ⋆}.

• The interpretation [[ΠX≤A:K_{1}.K_{2}]]γΔ is well-defined if the following conditions hold: – there is a K′ such that Δ ⊢_{S} (ΠX≤A:K_{1}.K_{2})[γ] ↠_{n} K′,

– [[K_{1}]]γΔ′ is defined for any ⊢_{S} Δ′ ≥ Δ, and

– if ⊢_{S} Δ′ ≥ Δ and (C, A[γ]) ∈ [[K_{1}]]_{≤}γΔ′, then [[K_{2}]]γ[X:=C]Δ′ is well-defined. Under these circumstances, the two components are: – [[ΠX≤A:K_{1}.K_{2}]]_{:}γΔ is the set of B such that: ∗ B is a semantic object for Δ and K′,

∗ if ⊢_{S} Δ′ ≥ Δ and (C, A[γ]) ∈ [[K_{1}]]_{≤}γΔ′, then B C ∈ [[K_{2}]]_{:}γ[X:=C]Δ′.

– [[ΠX≤A:K_{1}.K_{2}]]_{≤}γΔ is the set of (B, C) such that:

∗ B and C are in [[ΠX≤A:K_{1}.K_{2}]]_{:}γΔ,

∗ Δ ⊢_{S} B ≤ C : K′,

∗ if ⊢_{S} Δ′ ≥ Δ and (D, A[γ]) ∈ [[K_{1}]]_{≤}γΔ′ then (B D, C D) ∈ [[K_{2}]]_{≤}γ[X:=D]Δ′.

Definition 5.3 (Interpretation of Contexts) We define a partial interpretation of contexts:

• [[∅]]Δ = {ϵ}. This is defined if Δ ⊢_{S} ok.

• [[Γ, x:A]]Δ = [[Γ]]Δ. This is defined if x ∉ dom(Γ) and, for any ⊢_{S} Δ′ ≥ Δ, [[Γ]]Δ′ is defined and A[γ] ∈ [[⋆]]_{:}γΔ′ for every γ ∈ [[Γ]]Δ′.

• [[Γ, X≤A:K]]Δ = {γ[X:=B] | γ ∈ [[Γ]]Δ and (B, A[γ]) ∈ [[K]]_{≤}γΔ}. This is defined if X ∉ dom(Γ) and, for any ⊢_{S} Δ′ ≥ Δ, [[Γ]]Δ′ is defined and A[γ] ∈ [[K]]_{:}γΔ′ for every γ ∈ [[Γ]]Δ′.

5.2 Properties of the Interpretation

We need to establish a variety of properties about the interpretation before carrying out the soundness proof. Definition 5.4 We write Δ ⊢_{S} γ, γ′ ↠_{n} γ′′ if for all X ∈ dom(γ) there is a K′ such that Δ ⊢_{S} γ(X), γ′(X) ↠_{n} γ′′(X) : K′.

We first give some simple properties about the interpretation: Lemma 5.5 (Basic Properties)

1. If [[K]]γΔ is defined then there is a K′ such that Δ ⊢_{S} K[γ] ↠_{n} K′.

2. If γ ∈ [[Γ]]Δ then Δ ⊢_{S} ok.

3. If [[K]]γΔ is defined and γ′(X) = γ(X) for all X ∈ dom(γ) then [[K]]γΔ = [[K]]γ′Δ.

4. If [[K]]γΔ and [[K]]γ′Δ are defined and Δ ⊢_{S} γ, γ′ ↠_{n} γ′′ then [[K]]γΔ = [[K]]γ′Δ.

Proof: Properties 1 and 2 follow by straightforward induction on K and Γ.

Property 3 follows by induction on K, using the fact that A[γ] ≡ A[γ′] for types A if γ(X) = γ′(X) for all X ∈ FV(A), and similarly for kinds.

Property 4 follows by induction on K using the fact that Δ ⊢_{S} K[γ], K[γ′] ↠_{n} K′′ if there is a γ′′ such that for all X ∈ FV(A) there is a K′′′ such that Δ ⊢_{S} γ(X), γ′(X) ↠_{n} γ′′(X) : K′′′, which follows using Subject Reduction and Determinacy. □

Next, we need some properties similar to the usual saturated set conditions. In the following we assume Δ ⊢_{S} K[γ] ↠_{n} K′:

Lemma 5.6 (Saturated Sets)

1. If A ∈ [[K]]_{:}γΔ then A is a semantic object for Δ and K′.

2. If (A, B) ∈ [[K]]_{≤}γΔ then Δ ⊢_{S} A ≤ B : K′.

3. If (A, B) ∈ [[K]]_{≤}γΔ then A ∈ [[K]]_{:}γΔ and B ∈ [[K]]_{:}γΔ.

4. If A and B are in [[K]]_{:}γΔ and Δ ⊢_{S} A, B ↠_{n} C : K′ then (A, B) ∈ [[K]]_{≤}γΔ.

5. If (A, B) and (B, C) are in [[K]]_{≤}γΔ then (A, C) ∈ [[K]]_{≤}γΔ.

6. If Δ(X)(A_{1}, …, A_{m}) ∈ [[K]]_{:}γΔ then (X(A_{1}, …, A_{m}), Δ(X)(A_{1}, …, A_{m})) ∈ [[K]]_{≤}γΔ.

7. If Δ ⊢_{S} A, B ↠_{w} C _{w}↠_{n} D : K′, A ∈ [[K]]_{:}γΔ and B is a semantic object for Δ and K′ then B ∈ [[K]]_{:}γΔ.

8. If A ∈ [[K]]_{:}γΔ then (A, T_{K[γ]}) ∈ [[K]]_{≤}γΔ.

Proof: Properties 1, 2 and 3 follow by construction.

Property 4 follows by induction on K, using Reflexivity and Conversion of subtyping in the semantics, plus Adequacy, Subject Reduction and Determinism for the Π case.

Property 5 follows by induction on K, using Transitivity of subtyping in the semantics. For Property 6, we first show a lemma stating that if Δ(X)(A_{1}, …, A_{m}) is a semantic

object for Δ and K′ then Δ ⊢_{S} X(A_{1}, …, A_{m}) ≤ Δ(X)(A_{1}, …, A_{m}) : K′, which follows by definition of Δ(X), Adequacy and Reflexivity for subtyping in the semantics. Hence X(A_{1}, …, A_{m}) is a semantic object for Δ and K′, using this lemma and Transitivity for the semantics. Property 6 then follows by induction on K, using Properties 1 and 3, and the fact that if ⊢_{S} Δ′ ≥ Δ then Δ′(X) = Δ(X) for all X ∈ dom(Δ).

For Property 7, first notice that if Δ ⊢_{S} A, B ↠_{w} C ↠_{n} D : K′ and A is a semantic object for Δ and K′ then B is a semantic object for Δ and K′ as well, using Determinism to show that Δ ⊢_{S} B ≤ T′_{K} : K′. Furthermore, we can show that if Δ ⊢_{S} A, B ↠_{w} C ↠_{n} D : K and Δ ⊢_{S} A E ↠_{w} F _{w}↠_{n} G : K′ then Δ ⊢_{S} B E ↠_{w} F _{w}↠_{n} G : K′. The result follows by induction on K, using Thinning and this simple lemma in the Π case.

Finally, for Property 8, we first observe that if Δ ⊢_{S} K ↠_{n} K′ then T_{K} is a semantic object for Δ and K′, which follows by a simple induction on K. The result follows by induction on K, using Properties 3, 4 and 5, plus Thinning and Conversion of subtyping.

□

We also need properties corresponding to the model being a Kripke-model: Lemma 5.7 (Monotonicity) If ⊢_{S} Δ′ ≥ Δ then:

1. A ∈ [[K]]_{:}γΔ implies A ∈ [[K]]_{:}γΔ′.

2. (A, B) ∈ [[K]]_{:}γΔ implies (A, B) ∈ [[K]]_{≤}γΔ′.

3. γ ∈ [[Γ]]Δ implies γ ∈ [[Γ]]Δ′. Proof: By induction on K or Γ, using Thinning for the first two and using the first two for the last. □

We also need to account for the dependency, since bounds in kinds include types: Lemma 5.8 (Substitution)

1. [[K]]γ_{1}[X:=B[γ_{1}]]γ_{2}Δ = [[K[X←B]]]γ_{1}γ_{2}.

2. Suppose that:

• [[Γ_{1}, X≤B:K, Γ_{2}]]Δ is defined, and

• (A[γ_{1}], B[γ_{1}]) ∈ [[K]]γ_{1}Δ for γ_{1} ∈ [[Γ_{1}]]Δ. Then:

• [[Γ_{1}, Γ_{2}[X←A]]]Δ is defined, and

• if γ_{1}γ_{2} ∈ [[Γ_{1}, Γ_{2}[X←A]]]Δ then γ_{1}[X:=A[γ_{1}]]γ_{2} ∈ [[Γ_{1}, X≤B:K, Γ_{2}]]Δ. Proof: Case 1 follows by induction on K, using basic properties of parallel substitution. Case 2 follows by induction on Γ_{2}, using basic properties of parallel substitution and Case 1.

□

Finally, we prove a lemma to deal with the rules of context equality. Lemma 5.9 (Context Replacement) Suppose:

• [[Γ_{1}, X≤A:K, Γ_{2}]]Δ is defined, and

• for any γ_{1} ∈ [[Γ_{1}]]Δ then:

– Δ ⊢_{S} K[γ_{1}], K′[γ_{1}] ↠_{n} K′′ and Δ ⊢_{S} A[γ_{1}], B[γ_{1}] ↠_{n} C : K′′,

– [[K]]γ_{1}Δ = [[K′]]γ_{1}Δ, and

– A[γ_{1}] ∈ [[K]]_{:}γ_{1}Δ and B[γ_{1}] ∈ [[K′]]_{:}γ_{1}Δ. Then [[Γ_{1}, X≤A:K, Γ_{2}]]Δ = [[Γ_{1}, X≤B:K′, Γ_{2}]]Δ. Proof: By induction on Γ_{1}, using Lemma 5.6 Case 4 for the base case. □

5.3 Soundness

We can now prove soundness. As usual for strong normalization proofs, we first need to prove the more general statement with respect to arbitrary well-behaved substitutions.

Theorem 5.10 If Γ ⊢ J and Δ ⊢_{S} ok then [[Γ]]Δ is defined. Furthermore:

1. If Γ ⊢ K and γ ∈ [[Γ]]Δ then [[K]]γΔ is defined.

2. If Γ ⊢ A : K and γ ∈ [[Γ]]Δ then A[γ] ∈ [[K]]_{:}γΔ.

3. If Γ ⊢ K = K′ and γ ∈ [[Γ]]Δ then [[K]]γΔ = [[K′]]γΔ and there is a K′′ such that Δ ⊢_{S} K[γ], K′[γ] ↠_{n} K′′.

4. If Γ ⊢ A = B : K and γ ∈ [[Γ]]Δ then A[γ] and B[γ] are in [[K]]_{≤}γΔ and there are C and K′ such that Δ ⊢_{S} K[γ] ↠_{n} K′ and Δ ⊢_{S} A[γ], B[γ] ↠_{n} C : K′.

5. If Γ ⊢ A ≤ B : K and γ ∈ [[Γ]]Δ then (A[γ], B[γ]) ∈ [[K]]_{≤}γΔ.

Proof: By induction on derivations, using the above properties about the interpretation. We consider several cases:

C-Empty By definition [[∅]]Δ is defined if Δ ⊢_{S} ok.

C-Var By inductive hypothesis [[Γ]]Δ′ is defined for ⊢_{S} Δ′ ≥ Δ. If γ ∈ [[Γ]]Δ′, then A[γ] ∈ [[⋆]]_{:}γΔ′ by inductive hypothesis. Furthermore, x ∉ dom(Γ), so [[Γ, x:A]]Δ is defined.

C-TVar By inductive hypothesis [[Γ]]Δ′ is defined for ⊢_{S} Δ′ ≥ Δ. If γ ∈ [[Γ]]Δ′, then A[γ] ∈ [[K]]_{:}γΔ′ by inductive hypothesis, and X ∉ dom(Γ), so [[Γ, X≤A:K]]Δ is defined.

Kind Agreement By inductive hypothesis [[Γ]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. By inductive hypothesis A[γ] ∈ [[K]]_{:}γΔ, so [[K]]_{:}γΔ is defined. Furthermore, by Lemma 5.5 Case 1 there is a K′ such that Δ ⊢_{S} K[γ] ↠_{n} K′.

K-Subst By inductive hypothesis [[Γ_{1}, X≤B:K, Γ_{2}]]Δ and [[Γ_{0}]]Δ are defined, and γ_{0} ∈ [[Γ_{0}]]Δ implies (A[γ_{0}], B[γ_{0}]) ∈ [[K]]_{≤}γ_{0}Δ. By Lemma 5.8 Case 2 [[Γ_{1}, Γ_{2}[X←A]]]Δ is defined.

Furthermore, γ_{0}γ_{1} ∈ [[Γ_{1}, Γ_{2}[X←A]]]Δ implies γ_{0}[X:=A[γ_{0}]]γ_{1} ∈ [[Γ_{1}, X≤A:K′, Γ_{2}]]Δ, so [[K]]γ_{0}[X:=A[γ_{0}]]γ_{1}Δ is defined by inductive hypothesis, and [[K]]γ_{0}[X:=A[γ_{0}]]γ_{1}Δ = [[K[X←A]]]γ_{0}γ_{1}Δ by Lemma 5.8 Case 1.

K-Ctxt-Eq The inductive hypotheses satisfy the premises of Lemma 5.9, so

[[Γ_{1}, X≤A:K, Γ_{2}]]Δ = [[Γ_{1}, X≤B:K′, Γ_{2}]]Δ

Hence, [[Γ_{1}, X≤B:K′, Γ_{2}]]Δ is defined, and if γ ∈ [[Γ_{1}, X≤B:K′, Γ_{2}]]Δ then γ ∈ [[Γ_{1}, X≤A:K, Γ_{2}]]Δ, so by inductive hypothesis [[K]]γΔ is defined.

T-Top By inductive hypothesis [[Γ]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. We know Δ ⊢_{S} ok by Lemma 5.5 Case 2. Hence Δ ⊢_{S} T_{⋆} ↠_{n} T_{⋆} : ⋆ by ST-Top, and Δ ⊢_{S} T_{⋆} ≤_{W} T_{⋆} : ⋆ by SWS-Top and SS-Inc. Hence T_{⋆} is a semantic object for Δ and ⋆, and so T_{⋆} ∈ [[⋆]]_{:}γΔ.

T-TVar By inductive hypothesis [[Γ_{1}, X ≤ A : K, Γ_{2}]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. Then γ = γ_{1}[X:=B]γ_{2}, with γ_{1} ∈ [[Γ_{1}]]Δ and (B, A[γ_{1}]) ∈ [[K]]_{≤}γ_{1}Δ, by definition of [[Γ]]Δ. Hence B ∈ [[K]]_{:}γ_{1}Δ by Lemma 5.6 Case 3, and B ∈ [[K]]_{:}γΔ by Lemma 5.5 Case 3.

T-TAbs By inductive hypothesis [[Γ, X≤A_{1}:K_{1}]]Δ is defined, so by definition of the interpretation [[Γ]]Δ′ is defined and A_{1}[γ] ∈ [[K_{1}]]_{:}γΔ′ for γ ∈ [[Γ]]Δ′, for any ⊢_{S} Δ′ ≥ Δ.

Suppose γ ∈ [[Γ]]Δ. We want to show (ΛX≤A_{1}:K_{1}.A_{2})[γ] ∈ [[ΠX≤A_{1}:K_{1}.K_{2}]]_{:}γΔ. We have to show two conditions:

• Δ ⊢_{S} (ΠX≤A_{1}:K_{1}.K_{2})[γ] ↠_{n} K′ and (ΛX≤A_{1}:K_{1}.A_{2})[γ] is a semantic object for Δ and K′. By Lemma 5.5 Case 1 Δ ⊢_{S} K_{1}[γ] ↠_{n} K′_{1}, and by Lemma 5.6 Case 1 Δ ⊢_{S} A_{1}[γ] ↠_{n} A′_{1} : K′_{1}. Hence Δ, Y ≤A_{1}[γ]:K_{1}[γ] ⊢_{S} ok for Y fresh in Δ. By Lemma 5.7 Case 3 γ ∈ [[Γ]]Δ implies γ ∈ [[Γ]]Δ, Y ≤A_{1}[γ]:K_{1}[γ]. By Lemma 5.6 Case 6 (Y, A_{1}[γ]) ∈ [[K_{1}]]_{≤}γΔ, Y ≤A_{1}[γ]:K_{1}[γ]. Hence

γ[X:=Y] ∈ [[Γ, X≤A_{1}:K_{1}]]Δ, Y ≤A_{1}[γ]:K_{1}[γ]

so by inductive hypothesis A_{2}[γ[X:=Y]] ∈ [[K_{2}]]_{:}γ[X:=Y]Δ′. Hence

Δ, Y ≤A_{1}[γ]:K_{1}[γ] ⊢_{S} K_{2}[γ[X:=Y]] ↠_{n} K′_{2}
Δ, Y ≤A_{1}[γ]:K_{1}[γ] ⊢_{S} A_{2}[γ[X:=Y]] ↠_{n} A′_{2} : K′_{2}
Δ, Y ≤A_{1}[γ]:K_{1}[γ] ⊢_{S} A_{2}[γ[X:=Y]] ≤ T_{K′_{2}} : K′_{2}

by Lemma 5.6 Case 1 and definition of semantic object. Hence,

Δ ⊢_{S} (ΠX≤A_{1}:K_{1}.K_{2})[γ] ↠_{n} ΠY ≤A′_{1}:K′_{1}.K′_{2}
Δ ⊢_{S} (ΛX≤A_{1}:K_{1}.A_{2})[γ] ≡ ΛY ≤A_{1}[γ]:K_{1}[γ].A_{2}[γ[X:=Y]]
↠_{n} ΛY ≤A′_{1}:K′_{1}.A′_{2} : ΠY ≤A′_{1}:K′_{1}.K′_{2}
Δ ⊢_{S} (ΛX≤A_{1}:K_{1}.A_{2})[γ] ≤ ΛY ≤A′_{1}:K′_{1}.T_{K′_{2}} ≡ T_{ΠY ≤A′_{1}:K′_{1}.K′_{2}}
: ΠY ≤A′_{1}:K′_{1}.K′_{2}

where the last line follows using Adequacy and Subject Reduction for the welltypedness of the right-hand side. Hence, (ΠX≤A_{1}:K_{1}.K_{2})[γ] is a semantic object for Δ and ΠY ≤A′_{1}:K′_{1}.K′_{2}.

• (ΠX≤A_{1}:K_{1}.K_{2})[γ] B ∈ [[K_{2}]]_{:}γ[X:=B]Δ′, with ⊢_{S} Δ′ ≥ Δ and (B, A_{1}[γ]) ∈ [[K_{1}]]_{≤}γΔ′. First, by Lemma 5.7 Case 3 γ ∈ [[Γ]]Δ implies γ ∈ [[Γ]]Δ′, and (B, A_{1}[γ]) ∈ [[K_{1}]]_{≤}γΔ′ implies γ[X:=B] ∈ [[Γ, X≤A_{1}:K_{1}]]Δ′ by definition of the interpretation. Hence by inductive hypothesis A_{2}[γ[X:=B]] ∈ [[K_{2}]]_{:}γ[X:=B]Δ′, and so by Lemma 5.6 Case 1 Δ′ ⊢_{S} A_{2}[γ[X:=B]] ↠_{w} C : K′′_{2}, where Δ′ ⊢_{S} K_{2}[γ[X:=B]] ↠_{n} K′′_{2}. Then Δ ⊢_{S} (ΛX≤A_{1}:K_{1}.A_{2})[γ] : ΠY ≤A′_{1}:K′_{1}.K′_{2} implies Δ′ ⊢_{S} (ΛX≤A_{1}:K_{1}.A_{2})[γ] : ΠY ≤A′_{1}:K′_{1}.K′_{2} by Thinning, and Δ′ ⊢_{S} B ≤

A_{1}[γ] : K′_{1} by Lemma 5.6 Case 2. Hence

\begin{aligned}Δ′ & ⊢_{S} & (ΛX≤A_{1}:K_{1}.A_{2})[γ](B) \\ & ≡ & (ΛY ≤A_{1}[γ]:K_{1}[γ].A_{2}[γ[X:=Y]])(B) ↠_{w} C : K′′_{2} \end{aligned}

by ST-Beta, because A_{2}[γ[X:=Y]][Y ←B] ≡ A_{2}[γ[X:=B]] where Y can be chosen to be fresh in Δ′. Hence, by Lemma 5.6 Case 7

(ΛX≤A_{1}:K_{1}.A_{2})[γ](B) ∈ [[K_{2}]]_{:}γ[X:=B]Δ′

Hence, (ΛX≤A_{1}:K_{1}.A_{2})[γ](B) ∈ [[ΠX≤A_{1}:K_{1}.K_{2}]]_{:}γΔ.

T-TApp By inductive hypothesis [[Γ]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. Then A[γ] ∈ [[ΠX≤B:K_{1}.K_{2}]]_{:}γΔ and (C[γ], B[γ]) ∈ [[K_{1}]]_{≤}γΔ. Clearly ⊢_{S} Δ ≥ Δ, since Δ ⊢_{S} ok by Lemma 5.5 Case 2, so

(A[γ])(C[γ]) ≡ (A C)[γ] ∈ [[K_{2}]]_{:}γ[X:=C[γ]] = [[K_{2}[X←C]]]_{:}γΔ

where the last equality follows by Lemma 5.8 Case 2.

T-Eq-TApp By inductive hypothesis [[Γ]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. By inductive hypothesis A[γ], B[γ] ∈ [[ΠX≤E:K_{1}.K_{2}]]_{:}γΔ, Δ ⊢_{S} A[γ], B[γ] ↠_{n} A′ : ΠX≤E′:K′_{1}.K′_{2} with Δ ⊢_{S} (ΠX≤E:K_{1}.K_{2})[γ] ↠_{n} ΠX≤E′:K′_{1}.K′_{2}, and also C[γ], D[γ] ∈ [[K_{1}]]_{:}γΔ, Δ ⊢_{S} C[γ], D[γ] ↠_{n} C′ : K′_{1}, and finally (C[γ], E[γ]) ∈ [[K_{1}]]_{≤}γΔ. Hence,

(A[γ])(C[γ]) ≡ (AC)[γ] ∈ [[K_{2}]]_{:}γ[X:=C[γ]]Δ = [[K_{2}[X←C]]]_{:}γΔ
(B[γ])(D[γ]) ≡ (BD)[γ] ∈ [[K_{2}]]_{:}γ[X:=D[γ]]Δ = [[K_{2}[X←D]]]_{:}γΔ

Using Adequacy, Subject Reduction and Determinacy we conclude that

Δ ⊢_{S} (AC)[γ], (BD)[γ] ↠_{n} F : K′_{2}

where Δ ⊢_{S} K_{2}[X←C] ↠_{n} K′_{2}. Finally, Δ ⊢_{S} γ[X:=C[γ]], γ[X:=D[γ]] ↠_{n} γ′, so by Lemma 5.5 Case 4:

(BD)[γ] ∈ [[K_{2}]]_{:}γ[X:=C[γ]]Δ = [[K_{2}[X←C]]]_{:}γΔ

S-Top By inductive hypothesis [[Γ]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. Then A[γ] ∈ [[K]]_{:}γΔ, so by Lemma 5.6 Case 8 (A[γ], T_{K[γ]}) ∈ [[K]]_{≤}γΔ, and T_{K[γ]} ≡ T_{K}[γ].

5 SOUNDNESS 32

S-Trans By inductive hypothesis [[Γ]]Δ is defined.

Suppose γ ∈ [[Γ]]Δ. By inductive hypothesis (A[γ], B[γ]) ∈ [[K]]_{≤}γΔ and (B[γ], C[γ]) ∈ [[K]]_{≤}γΔ. Hence by Lemma 5.6 Case 5 (A[γ], C[γ]) ∈ [[K]]_{≤}γΔ. □

Lemma 5.11 If Γ ⊢ ok then id_{Γ} ∈ [[Γ]]Γ, where id_{Γ} is the identity substitution on Γ. Proof: By induction on Γ, using several simple generation lemmas for contexts. □ Corollary 5.12 (Soundness)

1. If Γ ⊢ A : K then there are K′, B and C such that Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ↠_{w} B _{w}↠_{n} C : K′.

2. If Γ ⊢ A ≤ B : K then there is a K′ such that Γ ⊢_{S} K ↠_{n} K′ and Γ ⊢_{S} A ≤ B : K′.

5.4 Consequences of Soundness

We can use Soundness, Corollary 5.12, and Completeness, Proposition 4.6, to transfer the metatheoretic results from the typed operational semantics to the original presentation. Lemma 5.13 (Admissibility of Structural Rules) The rules in Section 2.3 are admissible for the system Γ ⊢^{−} J. Proof: Suppose we have a derivation of Γ ⊢ J, for example Γ ⊢ A : K, which is then a derivation of Γ ⊢^{−} J with uses of the structural rules in Section 2.3. By Soundness we know that there are B and K′ such that Γ ⊢_{S} A ↠_{n} B : K′ and Γ ⊢_{S} K ↠_{n} K′. By Completeness Γ ⊢^{−} A : K′ and Γ ⊢^{−} K = K′, so by T-Conv Γ ⊢^{−} A : K. □ Lemma 5.14 (Strong Normalization) If Γ ⊢ A : K then A is strongly normalizing. Proof: By Soundness and Strong Normalization (Lemma 4.15). □ Lemma 5.15 (Subject Reduction for →_{β}_{2})

• If Γ ⊢ ok and Γ →_{β}_{2} Γ′ then Γ′ ⊢ ok.

• If Γ ⊢ K and K →_{β}_{2} K′ then Γ ⊢ K and Γ ⊢ K =_{β} K′.

• If Γ ⊢ A : K and A →_{β}_{2} B then Γ ⊢ A : K and Γ ⊢ A =_{β} B : K.

• If Γ ⊢ A ≤ B : K and A →_{β}_{2} C then Γ ⊢ C ≤ B : K, or if B →_{β}_{2} C then

Γ ⊢ A ≤ C : K. Proof: By Soundness, Subject Reduction (Corollary 4.13), and Completeness. □ Proposition 5.16 (Generation for Subtyping)

1. If Γ ⊢ (A_{1}→A_{2}) ≤ (B_{1}→B_{2}) : ⋆ then Γ ⊢ B_{1} ≤ A_{1} : ⋆ and Γ ⊢ A_{2} ≤ B_{2} : ⋆

2. If Γ ⊢ (∀X≤A_{1}:K_{A}.A_{2}) ≤ (∀X≤B_{1}:K_{B}.B_{2}) : ⋆ then Γ ⊢ K_{A} =_{β} K_{B}, Γ ⊢ A_{1} =_{β} B_{1} : K_{A}, and Γ, X≤A_{1}:K_{A} ⊢ A_{2} ≤ B_{2} : ⋆.

Proof:

1. By Soundness Γ ⊢_{S} A_{1}→A_{2} ≤ B_{1}→B_{2} : ⋆. Since the semantic presentation is deterministic the latter must have been obtained by SS-Inc and SWS-Arrow from Γ ⊢_{S} B_{1} ≤ A_{1} : ⋆ and Γ ⊢_{S} A_{2} ≤ B_{2} : ⋆. Then, by Completeness, Γ ⊢ B_{1} ≤ A_{1} : ⋆ and Γ ⊢ A_{2} ≤ B_{2} : ⋆.

2. By Soundness Γ ⊢_{S} ∀X≤A_{1}:K_{A}.A_{2} ≤ ∀X≤B_{1}:K_{B}.B_{2} : ⋆. Since the semantic presentation is deterministic the latter must have been obtained by SS-Inc and SWS-All from Γ, X≤A_{1}:K_{A} ⊢_{S} A_{2} ≤ B_{2} : ⋆, Γ ⊢_{S} A_{1}, B_{1} ↠_{n} C : K′′, and Γ ⊢_{S} K_{A}, K_{B} ↠_{n} K′′. By Completeness Γ, X≤A_{1}:K_{A} ⊢ A_{2} ≤ B_{2} : ⋆, and also Γ ⊢ A_{1} =_{β} C : K′′, Γ ⊢ B_{1} =_{β} C : K′′, Γ ⊢ K_{A} =_{β} K′′, and Γ ⊢ K_{B} =_{β} K′′. Hence by

T-EQ-Sym, T-EQ-Trans, K-EQ-Sym, K-EQ-Trans, it follows that Γ ⊢ K_{A} =_{β} K_{B},

and also that Γ ⊢ A_{1} =_{β} B_{1} : K′′, and Γ ⊢ K′′ =_{β} K_{A}. Finally, by T-EQ-Conv, Γ ⊢ A_{1} =_{β} B_{1} : K_{A}. □

Proposition 5.17 (Generation for Typing)

1. If Γ ⊢ λx:A_{1}.M : A then there exists an A_{2} such that Γ, x:A_{1} ⊢ M : A_{2} and Γ ⊢ A_{1}→A_{2} ≤ A : ⋆.

2. If Γ ⊢ λX≤A_{1}:K.M : A then there exists an A_{2} such that Γ, X≤A_{1}:K ⊢ M : A_{2} and Γ ⊢ ∀X≤A_{1}:K.A_{2} ≤ A : ⋆.

Proof: Each case follows by induction on the derivation of the antecedent. □

Lemma 5.18 (Agreement)

1. If Γ_{1}, x:A, Γ_{2} ⊢ ok then Γ_{1} ⊢ A : ⋆.

2. If Γ_{1}, X≤A:K, Γ_{2} ⊢ ok then Γ_{1} ⊢ A : K.

3. If Γ ⊢ M : A then Γ ⊢ A : ⋆.

Proof: We use Lemma 4.23, Soundness and Completeness. □

6 Subject Reduction

Proposition 6.1 (→_{β}_{1} Subject Reduction for Terms)

If Γ ⊢ M : A and M →_{β}_{1} M′ then Γ ⊢ M′ : A.

Proof: By induction on the derivation of Γ ⊢ M : A.

t-Var Vacuously true.

t-Abs By the induction hypothesis and t-Abs.

t-App Let M ≡ N a. Then we are given that Γ ⊢ N : A_{1}→A and Γ ⊢ a : A_{1}. There are 3 cases to consider. If N →_{β}_{1} N′ or a →_{β}_{1} a′ then the result follows by the induction hypothesis and t-App. The interesting case is when N ≡ λx:B_{1}.N′ and M →_{β}_{1} N′[x←a]. By Generation for Typing (Proposition 5.17), Γ, x:B_{1} ⊢ N′ : B_{2} and Γ ⊢ B_{1}→B_{2} ≤ A_{1}→A, for some B_{2}. By Generation for Subtyping (Proposition 5.16) Γ ⊢ A_{1} ≤ B_{1} and Γ ⊢ B_{2} ≤ A. By t-Sub, Γ ⊢ a : B_{1}, and, by Substitution (Lemma 4.26), Γ ⊢ N′[x←a] : B_{2}. Finally, by t-Sub, Γ ⊢ N′[x←a] : A.

t-TAbs By the induction hypothesis and t-TAbs.

t-TApp Let M ≡ N B. We are given that Γ ⊢ N : ∀X≤A_{1}:K_{A}.A_{2}, Γ ⊢ B ≤ A_{1} : K_{A}, and A ≡ A_{2}[X←B]. There are two cases to consider. If N →_{β}_{1} N′ then the result follows by the induction hypothesis and t-TApp. Otherwise, N ≡ λX≤B_{1}:K_{B}.N′ and M′ ≡ N′[X←B]. By Generation for Typing (Proposition 5.17), Γ, X≤B_{1}:K_{B} ⊢ N′ : B_{2}, and Γ ⊢ ∀X≤B_{1}:K_{B}.B_{2} ≤ ∀X≤A_{1}:K_{A}.A_{2} : ⋆, for some B_{2}. By Generation for Subtyping (Proposition 5.16), Γ, X≤A_{1}:K_{A} ⊢ B_{2} ≤ A_{2} : ⋆, Γ ⊢ A_{1} =_{β} B_{1} : K_{A}, and Γ ⊢ K_{A} =_{β} K_{B}. By S-Conv, Γ ⊢ A_{1} ≤ B_{1} : K_{A}, and, by S-Trans, Γ ⊢ B ≤ B_{1} : K_{A}. By Substitution (Lemma 4.26), Γ ⊢ N′[X←B] : B_{2}[X←B]. By Subst, Γ ⊢ B_{2}[X←B] ≤ A_{2}[X←B] : ⋆. Finally, by t-Sub Γ ⊢ N′[X←B] : A_{2}[X←B] : ⋆.

t-Sub By the induction hypothesis and t-Sub. □

Lemma 6.2 If Γ ⊢ M : A and Γ →_{β}_{2} Γ′ then Γ′ ⊢ M : A.

Proof: By induction on derivations using Lemma 5.15. □

Lemma 6.3 If C →_{β}_{2} C′ then B[X←C] ↠_{β}_{2} B[X←C′].

Proposition 6.4 (→_{β}_{2} Subject Reduction for Terms)

If Γ ⊢ M : A and M →_{β}_{2} M′ then Γ ⊢ M′ : A.

Proof: By induction on derivations.

t-Var Vacuously true.

t-Abs There are two cases to consider.

1. A →_{β}_{2} A′. By Lemma 6.2, Γ, x:A′ ⊢ M : B, by t-Abs, Γ ⊢ λx:A′.M : A′→B. By Lemma 5.18 Case 1 and Lemma 4.23 we conclude Γ ⊢ A : ⋆ from Γ, x:A ⊢ M : B. By Lemma 5.15, Γ ⊢ A =_{β} A′ : ⋆. By Lemma 5.18 Case 3, Γ, x:A′ ⊢ B : ⋆, by Strengthening (Lemma 4.24), Γ ⊢ B : ⋆, by T-EQ-Refl, Γ ⊢ B =_{β} B : ⋆, by

T-EQ-Arrow and T-EQ-Sym, Γ ⊢ A′→B =_{β} A→B : ⋆. Then, by S-Conv,

Γ ⊢ A′→B ≤ A→B : ⋆, and by T-Sub Γ ⊢ λx:A′.M : A→B

2. M →_{β}_{2} M′. By the induction hypothesis and T-Abs.

t-App There are two cases to consider, either M →_{β}_{2} M′ or N →_{β}_{2} N′. Both cases follow by the induction hypothesis and t-App.

t-TAbs There are three cases to consider.

1. If M →_{β}_{2} M′, the result follows by the induction hypothesis and t-TAbs.

2. If A →_{β}_{2} A′, it is similar to t-Abs case 1.

3. If K →_{β}_{2} K′, by Lemma 6.2, Γ, X≤A:K′ ⊢ M : B, by t-TAbs, Γ ⊢ λX≤A:K′.M : ∀X≤A:K′.B. From Γ, X≤A:K ⊢ M : B, by Lemma 4.23 and Lemma 5.18 Case 2, Γ ⊢ A : K, and, by the rule Kind-Agreement, Γ ⊢ K. By Lemma 5.15, Γ ⊢ K =_{β} K′, by T-EQ-Refl, Γ ⊢ A =_{β} A : K. With a similar argument to that used in the t-Abs case we prove that Γ ⊢ B =_{β} B : ⋆. Now, by T-EQ-Sym and T-EQ-All, Γ ⊢ ∀X≤A:K′.B =_{β} ∀X≤A:K.B : ⋆, by S-Conv, Γ ⊢ ∀X≤A:K′.B ≤ ∀X≤A:K.B : ⋆. Finally, by t-Sub, Γ ⊢ λX≤A:K′.M : ∀X≤A:K.B.

t-TApp There are two cases to consider.

1. If M →_{β}_{2} M′ then the result follows by the induction hypothesis and t-TApp.

2. If C →_{β}_{2} C′, by Lemma 4.13, Γ ⊢ C′ ≤ A : K, by t-TApp, Γ ⊢ M C′ : B[X←C′], by Lemma 5.18 Case 3, Γ ⊢ B[X←C] : ⋆, by Lemma 6.3 and Lemma 5.15, Γ ⊢ B[X←C] =_{β} B[X←C′] : ⋆, by T-EQ-Sym and t-Sub, Γ ⊢ M C′ : B[X←C].

t-Sub By the induction hypothesis and t-Sub. □

Proposition 6.5 (↠_{β} Subject Reduction for Terms)

If Γ ⊢ M : A and M ↠_{β} M′ then Γ ⊢ M′ : A.

Proof: The proof is by induction on the definition of ↠_{β}. The reflexive case is immediate, the cases for →_{β}_{1} and →_{β}_{2} follow by Propositions 6.1 and 6.4 respectively, and the transitivity case follows by the induction hypothesis. □

7 An Algorithmic Presentation

From the rules for subtyping in the typed operational semantics we extract an algorithm that computes the subtyping relation on weak head normal forms, ignoring kind information and well-formation of contexts. The reductions to weak head normal form are then untyped calculations defined as follows:

A ↠_{w} A  if A is weak head normal.
A B ↠_{w} C D if A ↠_{w} C, B ↠_{n} D, and C ≠ ΛX≤E:K.F
A B ↠_{w} E  if A ↠_{w} ΛX≤C:K.D and D[X←B] ↠_{w} E

where ↠_{n} is defined simultaneously by recursively finding the normal form of each subterm in a weak head normal form.

The algorithm to compute the subtyping relation is defined by the following rules.

7.1 Algorithmic Subtyping

\frac{A ↠_{w} C  B ↠_{w} D  Γ ⊢_{A} C ≤_{W} D}{Γ ⊢_{A} A ≤ B}  (AS-Inc)

This rule reduces the arguments to weak head normal and then invokes the weak-head subtyping algorithm defined as follows.

7.2 Algorithmic Weak-Head Subtyping

Γ ⊢_{A} A ≤_{W} T_{⋆}  A does not have a head variable  (AWS-Top)

\frac{\begin{matrix}Γ(X) ↠_{n} B \\ B(A_{1}, …, A_{m}) ↠_{w} E \end{matrix}  \begin{matrix}Γ ⊢_{A} E ≤_{W} C \\ C ≠ X(A_{1}, … A_{n}) \end{matrix}}{Γ ⊢_{A} X(A_{1}, …, A_{m}) ≤_{W} C : K}  (AWS-TApp)
Γ ⊢_{A} X(A_{1}, …, A_{m}) ≤_{W} X(A_{1}, …, A_{m})  (AWS-Refl)
\frac{Γ ⊢_{A} B_{1} ≤ A_{1}  Γ ⊢_{A} A_{2} ≤ B_{2}}{Γ ⊢_{A} A_{1}→A_{2} ≤_{W} B_{1}→B_{2}}  (AWS-Arrow)
\frac{Γ, X≤A_{1}:K ⊢_{A} A_{2} ≤ B_{2}  nf(A_{1}) = nf(B_{1})  nf(K) = nf(K′)}{Γ ⊢_{A} ∀X≤A_{1}:K.A_{2} ≤_{W} ∀X≤B_{1}:K′.B_{2}}  (AWS-All)
\frac{Γ, X≤A_{1}:K_{1} ⊢_{A} A_{2} ≤ B_{2}  nf(A_{1}) = nf(B_{1})}{Γ ⊢_{A} ΛX≤A_{1}:K_{1}.A_{2} ≤_{W} ΛX≤B_{1}:K′_{1}.B_{2}}  (AWS-TAbs)

Our aim is to prove that this algorithm is sound with respect to the original system on well-formed types: if Γ ⊢_{A} A ≤ B and Γ ⊢ A, B : K then Γ ⊢ A ≤ B : K. The problem we encounter is that the original system uses subtyping to check Γ ⊢ A, B : K. Therefore we need algorithmic versions of the judgements involved in proving well-kindedness.

The algorithmic rules for the other judgements are modifications of the F_{≤}^{ω} rules and not of the typed operational semantics. The rules for Context Formation are identical, and 7 AN ALGORITHMIC PRESENTATION 37

in Kind and Type Formation the assumptions of the form Γ ⊢ ok are dropped. The rules AK-Π, AT-All and AT-TAbs need the side condition X ∉ dom(Γ) and the rule AT-TApp uses an arbitrary normalization procedure.

7.3 Algorithmic Context Formation

∅ ⊢_{A} ok  (AC-Empty)
\frac{Γ ⊢_{A} A : ⋆  x ∉ dom(Γ)}{Γ, x:A ⊢_{A} ok}  (AC-Var)
\frac{Γ ⊢_{A} A : K  X ∉ dom(Γ)}{Γ, X≤A:K ⊢_{A} ok}  (AC-TVar)

7.4 Algorithmic Kind Formation

Γ ⊢_{A} ⋆  (AK-⋆)
\frac{Γ, X≤A:K_{1} ⊢_{A} K_{2}  Γ ⊢_{A} A : K_{1}  X ∉ dom(Γ)}{Γ ⊢_{A} ΠX≤A:K_{1}.K_{2}}  (AK-Π)

7.5 Algorithmic Type Formation

Γ ⊢_{A} T_{⋆} : ⋆  (AT-Top)
Γ_{1}, X≤A:K, Γ_{2} ⊢_{A} X : K  (AT-TVar)
\frac{Γ ⊢_{A} A_{1} : ⋆  Γ ⊢_{A} A_{2} : ⋆}{Γ ⊢_{A} A_{1}→A_{2} : ⋆}  (AT-Arrow)
\frac{Γ, X≤A_{1}:K ⊢_{A} A_{2} : ⋆  Γ ⊢_{A} A_{1} : K_{1}  X ∉ dom(Γ)}{Γ ⊢_{A} ∀X≤A_{1}:K.A_{2} : ⋆}  (AT-All)
\frac{Γ, X≤A_{1}:K_{1} ⊢_{A} A_{2} : K_{2}  Γ ⊢_{A} A : K_{1}  X ∉ dom(Γ)}{Γ ⊢_{A} ΛX≤A_{1}:K_{1}.A_{2} : ΠX≤A_{1}:K_{1}.K_{2}}  (AT-TAbs)
\frac{Γ ⊢_{A} A : ΠX≤B:K_{1}.K_{2}  Γ ⊢_{A} C ≤ B  Γ ⊢_{A} C : K′_{1}  nf(K) = nf(K′)}{Γ ⊢_{A} A C : K_{2}[X←C]}  (AT-TApp)

7.6 Equivalence of the Algorithm and F_{≤}^{ω}

Proposition 7.1 (Correctness of the Algorithm)

1. If Γ ⊢_{A} ok then Γ ⊢ ok.

2. Given Γ ⊢ ok. If Γ ⊢_{A} K then Γ ⊢ K.

3. Given Γ ⊢ ok. If Γ ⊢_{A} A : K then Γ ⊢ A : K.

4. Given Γ ⊢ A, B : K. If Γ ⊢_{A} A ≤_{W} B then Γ ⊢ A ≤ B : K.

5. Given Γ ⊢ A, B : K. If Γ ⊢_{A} A ≤ B then Γ ⊢ A ≤ B : K.

Proof: By induction on derivations, using Soundness (Corollary 5.12), Completeness (Proposition 4.6), and Subject Reduction (Corollary 4.13). □

Proposition 7.2 (Completeness of the Algorithm)

1. If Γ ⊢_{S} ok then Γ ⊢_{A} ok.

2. If Γ ⊢_{S} K then Γ ⊢_{A} K.

3. If Γ ⊢_{S} A : K then Γ ⊢_{A} A : K.

4. If Γ ⊢_{S} A ≤_{W} B : K then Γ ⊢_{A} A ≤ B.

5. If Γ ⊢_{S} A ≤ B : K then Γ ⊢_{A} A ≤ B.

Proof: By induction on derivations. The proof is straightforward because all the information in each ⊢_{A} rules is included in or follows easily from the corresponding ⊢_{S} rules. □

The last two properties together with the soundness of the semantics (Corollary 5.12) prove that the algorithm is sound and complete with respect to F_{≤}^{ω}.

Proposition 7.3 (Equivalence of the Algorithm and F_{≤}^{ω})

1. Γ ⊢_{A} ok iff Γ ⊢ ok.

2. Γ ⊢ ok and Γ ⊢_{A} K iff Γ ⊢ K.

3. Γ ⊢ ok, Γ ⊢_{A} A : K′, and Γ ⊢_{A} K ↠_{n} K′ iff Γ ⊢ A : K.

4. Γ ⊢ A, B : K and Γ ⊢_{A} A ≤ B iff Γ ⊢ A ≤ B : K.

Proof: By induction on derivations, using Soundness (Corollary 5.12), Completeness (Proposition 4.6), and Subject Reduction (Corollary 4.13). □ By the equivalence, we can use the following sequence to check whether Γ ⊢ A ≤ B : K:

1. check that Γ is a good context, Γ ⊢_{A} ok,

2. infer kinds K′ and K′′ such that Γ ⊢_{A} A : K′ and Γ ⊢_{A} B : K′′,

3. check that the given kind is well formed, Γ ⊢_{A} K,

4. check that K′, K′′ and the normal form of K (which exists by Strong Normalization (Lemma 4.15)) are syntactically equal,

5. check that Γ ⊢_{A} A ≤ B.

If any of the steps fails then the statement Γ ⊢ A ≤ B : K is not derivable in F_{≤}^{ω}, and otherwise it is.

Hence, the only significant result that remains to be proved for F_{≤}^{ω} is the decidability of type-checking and subtyping. These follow straightforwardly from the termination of the subtyping algorithm. The details of such a proof should be a simple modification of the proof of decidability of subtyping for F_{∧}^{ω} by Compagnoni [17].

8 Related and Future Work

Bruce [6] uses bounded operator abstraction, but does not develop the metatheory. Compagnoni [17] mentions the open problem of studying the metatheory for bounded operator abstraction.

Most type systems with subtyping do not have the circularity between type formation and subtyping mentioned in the introduction: for example, F_{<:}^{ω} [11, 13, 12, 31, 14], F_{∧}^{ω} [18], and the systems in Abadi and Cardelli’s book on objects [2] all separate the two judgements. One system that does have the circularity is λP_{≤}, a system for subtyping with dependent types studied by Aspinall and Compagnoni [4]. There, the authors avoid the interdependency by finding a particular order in which to prove results.

As we mentioned in Section 1, the model construction is based on well-established ideas in dependent type theory. Streicher [34] gives a partial interpretation function to define the categorical semantics of the calculus of constructions, a technique which is now widely used. Coquand and Gallier [20] introduce Kripke-style models to build typed proofs of strong normalization for systems with dependent types. Typed operational semantics has been used to develop the metatheory of UTT, a sophisticated type theory with inductive types, impredicative propositions and type universes [24, 25]. Coquand [19] interprets judgemental equality as a logical relation to show properties of Martin-Löf type theory with βη-equality, similar to our interpretation of the subtyping relation.

It seems to be possible to use the technique developed by the first author for higherorder subtyping [17] for the particular system F_{≤}^{ω} that we study here. We believe that substitution can first be proved simultaneously for the kinding and subtyping judgements for the original system (without the structural rules). This can then be used to prove the subject reduction property for the original system, which in turn is used to establish basic properties of the normal system appropriately formulated for F_{≤}^{ω}. However, this approach does not enjoy the advantages of typed operational semantics mentioned in Section 1.2. In particular, the admissibility of the structural rules in Section 2.3 needs to be proved by induction on derivations for each individual rule, the overall proof is delicate and based on a particular order for the results, and the benefits of typed operational semantics for studying properties of reduction such as subject reduction and strong normalization are lost.

There are several directions for future work. The proof here should easily extend to a system with βη-equality, the equality for which typed operational semantics was originally developed. We also believe that the model construction can be extended to cope with Γ-reduction, replacing variables X by their bounds A if X≤A : K is in Γ, which cannot be done directly in the semantics because of an interdependency of transitivity elimination and context replacement. Furthermore, it seems that the model can deal with a limited form of contravariance for quantification over the kind ⋆ but not over arbitrary kinds. Finally, we have not included recursive types or objects, but Abadi and Cardelli [2] have demonstrated that these do not present difficulties at the level of types, and our proof should extend without any problems.

9 CONCLUSIONS 40

9 Conclusions

In this paper we have studied F_{≤}^{ω}, the first treatment of the metatheory for a system of higher-order subtyping with bounded operator abstraction. We have used techniques for constructing models for dependent type theory to solve problems associated with the weak dependency introduced by bounds in kinds, and we have modeled the subtyping relation directly rather than using a syntactic encoding. We have also used the new tool of typed operational semantics to give simpler proofs for meta-theoretic properties such as substitution, kind correctness, and subject reduction and Church–Rosser for type reduction. Finally, we have shown the equivalence with the algorithmic presentation of the system. Because the techniques introduced are adapted from other contexts and do not involve encodings of syntax, we believe that they are generally applicable.

Acknowledgments

We thank Luca Cardelli for providing encouragement and motivation for this work, and Paul Jackson and Martin Steffen for their comments on drafts of the paper. The first author is funded by a European Community TMR grant, and the second author is funded by a research fellowship from EPSRC.

References

[1] M. Abadi and L. Cardelli. On subtyping and matching. In ECOOP’95, pages 145–167. Springer-Verlag, August 1995.

[2] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[3] R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993. A preliminary version appeared in POPL ’91 (pp. 104–118), and as DEC Systems Research Center Research Report number 62, August 1990.

[4] D. Aspinall and A. Compagnoni. Subtyping dependent types. In Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA., July 27-30 1996. Preliminary version July 1995.

[5] H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

[6] K. B. Bruce. Typing in object-oriented languages: Achieving expressiveness and safety. Unpublished, June 1996.

[7] K. B. Bruce and G. Longo. A modest model of records, inheritance, and bounded quantification. Information and Computation, 87:196–240, 1990. Also in [27]. An earlier version appeared in the proceedings of the IEEE Symposium on Logic in Computer Science, 1988.

REFERENCES 41

[8] K. B. Bruce and J. Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, Albequerque, NM, January 1992.

[9] K. B. Bruce, A. Schuett, and R. van Gent. Polytoil: a type-safe polymorphic object-oriented language. In ECOOP’95. Springer-Verlag, August 1995.

[10] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. Preliminary version in Semantics of Data Types, Kahn, MacQueen, and Plotkin, eds., Springer-Verlag LNCS 173, 1984.

[11] L. Cardelli. Types for data-oriented languages. In First Conference on Extending Database Technology, volume 303 of Lecture Notes in Computer Science. Springer-Verlag, May 1988.

[12] L. Cardelli. Notes about F_{<:}^{ω}. Unpublished manuscript, October 1990.

[13] L. Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991. An earlier version appeared as DEC Systems Research Center Research Report #45, February 1989.

[14] L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, October 1991. Preliminary version in ACM Conference on Lisp and Functional Programming, June 1990. Also available as DEC SRC Research Report 55, Feb. 1990.

[15] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), December 1985.

[16] A. B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL’94, Kazimierz, Poland, number 933 in Lecture Notes in Computer Science. Springer-Verlag, June 1995. Preliminary version available as University of Edinburgh technical report ECS-LFCS-94-281, January 1994, under the title “Subtyping in F_{∧}^{ω} is decidable”.

[17] A. B. Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, University of Nijmegen, The Netherlands, January 1995. ISBN 90-9007860-6.

[18] A. B. Compagnoni and B. C. Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science, 6:469–501, 1996. Preliminary version available under the title Multiple Inheritance via Intersection Types as University of Edinburgh technical report ECS-LFCS-93-275 and Catholic University Nijmegen computer science technical report 93-18, Aug. 1993.

[19] T. Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.

[20] T. Coquand and J. Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. In Workshop on Logical Frameworks–Preliminary Proceedings, 1990.

[21] P.-L. Curien and G. Ghelli. Coherence of subsumption: Minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

REFERENCES 42

[22] M. Dezani-Ciancaglini and I. Margaria. A characterisation of F -complete type assignments. Theoretical Computer Science, 45:121–157, 1986.

[23] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[24] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994.

[25] H. Goguen. The metatheory of UTT. In Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 60–82, Baastad, Sweden, June 1995. Springer– Verlag.

[26] H. Goguen. Typed operational semantics. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 186–200. Springer–Verlag, 1995.

[27] C. A. Gunter and J. C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1994.

[28] P. Martin-Löf. An intuitionistic theory of types, 1972. Unpublished manuscript.

[29] J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289–305. Springer–Verlag, LNCS 664, Mar. 1993.

[30] J. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. North Holland, 1990.

[31] J. C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109–124, January 1990. Also in [27].

[32] B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991. Available as School of Computer Science technical report CMU-CS-91-205.

[33] M. Steffen and B. Pierce. Higher-order subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), June 1994. An earlier version appeared as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, February 1994.

[34] T. Streicher. Semantics of Type Theory: Correctness, Completeness and Independence Results. Birkhäuser, 1991.

[35] M. Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120–127, 1995.

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