A Framework for Internalizing Relations into
Type Theory
Peng Fu1 , Aaron Stump1 , and Jeff Vaughan212Computer Science, The University of Iowa
Computer Science, University of California, Los Angeles

Abstract. This paper introduces the concept of internalization structure, which can be used to incorporate certain relations into FΠ , a variantof system F, while maintaining termination of the new system. We willcall this process of incorporation internalization, FΠ the base system andthe new system after the incorporation the internalized system. We first
specify the syntax, and then the semantics of FΠ via the Tait-Girard
reducibility method. We then define internalization structure. We showthat we can obtain a terminating internalized system from an internalization structure. Finally, as motivating examples, we demonstrate how
our framework can be applied to internalize subtyping, full-beta term
equality and term-type inhabitation relations.

1

Introduction

Type systems, including the Calculus of Inductive Constructions [7] and F<: [13],incorporate auxiliary judgments in their typing relations. For example, the subtype judgment is a premise of F<: ’s subsumption rule:Γ ` t : T T <: T 0
subΓ ` t : T0
Likewise, the type-equivalence judgment appears in CIC’s conversion rule:Γ ` t : T T ≡ T 0 conv
Γ ` t : T0
Conventionally, adding a rule like sub or conv to a lambda calculus requires
ad-hoc reasoning about the auxiliary judgment system and its relation to theunderlying type theory. This paper proposes a new framework for defining language extensions in the style of sub or conv, and shows how to systematicallyverify that such extensions yield terminationing systems under call-by-name reduction.
We call deduction systems producing auxiliary judgments metasystems, andrefer to typing rules that modify types based such metasystem judgments automatic conversion rules. We will also consider cut-down type systems without
automatic conversion rules; these are called base systems.

For instance the subtyping (<:) and type-equivalence (≡) derivation systems
are metasystems, and rules sub and conv are automatic conversion rules. System F is F<: ’s base system. Automatic conversion rules may be viewed as abridge between a base system and a metasystem; metasystem derivations serve
as evidence that type conversion or subsumption should be allowed.
Type structure may be used to reflect metasystem judgments. Indeed this has
been done in several languages: equality sets in Martin-Löf type theory enablereasoning about equality relations [11], Sjöberg and Stump’s T vec uses types toreflect call-by-value term equality in the presence of divergence [16], and the
AuraConf language uses proofs of type e isa t to indicate expression e may becast to type t [18]. As we will see, the language extension framework proposedin this paper is implemented using a generalization of these ideas.
The Curry-Howard isomorphism enable us to view the base system as a kindof constructive logic. Once we internalized metasystem judgments as types, we
can reason about these judgments using the logic provided by the base system.
Moreover, we can derive new judgments by the internalized system not only justthrough metasystem. Later we will see how the internalized system realized this
aspect.
This paper introduces a new framework, internalization, that enables the systemic definition and investigation of λ-calculi with automatic conversion rules.
We use a dependent variant of polymorphic lambda calculus FΠ as a base system (Section 2). We then show how to create generalizations of FΠ —internalized
systems—given a compact internalization structure (Section 3). A sound internalization structure yields a terminating internalized system (Section 4). This
framework is powerful enough to augment FΠ with interesting features, including subtyping, conversion based on full-beta term joinability, and a reflectedtyping relation (Section 5). Finally this paper compares internalization withseveral related ideas from type theory (Section 6).
An internalization structure is a triple hD, E, Ii. Reflective relational sentences D define the syntax of metasystem propositions and identify valid metasystem judgments. Elimination relation E defines automatic conversion rules
based on judgments from D. Finally, interpretation I defines semantics for reflective relational sentences as relations over sets of terms. All internalization
structures require that D and E are sound. As a central result of our work, weshow that any sound internalized system constructed from an internalization
structure is guaranteed to be terminating.
The contributions of this work are as follows. We define internalization, aframework that enables the systematic study of automatic conversion rules andmetasystems relative to a base system. We instantiate this framework with respect to system FΠ , and prove that every internalization structure yields a new,terminating lambda calculus. Finally we demonstrate the utility of this methodology with examples.

2

Base system FΠ

Internalization builds off of base system FΠ , a variant of system F. FΠ ’s syntax
and operational semantics are given in Figure 1. We use call-by-name operationalsemantics. Key differences between F and FΠ are as follows:
1. FΠ is parametrized by a finite set B of constant types and it contains a
constant term axiom.
2. Values is extended by including constant terms.
3. FΠ uses dependent product Π instead of arrow → as the function type
constructor.
A word about the use of call-by-name reduction is warranted. The main
result of this paper is normalization for systems derived by internalization fromthe base system FΠ . Strong normalization does not hold for all such systems,
as we show by example in Section 5.1. So (weak) normalization is all that we
can obtain. An interesting result of our investigation into internalization is that
normalization with respect to call-by-name reduction imposes fewer requirements
on internalization structures than with call-by-value reduction. Specifically, theλ-abstraction case of the proof of Theorem 1 goes through more directly using
call-by-name reduction; with call-by-value reduction, dependent typing imposes
additional requirements on the internalization structure.
For FΠ , we use dependent product instead of arrow anticipating the useof internalization structures whose types mention terms. FΠ contains constantaxiom but does not give it a type; later, internalized systems will use axiom
to inhabit special types. Moreover, defining axiom now allows us to fix a single
universe of reducibility candidates and to use FΠ type interpretations directly
when interpreting these special internalized-system types.
2.1

Syntax of FΠ

Figure 2 gives the type assignment rules for FΠ . The definition of typing context
is standard. We define the judgment Γ ` OK for well-formedness of context Γas follows:· ` OKΓ ` OKΓ, X ` OK

Γ ` OK

FVar(T ) ⊆ dom(Γ )Γ, x : T ` OK

FVar(T ) means the set of free type variables and free term variables in type T .
dom(Γ ) means the domain of the context, i.e., e ∈ dom(Γ ) iff e is either a typevariable such that Γ ≡ Γ1 , e, Γ2 , or a term variable such that Γ ≡ Γ1 , e : T, Γ2 .
2.2

Interpretation of Types in FΠ

Reducibility is a well-known technique for proving the normalization of type systems such as F. In this paper, we use it to interpret FΠ ’s types. Reducibility willboth provide intuition for FΠ ’s semantics and yield a normalization result. To
begin, we define reducibility candidates following Girard’s Proofs and Types [9].

TypesT
Termst, uContexts C
Valuesv::= B | X | Πx : T.T | ∀X.T::= axiom | x | (t t) | λx.t::= [] | C t::= λx.t | axiom

C [(λx.t) t0 ] ; C [[t0 /x]t]
Fig. 1. Syntax and Operational Semantics of FΠ
(x : T ) ∈ Γ Γ ` OKVar
Γ `x:TΓ, x : T1 ` t : T2
Π-introΓ ` λx.t : Πx : T1 .T2

Γ ` t1 : Πx : T1 .T2 Γ ` t2 : T1
Π-elimΓ ` t1 t2 : [t2 /x]T2

Γ, X ` t : T∀-introΓ ` t : ∀X.T

Γ ` t : ∀X.T

F V ar(T 0 ) ⊆ dom(Γ )Γ ` t : [T 0 /X]T∀-elimFig. 2. Type Assignment System of FΠ

Definition 1. A reducibility candidate R is a set of terms that satisfies thefollowing conditions:
CR 1 If t ∈ R,then t ∈ V, where V is the set of closed terms that that reduces
to a value in Values.
CR 2 If t ∈ R and t ; t0 , then t0 ∈ R.
CR 3 If t is a closed term, t ; t0 and t0 ∈ R, then t ∈ R.
Definition 2. Let < be the set of all reducibility candidates. Let TVar be theset of all type variables. Let φ be a finite function with dom(φ) ⊆ TVar andrange(φ) ⊆ <. If dom(φ) = {X1 , X2 , ...Xn }, then we usually write φ as [R1 /X1 , ...Rn /Xn ].
Figure 3 defines the interpretation [[T ]]φ of a type T as a set of terms. Notethat constant types B and their interpretations RB are left unspecified; these
may be filled in later. For any [[T ]]φ , let F V (T ) be the set of free type variable
in T .we assume F V (T ) ⊆ dom(φ).
t ∈ [[B]]φiff t ∈ RB , where RB ∈ <t ∈ [[X]]φiff t ∈ φ(X)t ∈ [[Πx : T1 .T2 ]]φ iff t ∈ V and (∀u ∈ [[T1 ]]φ ⇒ (t u) ∈ [[[u/x]T2 ]]φ )t ∈ [[∀X.T ]]φiff ∀R ∈ <, t ∈ [[T ]]φ[R/X]
Fig. 3. Interpretation of Types in FΠ

2.3

Type Soundness

The theorem below shows that any typable closed term is normalizing, andcan be shown in a standard way using Tait-Girard reducibility (cf. [9]). Several
properties of the interpretation of types are required, which can all be provedby induction on the structure of types in FΠ . The proofs of the lemmas andtheorems below are relegated to the appendix.
Lemma 1. [[T ]]φ ∈ <, in the other words, the interpretation of a type is indeed
a reducibility candidate.
Lemma 2. Let Sub be the set of all capture avoiding term-level substitutions
with a domain of term variables and a range of terms that are in V. ∀σ ∈Sub, [[σT ]]φ = [[T ]]φ .
Since FΠ essentially is system F, it does not contain terms in the types, we haveσT ≡ T in FΠ , thus this lemma is true.
Lemma 3 (Substitution lemma). [[[T 0 /X]T ]]φ = [[T ]]φ[[[T 0 ]]φ /X] .
Definition 3. We define the set [Γ ] of well-typed substitutions (σ, δ) w.r.t. Γ
as follows:(∅, ∅) ∈ [.](σ, δ) ∈ [Γ ] R ∈ <(σ, δ ∪ {(X, R)}) ∈ [Γ, X](σ, δ) ∈ [Γ ] t ∈ [[σT ]]δ
(σ ∪ {(x, t)}, δ) ∈ [Γ, x : T ]Theorem 1 (Type Soundness). If Γ ` t : T , then ∀(σ, δ) ∈ [Γ ], (σ t) ∈[[σT ]]δ .

3

Internalized StructureInternalization is based on internalization structure. The internalization structure contains the information of how to construct reflective relational sentences
and how these reflective relational sentences interact with the base system. It
also gives the meaning of the reflective relational sentences through the interpretation of types in the base system. Once we define an internalization structure,
we can then begin the process of internalization by first internalizing the reflective relational sentences as types, then add two new typing rules to deal withthese reflective relational sentences.
Internalization structure consists of three parts, they are reflective relational
sentences, elimination relation and interpretation. Besides these three parts, aninternalization structure has two soundness properties, which we will identify
later. In this section, we will first describe these three parts of the internalization
structure and the two soundness properties of internalization structure. Thenwe will illustrate how to construct a new system, which is called internalized
system, from an internalization structure. The internalized system is shown to
be terminating.

3.1

Reflective Relational Sentence-D

We define the kind of judgments or relations that could be integrated into thebase system. Essentially these are the relations on the terms and types from thebase system.
Definition 4. Let signature Σ ⊆ Symbols × N × N, where Symbols means a
set of relation symbols, and N is the set of natural numbers. Rn×m ∈ Σ means
R ∈ Symbols and the arity of R is n + m.
Definition 5. A relational sentence on the basic system is a syntactic object ofform R(n×m) (t1 , ..., tn , T1 , ..., Tm ), where t, T are defined in FΠ and R(n×m) ∈ Σ.
Note that in this paper we do not deal with nesting relational sentences.
Definition 6. Let A be the set of all relational sentences. A set of reflective
relational sentences D is a subset of all relational sentences, i.e. D ⊆ A.
Reflective relational sentences are used to formalize a metasystem’s derivable
judgments. When we define specifically how to recognize the reflective relational
sentences from relational sentences, we obtain a kind of metasystem. This metasystem need not be recursive; it can be defined axiomatically.
3.2

Elimination Relation-E

An elimination relation is a syntactic constraint used to specify how the metasystem influences the base system. We will appeal to an elimination relation
when we add the elimination rule to the base system for the reflective relational
sentences. Since the elimination relation is used after internalizing reflective relational sentences as types, we need to extend the definition of types and thecontext accordingly.
Definition 7. We define extended types and extended contexts as follows:
(n×m)

(n×m)

RTypes A ::= R1(t1 , ..., tn , T1 , ..., Tm ) | ... | Rl
ETypes S ::= B | X | Πx : S.S | ∀X.S | A
EContext ∆ ::= · | ∆, x : S | ∆, X

(t1 , ..., tn , T1 , ..., Tm )We can see that the extended types and the extended context defined above
are really extended in the sense of adding the relational sentences as new types.
Definition 8. We specify an elimination relation E by:
E ⊆ EContext × Terms × Terms × A × ETypes × ETypes.
For example, when we consider the specific internalization structure for subtyping below, we will define an elimination relation where (∆, t, t0 , T < T 0 , T, T 0 ) ∈E holds iff in extended context ∆, t has the type T , t0 has the type T < T 0 , andwe can change the type of t to T 0 .

3.3Interpretation-I

We defined the interpretation of types of FΠ before. Since interpretation oftypes is a set of terms and the reflective relational sentences are relations about
between terms and types in FΠ , it is natural to understand the meaning of thesereflective relational sentences as set-theoretic relations between interpretation oftypes. Take subtyping as an example; we interpret subtype judgment <: as themathematical subset relation ⊆ on interpretation of types [14].
Interpretation-I is defined to capture this intuition. Later we will relateinterpretation-I to reflective relational sentences and elimination relation throughtwo soundness properties.
Definition 9. Let < be the set of all reducibility candidates as defined in FΠ .
We define an interpretation of R(n×m) –IR(n×m) to be IR(n×m) ⊆ Termsn × <m .
3.4

Soundness Properties

Now that we have defined all parts of an internalization structure, we can formulate two soundness properties for an internalization structure. Since one of
the soundness properties is related to the extended types, we first define theinterpretation for extended types. Then we identify the soundness properties.
Definition 10. Let φ be an environment function w.r.t. type S, which is definedin the same way as definition 2 except we extend it to type S. Let A be the setof closed terms that normalize at axiom. The interpretation of types [[S]]φ isdefined inductively as follows:– t ∈ [[B]]φ iff t ∈ RB .
– t ∈ [[X]]φ iff t ∈ φ(X).
– t ∈ [[Πx : S1 .S2 ]]φ iff t ∈ V and (∀u ∈ [[S1 ]]φ ⇒ (t u) ∈ [[[u/x]S2 ]]φ ).
– t ∈ [[∀X.S]]φ iff ∀R ∈ <, t ∈ [[S]]φ[R/X] .
– t ∈ [[R(n×m) (t1 , ..., tn , T1 , ..., Tm )]]φ iff t ∈ A and (t1 , ..., tn , [[T1 ]]φ , ..., [[Tm ]]φ ) ∈IR(n×m) .
Define (σ, δ) ∈ [∆] in the same way as (σ, δ) ∈ [Γ ], except with extended
contexts and extended types.
Definition 11. We say a tuple hD, E, Ii is an internalization structure iff itsatisfies the following soundness properties:– Soundness of reflective relational sentences
If R(n×m) (t1 , ..., tn , T1 , ..., Tm ) ∈ D, then∀φ, ∀σ ∈ Sub, (σt1 , ..., σtn , [[σT1 ]]φ , ..., [[σTm ]]φ ) ∈ IR(n×m) .
– Soundness of the elimination relation
Suppose (∆, t, t0 , R(n×m) (t1 , ..., tn , T1 , ..., Tm ), S, S 0 ) ∈ E, and (σ, δ) ∈ [∆].
Also, suppose σ(t) ∈ [[σS]]δ and R(n×m) (t1 , ..., tn , T1 , ..., Tm ) ∈ D. Thenσ(t) ∈ [[σS 0 ]]δ .

Soundness of reflective relational sentences means that the reflective relational sentences are a conservative approximation of interpretation-I. Soundnessof the elimination relation will imply that the elimination rule for internalized
systems respects the Girard-Tait type interpretation and is semantically compatible with substitutions that arise duing CBN evaluation. We will see that innext section. We can extend the lemmas from Section 2.3 above to our extended
interpretation of types:
Lemma 4. ∀φ, [[S]]φ ∈ <.
Lemma 5 (Substitution lemma). If [S 0 /X]S ∈ ETypes, then [[[S 0 /X]S]]φ =[[S]]φ[[[S 0 ]]φ /X] .

4

Internalized System

So far, we defined the internalization structure–hD, E, Ii. Now using an internalization structure, we can construct a new system–we call it the internalized
system–from the internalization structure and FΠ . The term syntax and operational semantics of internalized system are the same as FΠ , while the syntax oftypes and contexts are the RTypes, ETypes, EContexts in definition 7. The
well-formed extended context ∆ ` OK is defined just as before except using
EContexts. Figure 4 shows the new type assignment rules for the internalized
system. We can see that the new type assignment system contains two newrules:A-intro and A-elim. The A-intro rule is used to introduce reflective relational sentences as types in the internalized system, while the A-elim rule is forusing the reflective relational sentences to change the type of a term accordingly.
A∈D

∆`t:T

FVar(A) ⊆ dom(∆)∆ ` axiom : A∆ ` t0 : A∆ ` OK∆(x) = S ∆ ` OK
Var
∆`x:S

A-introE(∆, t, t0 , A, T, T 0 )∆ ` t : T0∆, x : S1 ` t : S2
Π intro∆ ` λx.t : Πx : S1 .S2A-elim∆, X ` t : S∀ intro∆ ` t : ∀X.S

∆ ` t1 : Πx : S1 .S2 ∆ ` t2 : S1
Π elim∆ ` t1 t2 : [t2 /x]S2∆ ` t : ∀X.S

[S 0 /X]S ∈ ETypes0∆ ` t : [S /X]SF V ar(S 0 ) ⊆ dom(∆)∀ elimFig. 4. Type Assignment System of Internalized System

The theorem below guarantees that the internalized system generated fromFΠ and internalization structure is terminating, which is the central result ofinternalization.

Theorem 2 (Type Soundness). If hD, E, Ii is an internalization structureand ∆ ` t : S, then ∀(σ, δ) ∈ [∆], (σ t) ∈ [[σS]]δ .
The proof of this theorem is in appendix.
Corollary 1. If · ` t : S, then t ∈ V.
Because typing contexts may introduce spurious assumptions, some open contexts may assign a type to a diverging term. Section 5.1 shows gives an example.
This is an expected outcome of reasoning from invalid premises. Indeed Corollary 1 may be strengthened to allow contexts where all variables are classified
by inhabited types.

5

ExamplesIn previous section, we capsule our development of internalized system as constructing a sound internalization structure. Now let us see how we can apply ourformalization of internalization to internalize subtyping, full-beta term equality
and term-type inhabitation relations as types. First, we specify an instance ofFΠ . Essentially, we instantiate constant types as B ::= > | ⊥. Additionally, wedefine [[⊥]]φ := ∅, [[>]]φ := V.
Recall that internalization works as follows. We first define the set of reflective
relational sentences that contains all the derivable judgments from subtyping,full-beta term equality and term-type inhabitation. Then we define the elimination relation and interpretation. We show our definition interpretation structure
is sound. Finally we present the internalized system as the result of internalization. We will follow this recipe in the sequel.
5.1

Subtyping

We need to instantiate the three parts of internalization structure-hD, E, Ii.
First, we specify Σ := {<0+2 }. Then we know all the reflective relational sentences should be in the form T1 < T2 . We identify reflective relational sentences
D as follows:
T <>∈D⊥<T ∈D

X<X∈D

T1 < T2 ∈ D∀X.T1 < ∀X.T2 ∈ D

T10 < T1 ∈ D T2 < T20 ∈ D
Πx : T1 .T2 < Πx : T10 .T20 ∈ D
We can see that the way we identify D is similar to the way we write subtyping
rules. Now we define E as follows:(∆, t, t0 , T < T 0 , T, T 0 ) ∈ E

The meaning of this elimination relation is that if t has type T in context ∆ andt0 has type T < T 0 , then t can also has the type T 0 .
We define interpretation I< :I< := {(R1 , R2 ) |R1 ⊆ R2 }We can see that I< capture all the subset relations on reducibility candidates.
The following two lemmas make sure we obtain a sound internalization structurefrom hD, E, I< i we defined above.
Lemma 6 (Soundness of the Reflective Relational Sentence). If (T <T 0 ) ∈ D, then ∀σ ∈ Sub, ∀φ, ([[σT ]]φ , [[σT 0 ]]φ ) ∈ I< .
Proof. Since [[σT ]]φ = [[T ]]φ by lemma 2. We just need to show: If (T < T 0 ) ∈ D,then ∀φ, ([[T ]]φ , [[T 0 ]]φ ) ∈ I< . We will prove this by induction on the structure ofT.
Case: T = > or T = ⊥By inversion, it holds.
Case: T = X
By inversion, we know T 0 = X or >, again, it is the case.
Case: T = Πx : T1 .T2
By inversion, T 0 = > or T 0 = Πx : T10 .T20 . Let us consider T 0 = Πx : T10 .T20 . In
this case, by inversion, T10 < T1 ∈ D, T2 < T20 ∈ D. By IH, we have [[T10 ]]φ ⊆ [[T1 ]]φ .
Again, by IH, we have [[T2 ]]φ ⊆ [[T20 ]]φ . For any u ∈ [[T10 ]]φ ⊆ [[T1 ]]φ , if t ∈ [[Πx :T1 .T2 ]]φ , we have tu ∈ [[[u/x]T2 ]]φ = [[T2 ]]φ ⊆ [[T20 ]]φ . So t ∈ [[Πx : T10 .T20 ]]φ .
Case: T = ∀X.T
By inversion, T 0 = > or ∀X.T 0 . So let’s consider T 0 = ∀X.T 0 . By inversion, weknow T < T 0 ∈ D. We know for t ∈ [[∀X.T ]]φ , ∀R ∈ <, t ∈ [[T ]]φ[R/X] . By IH,[[T ]]φ[R/X] ⊆ [[T 0 ]]φ[R/X] . So t ∈ [[∀X.T 0 ]]φ .
Lemma 7 (Soundness of the Elimination Relation).
If (∆, t, t0 , T1 < T2 , T1 , T2 ) ∈ E, (σ, δ) ∈ [∆] and σ(t) ∈ [[σT1 ]]δ = [[T1 ]]δ andT1 < T2 ∈ D, then σ(t) ∈ [[σT2 ]]δ = [[T2 ]]δ .
It is the case by soundness of the reflective relational sentences.
For this internalization structure–hD, E, I< i, the A-intro and A-elim rules
are equivalent to:
T1 < T2 ∈ D

FVar(T1 < T2 ) ⊆ dom(∆)∆ ` axiom : T1 < T2

∆ ` OK

A-intro∆ ` t : T1 ∆ ` t0 : T1 < T2
A-elim∆ ` t : T2
The subtyping setting also provides a clear illustration that it is possible tohave diverging term under open terms and full-beta reduction in internalized
system. Here it is possible to derivey : (> < (> → >)) ` (λx.xx)(λx.xx) : >using the underivable fact > < (> → >) and derivable (> → >) < > to establish
an isomorphism between types > and > → >. Sticking to closed terms means
we need not worry about this derivation directly. And call-by-name evaluation
ensures that· ` λy.(λx.xx)(λx.xx) : (> < (> → >)) → >does not reduce. In contrast, full reduction would loop.
5.2

Full-beta Term Equality, Term-Type Inhabitation

We can go even further to explore the internalization structure. We add two
more relation symbols to signature so that Σ = {↓(2+0) , <(0+2) , /(1+1) }. For
simplicity, we usually do not specify the arity. Thus the relational sentences
have form: t1 ↓ t2 , T1 < T2 , and t / T for base-system t and T .
Now we are ready to specify more reflective relational sentences. We define/ reflective relational sentences by the following condition:t / T ∈ D iff ∀φ, t ∈ [[T ]]φNotice that this definition is not algorithmic, which is fine since our framework
does not require decidability for the set D for reflective relational sentences.
The / symbol allows us to give “morally correct” types to terms which cannot otherwise be checked. In practice, such terms are created when extracting
computational content from mechanically checked proofs. As a concrete example, the Coq proof assistant uses an expressive language to define functional
programs and exports that code to OCaml for efficient compilation. Resulting
OCaml programs do not go wrong, but must use Obj.magic:α → β to pass ML’s
weaker type system. Likewise, AuraConf [18] uses a type constructor resembling/ to inform the type checker about the concealed types of opaque ciphertexts.
Note that weaker variants of / may be possible when, as in the case of extracted
proofs, there is a conservative procedure for checking semantic type inclusion,t /alt T ∈ D iff Oracle(t, T ). (We do not consider such variants further.)
We define t1 ↓ t2 ∈ D by the following rules:t↓t∈D(λx.t)t0 ↓ [t0 /x]t ∈ D

t1 ↓ t2 ∈ D
t1 t ↓ t2 t ∈ D

t1 ↓ t2 ∈ D
λx.t1 ↓ λx.t2 ∈ D

t1 ↓ t2 ∈ D
t t1 ↓ t t2 ∈ D

t1 ↓ t2 ∈ D t2 ↓ t3 ∈ D
t1 ↓ t3 ∈ D

t1 ↓ t2 ∈ D
t2 ↓ t1 ∈ D
The rules above are the same as how we define the conversion in lambda calculus. In this case, the syntax of extended types (as defined by the internalization
framework) is:
EType S ::= > | ⊥ | X | Πx : S.S | ∀X.S | t1 ↓ t2 | T1 < T2 | t / T

The additional elimination relations are:(∆, t, t0 , t1 ↓ t2 , [t1 /x](t3 ↓ t4 ), [t2 /x](t3 ↓ t4 )) ∈ E.
(∆, t, t0 , t / T 0 , T, T 0 ) ∈ E
The additional interpretations I↓ , I/ are:– I↓ ⊆ Terms × Terms defined by I↓ := {(t1 , t2 ) | t1 ↓ t2 ∈ D}.
– I/ ⊆ Terms × < defined by I/ := {(t, R) | t ∈ R}.
We have now defined the three parts of the internalization structure. We
need to show that this structure is sound. For that purpose, we have following
lemmas.
Lemma 8 (Soundness of the Reflective Relational Sentence).
– If (t1 ↓ t2 ) ∈ D, then ∀σ ∈ Sub, (σt1 , σt2 ) ∈ I↓ .
– If (t / T ) ∈ D, then ∀σ ∈ Sub, ∀φ, (σt, [[σT ]]φ ) ∈ I/ .
Proof. If (t1 ↓ t2 ) ∈ D, we have ∀σ ∈ Sub, (σt1 , σt2 ) ∈ D. This is because wedefine the t ↓ t0 relation same as the conversion in lambda calculus and this is
one of its properties. (see [4]) Thus (σt1 , σt2 ) ∈ I↓ by definition of I↓ .
If (t / T ) ∈ D, by definition, we have ∀φ, t ∈ [[T ]]φ . Since t is closed, ∀σ ∈Sub, σt ≡ t. And we have [[σT ]]φ = [[T ]]φ . So ∀φ, ∀σ ∈ Sub, σt ∈ [[σT ]]φ . Thus∀σ ∈ Sub, ∀φ, (σt, [[σT ]]φ ) ∈ I/ .
Lemma 9 (Soundness of the Elimination Relation).
– If (∆, t, t0 , t1 ↓ t2 , [t1 /x](t3 ↓ t4 ), [t2 /x](t3 ↓ t4 )) ∈ E, (σ, δ) ∈ [∆] andσ(t) ∈ [[σ[t1 /x](t3 ↓ t4 )]]δ and t1 ↓ t2 ∈ D, then σ(t) ∈ [[σ[t2 /x](t3 ↓ t4 )]]δ .
– If (∆, t, t0 , t / T 0 , T, T 0 ) ∈ E, (σ, δ) ∈ [∆] and σ(t) ∈ [[σT ]]δ and t / T 0 ∈ D,then σ(t) ∈ [[σT 0 ]]δ .
Proof. We have σ(t) ∈ [[σ[t1 /x](t3 ↓ t4 )]]δ , thus σ(t) ∈ A and (σ[t1 /x]t3 ) ↓(σ[t1 /x]t4 ) ∈ D. Since t1 ↓ t2 ∈ D, then we have (σ[t2 /x]t3 ) ↓ (σ[t2 /x]t4 ) ∈ D.
This is also followed by the property of t ↓ t0 (see [4]). So σ(t) ∈ [[σ[t2 /x](t3 ↓t4 )]]δ .
By soundness of reflective relational sentences, t / T 0 ∈ D implies ∀φ, σt = t ∈[[T 0 ]]φ . So it is the case.
So the structure hD, E, I< , I↓ , I/ i we have defined is a sound internalization
structure. Let us see some instances of A-elim rule and A-intro rule for theinternalized system based on this internalization structure:t1 ↓ t2 ∈ D

FVar(t1 ↓ t2 ) ⊆ dom(∆) ∆ ` OK
A-intro∆ ` axiom : t1 ↓ t2

∆ ` t : [t1 /x](t3 ↓ t4 ) ∆ ` t0 : t1 ↓ t2
∆ ` t : [t2 /x](t3 ↓ t4 )t / T0 ∈ D

A-elimFVar(t / T 0 ) ⊆ dom(∆) ∆ ` OK
A-intro∆ ` axiom : t / T 0∆ ` t : T ∆ ` t0 : t / T 0
A-elim∆ ` t : T0

We can see that our elimination rule for ↓ realizes a more general form oftransitivity. For example, if we have a term with a type [t2 /y](t1 ↓ y) andt2 ↓ t3 ∈ D, then we can assign this term a new type [t3 /y](t1 ↓ y) by theelimination rule.

6

Related Work

Reflection allows users of logical frameworks such as Coq or NuPRL to use
object-level definitions and computations as proxies or replacements for metalevel processes such as tactic application. NuPRL includes a built-in reflection
rule, showing (roughly) that H ` G follows from ` ∃p.p proves rep(H ` G).
A key difficulty in making this precise is reflecting uses of the reflection rule itself [6]. Solutions to this problem are given by [1] and [5]. Like the internalization
discussed in the present paper, reflection involves a subtle interaction between
the object- and meta-level. However, while reflection uses the object language
to replace meta-level reasoning, internalization uses systematic meta-level operations to extend and enhance the object language. Scharp seems to addresssimilar issues of internalization, from the perspective of natural language with
Tarski semantics [15].
Many type theories make direct use of auxiliary judgments. For example,
Pure Type Systems includes a conversion rule based on a convertibility judgment that is is not internalized as a type [3]. In CIC (and similar systems), one
can define an equality type inductively. In a sense this internalizes the convertibility judgment [12], but such an equality type cannot be used to change thetype of a given term; rather, an explicit cast is required. In contrast, the current
paper’s internalized equality can be used to change the type of a term without
an explicit cast. Cast terms raise a number of well-known problems, addressedusing axioms like Streicher’s axiom K [17]. Systems like the Implicit Calculusof Constructions have sought to alleviate similar problems by leaving term annotations implicit, although not for equality casts [10]. More recently, Sjöberg
and Stump have proposed a system where all such equality casts are implicit,
eliminating the practical need for methods like axiom K [16]. Indeed, providing
a framework to support systems like their T vec system is one motivation forthe present work. The problem of equality in type theory is, of course, one of
the most longstanding and central ones, and has been addressed in too many
works to summarize further (but see also [2] for a recent approach combining
intensional and extensional features).
Also related is language extension using meta-programming techniques. Felleisenbuilds a formal model describing the power of and limitations of macros forextending programming languages with new features [8]. As with internalization, macros can define “local” language extensions. In Felleisen’s setting locality is induced by a requirement that macro expansion be a homomorphism on
base-language syntax. In contrast to this syntactic approach, our internalization
framework specifies semantic constraints which, if satisfied, enable preservationof deep semantic properties of the system being extended.

7

Conclusion and Future Work

We have formalized the notion of internalization structure and demonstrated
that the internalized system is terminating. We also have shown how our formalization can be applied to full-beta term equality, subtyping and term-type
inhabitation relation. Our approach makes it easier to establish normalization
for type theories with these features, since the framework provides the analysis
for all but the internalization-specific parts of the language. In future work, we
hope to change our base system to the Calculus of Construction and see if we
can obtain a similar internalization structure from it. Also, we plan to proveother standard meta-theoretic results, such as type preservation (i.e. subject reduction). Another direction would be trying to find out more relations that canbe incorporated into base system through internalization.

References
1. Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The
semantics of reflected proof. In Proceedings of Fifth IEEE Symposium on Logic in
Computer Science, pages 95–197, 1990.
2. T. Altenkirch, C. McBride, and W. Swierstra. Observational Equality, Now! In
A. Stump and H. Xi, editors, PLPV ’07: Proceedings of the 2007 Workshop on
Programming Languages meets Program Verification, pages 57–68, 2007.
3. H. Barendregt. Lambda Calculi with Types. In S. Abramsky, D. Gabbay, andT. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University
Press, 1992.
4. H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co., 1984.
5. Eli Barzilay. Implementing Reflection in Nuprl. PhD thesis, Cornell, 2006.
6. Robert L. Constable. Using reflection to explain and enhance type theory. In Proof
and Computation, volume 139 of NATO Advanced Study Institute, International
Summer School held in Marktoberdorf, Germany, July 20-August 1, NATO SeriesF, pages 65–100. Springer, 1994.

7. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Lf
and Grigori Mints, editors, COLOG-88, volume 417 of Lecture Notes in Computer
Science, pages 50–66. Springer Berlin / Heidelberg, 1990.
8. Matthias Felleisen. On the expressive power of programming languages. In Scienceof Computer Programming, pages 134–151. Springer-Verlag, 1990.
9. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge
University Press, New York, NY, USA, 1989.
10. A. Miquel. The Implicit Calculus of Constructions. In Typed Lambda Calculi andApplications, volume 2044 of Lecture Notes in Computer Science, pages 344–359.
Springer, 2001.
11. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in MartinLöf ’s Type Theory: An Introduction. Oxford University Press, USA, July 1990.
12. F. Pfenning and C. Paulin-Mohring. Inductively Defined Types in the Calculus ofConstructions. In Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics, pages 209–228, London, UK, 1990.
Springer-Verlag.
13. Benjamin C. Pierce. Types and programming languages. MIT Press, Cambridge,
MA, USA, 2002.
14. Jakob Rehof. Strong normalization for non-structural subtyping via saturated sets.
Inf. Process. Lett., 58:157–162, May 1996.
15. Kevin Scharp. Truth and internalizability. Draft available from http://people.
cohums.ohio-state.edu/scharp1, 2010.
16. V. Sjöberg and A. Stump. Equality, Quasi-Implicit Products, and Large Eliminations. In B. Venneri, editor, Workshop on Intersection Types and Related Systems(ITRS), 2010.
17. T. Streicher. Investigations into Intensional Type Theory. PhD thesis, Ludwig
Maximilians University, Munich, 1993. Habilitation thesis.
18. Jeffrey A. Vaughan. Aura: Programming with Authorization and Audit. PhD thesis,
University of Pennsylvania, Philadelphia, 2009.

A

ProofsA.1

Proof of Lemma 1

Proof. By induction on the structure of T .
Case: T = X, B
CR 1–CR 3 Obvious from the definition.
Case: T = Πx : T1 .T2
CR 1 Obvious from the definition of [[Πx : T1 .T2 ]]φ .
CR 2 Assume t ∈ [[Πx : T1 .T2 ]]φ and t ; t0 . Take arbitrary u ∈ [[T1 ]]φ . By
definition, we know (t u) ∈ [[[u/x]T2 ]]φ . With our reduction strategy, (t u) ;(t0 u). By IH(CR 2), (t0 u) ∈ [[[u/x]T2 ]]φ . So by definition of [[Πx : T1 .T2 ]]φ ,t0 ∈ [[Πx : T1 .T2 ]]φ .
CR 3 Assume t is closed, t ; t0 and t0 ∈ [[Πx : T1 .T2 ]]φ . Take arbitrary u ∈[[T1 ]]φ . By definition, we know (t0 u) ∈ [[[u/x]T2 ]]φ . With our reduction strategy,(t u) ; (t0 u). By IH(CR 1), u is closed, thus we know (t u) is closed. By IH(CR3), (t u) ∈ [[[u/x]T2 ]]φ . So by definition of [[Πx : T1 .T2 ]]φ , t ∈ [[Πx : T1 .T2 ]]φ .
Case: T = ∀X.T
CR 1 Assume t ∈ [[∀X.T ]]φ . We know that < is non-empty (for example, V ∈<, this follow by lemma 10). Take an arbitrary reducibility candidate R. By
definition of [[∀X.T ]]φ , t ∈ [[T ]]φ[R/X] . By IH(CR 1), t ∈ V.
CR 2 Assume t ∈ [[∀X.T ]]φ and t ; t0 . Consider arbitrary reducibility candidate
R. By definition, t ∈ [[T ]]φ[R/X] . By IH(CR 2), t0 ∈ [[T ]]φ[R/X] . So by definitionof [[∀X.T ]]φ , t0 ∈ [[∀X.T ]]φ .
CR 3 Assume t is closed, t ; t0 and t0 ∈ [[∀X.T ]]φ . Take arbitrary reducibility
candidate R. By definition, t0 ∈ [[T ]]φ[R/X] . We know that t ; t0 and t is closed.
So by IH(CR 3), t ∈ [[T ]]φ[R/X] . So by definition of [[∀X.T ]]φ , t ∈ [[∀X.T ]]φ .
∗Lemma 10. Let B ⊆ V. We have B̂ = {t | ∃v ∈ B, t ; v and t closed } ∈ <.
Proof. CR1: t ∈ B̂ implies t ∈ V.
CR2: If t ∈ B̂ and t ; t0 , again by definition of B̂, we have t0 ∈ B̂.
CR3: Similar argument as CR2.

A.2

Proof of Lemma 3

Proof. By induction on the structure of T .
Case: T = X, B
If T = B, trivial. If T = X, we need to show [[T 0 ]]φ = [[X]]φ[[[T 0 ]]φ /X] . By definition,[[X]]φ[[[T 0 ]]φ /X] = φ[[[T 0 ]]φ /X](X) = [[T 0 ]]φ . If T = Y 6= X, then [[[T 0 /X]Y ]]φ =[[Y ]]φ = [[Y ]]φ[[[T 0 ]]φ /X] . So it is the case.
Case: T = ∀X1 .T1Then we need to show [[(∀X1 .[T 0 /X]T1 )]]φ = [[∀X1 .T1 ]]φ[[[T 0 ]]φ /X] . Take arbitrary
R ∈ < and arbitrary t ∈ [[(∀X1 .[T 0 /X]T1 )]]φ . By definition, t ∈ [[[T 0 /X]T1 ]]φ[R/X1 ] .
By IH, [[[T 0 /X]T1 ]]φ[R/X1 ] = [[T1 ]]φ[R/X1 ,[[T 0 ]]φ[R/X1 ] /X] = [[T1 ]]φ[R/X1 ,[[T 0 ]]φ /X] ,since we may assume X1 ∈/ F V (T 0 ). So t ∈ [[T1 ]]φ[R/X1 ,[[T 0 ]]φ /X] . By definition,t ∈ [[∀X1 .T1 ]]φ[[[T 0 ]]φ /X] .
Now let’s prove the other direction. Take arbitrary t ∈ [[∀X1 .T1 ]]φ[[[T 0 ]]φ /X] andarbitrary R ∈ <. By definition, t ∈ [[T1 ]]φ[[[T 0 ]]φ /X,R/X1 ] . By IH, [[T1 ]]φ[[[T 0 ]]φ /X,R/X1 ] =[[[T 0 /X]T1 ]]φ[R/X1 ] . So t ∈ [[[T 0 /X]T1 ]]φ[R/X1 ] . By definition, t ∈ [[∀X1 .[T 0 /X]T1 ]]φ .
So it is the case.
Case: T = Πx : T1 .T2Then we need to show [[(Πx : [T 0 /X]T1 .[T 0 /X]T2 )]]φ = [[(Πx : T1 .T2 )]]φ[[[T 0 ]]φ /X] .
Take arbitrary u ∈ [[([T 0 /X]T1 )]]φ and t ∈ [[Πx : [T 0 /X]T1 .[T 0 /X]T2 )]]φ . By definition, (t u) ∈ [[([u/x][T 0 /X]T2 )]]φ = [[[T 0 /X]([u/x]T2 )]]φ . By IH, [[([T 0 /X]T1 )]]φ =[[T1 ]]φ[[[T 0 ]]φ /X] and [[[T 0 /X]([u/x]T2 )]]φ = [[[u/x]T2 ]]φ[[[T 0 ]]φ /X] . So t ∈ [[Πx : T1 .T2 ]]φ[[[T 0 ]]φ /X] .
The other direction is similar.
A.3

Proof of Theorem 1

Proof. By induction on the typing derivation of Γ ` t : TCase:Γ (x) = TΓ `x:T
By definition of (σ, δ) ∈ [Γ ], there exists t such that {(x, t)} ⊆ σ and t ∈ [[σ(T )]]δ ,so σ x = t ∈ [[σ(T )]]δ .
Case:Γ ` t1 : Πx : T1 .T2 Γ ` t2 : T1
Γ ` t1 t2 : [t2 /x]T2

We need to prove that σ(t1 t2 ) ∈ [[σ([t2 /x]T2 )]]δ . By IH, for any (σ, δ) ∈ [Γ ], σ t1 ∈[[Πx : σT1 .σT2 ]]δ and σ t2 ∈ [[σT1 ]]δ . Then from definition of [[Πx : σT1 .σT2 ]]δ , wehave (σt1 )(σt2 ) = σ(t1 t2 ) ∈ [[[σ(t2 )/x](σT2 )]]δ . So we need to show [[σ([t2 /x]T2 )]]δ =[[[σ(t2 )/x](σT2 )]]δ , which is true.
Case:Γ, x : T1 ` t : T2
Γ ` λx.t : Πx : T1 .T2
We need to show that for all (σ, δ) ∈ [Γ ], we have σ(λx.t) = λx.(σ t) ∈[[Πx : σT1 .σT2 ]]δ . First, we know that λx.(σ t) ∈ V. Then by definition of[[Πx : σT1 .σT2 ]]δ ,we need to show for arbitrary u ∈ [[σT1 ]]δ , (λx.(σ t)) u ∈[[[u/x](σT2 )]]δ . Since we use LTR-CBN, we have (λx.(σ t)) u ; σ[u/x]t. Sinceu ∈ [[σT1 ]]δ ,(σ ∪ {(x, u)}, δ) ∈ [Γ, x : T1 ]. By IH, σ[u/x](t) ∈ [[(σ[u/x]T2 )]]δ . Since(λx.(σ t)) u is closed ,by CR 3, (λx.(σ t)) u ∈ [[(σ[u/x]T2 )]]δ . So it is the case.
Case:Γ, X ` t : TΓ ` t : ∀X.T
We need to show for any (σ, δ) ∈ [Γ ], σ(t) ∈ [[σ∀X.T ]]δ . By definition of[[σ∀X.T ]]δ , we just need to show for arbitrary R ∈ <, σ(t) ∈ [[σT ]]δ[R/X] . By
IH, for any (σ, δ ∪ {(X, R)}) ∈ [Γ, X], so σ(t) ∈ [[(σT )]]δ[R/X] . So it is the case.
Case:Γ ` t : ∀X.T
Γ ` t : ([T 0 /X]T )We need to show for any (σ, δ) ∈ [Γ ], σ(t) ∈ [[([σT 0 /X]σT )]]δ . By IH, we knowthat σ(t) ∈ [[(∀X.σT )]]δ . By definition, for any R ∈ <, σ(t) ∈ [[(σT )]]δ[R/X] . Since[[σT 0 ]]δ is a reducibility candidate, we have σ(t) ∈ [[(σT )]]δ[[[σT 0 ]]δ /X] . By lemma
3 (Substitution Lemma), we know [[([σT 0 /X]σT )]]δ = [[(σT )]]δ[[[σT 0 ]]δ /X] . So it is
the case.
A.4

Proof of Lemma 4

Proof. By induction on the structure of S.
Case: S = X, B
CR 1–CR 3 Obvious from the definition.

Case: S = Πx : S1 .S2
CR 1 Obvious from the definition of [[Πx : S1 .S2 ]]φ .
CR 2 Assume t ∈ [[Πx : S1 .S2 ]]φ and t ; t0 . Take arbitrary u ∈ [[S1 ]]φ . By
definition, we know (t u) ∈ [[[u/x]S2 ]]φ . With our reduction strategy, (t u) ;(t0 u). By IH(CR 2), (t0 u) ∈ [[[u/x]S2 ]]φ . So by definition of [[Πx : S1 .S2 ]]φ ,t0 ∈ [[Πx : S1 .S2 ]]φ .
CR 3 Assume t is closed, t ; t0 and t0 ∈ [[Πx : S1 .S2 ]]φ . Take arbitrary u ∈[[S1 ]]φ . By definition, we know (t0 u) ∈ [[[u/x]S2 ]]φ . With our reduction strategy,(t u) ; (t0 u). By IH(CR 1), u is closed, thus we know (t u) is closed. By IH(CR3), (t u) ∈ [[[u/x]S2 ]]φ . So by definition of [[Πx : S1 .S2 ]]φ , t ∈ [[Πx : S1 .S2 ]]φ .
Case: S = ∀X.S
CR 1 Assume t ∈ [[∀X.S]]φ . We know that < is non-empty (for example, V ∈<). Take an arbitrary reducibility candidate R. By definition of [[∀X.S]]φ , t ∈[[S]]φ[R/X] . By IH(CR 1), t ∈ V.
CR 2 Assume t ∈ [[∀X.S]]φ and t ; t0 . Consider arbitrary reducibility candidate
R. By definition, t ∈ [[S]]φ[R/X] . By IH(CR 2), t0 ∈ [[S]]φ[R/X] . So by definitionof [[∀X.S]]φ , t0 ∈ [[∀X.S]]φ .
CR 3 Assume t is closed, t ; t0 and t0 ∈ [[∀X.S]]φ . Take arbitrary reducibility
candidate R. By definition, t0 ∈ [[S]]φ[R/X] . We know that t ; t0 and t is closed.
So by IH(CR 3), t ∈ [[S]]φ[R/X] . So by definition of [[∀X.S]]φ , t ∈ [[∀X.S]]φ .
Case: S = A
By definition we know that [[S]]φ is either an empty set or A. Since {axiom} ⊆ V,
by lemma 10, we have A ∈ <.
A.5

Proof of Lemma 5

Proof. Prove by induction on the structure of S.
Case: S = X, B
If S = B, trivial. If S = X, we need to show [[S 0 ]]φ = [[X]]φ[[[S 0 ]]φ /X] . By definition,[[X]]φ[[[S 0 ]]φ /X] = φ[[[S 0 ]]φ /X](X) = [[S 0 ]]φ .
Case: S = ∀X1 .S1
We have ∀X1 .[S 0 /X]S1 ∈ ETypes. Thus we also have [S 0 /X]S1 ∈ ETypes. We
need to show [[(∀X1 .[S 0 /X]S1 )]]φ = [[∀X1 .S1 ]]φ[[[S 0 ]]φ /X] . Take arbitrary R ∈ <and arbitrary t ∈ [[(∀X1 .[S 0 /X]S1 )]]φ . By definition, t ∈ [[[S 0 /X]S1 ]]φ[R/X1 ] . By
IH, [[[S 0 /X]S1 ]]φ[R/X1 ] = [[S1 ]]φ[R/X1 ,[[S 0 ]]φ[R/X1 ] /X] = [[S1 ]]φ[R/X1 ,[[S 0 ]]φ /X] . So t ∈[[S1 ]]φ[R/X1 ,[[S 0 ]]φ /X] . By definition, t ∈ [[∀X1 .S1 ]]φ[[[S 0 ]]φ /X] .
Now let’s prove the other direction. Take arbitrary t ∈ [[∀X1 .S1 ]]φ[[[S 0 ]]φ /X] and arbitrary R ∈ <. By definition, t ∈ [[S1 ]]φ[[[S 0 ]]φ /X,R/X1 ] . By IH, [[S1 ]]φ[[[S 0 ]]φ /X,R/X1 ] =[[[S 0 /X]S1 ]]φ[R/X1 ] . So t ∈ [[[S 0 /X]S1 ]]φ[R/X1 ] . By definition, t ∈ [[∀X1 .[S 0 /X]S1 ]]φ .
So it is the case.
Case: S = Πx : S1 .S2
We have Πx : [S 0 /X]S1 .[S 0 /X]S2 ∈ ETypes and [S 0 /X]S1 , [S 0 /X]S2 ∈ ETypes.
Then we need to show [[(Πx : [S 0 /X]S1 .[S 0 /X]S2 )]]φ = [[(Πx : S1 .S2 )]]φ[[[S 0 ]]φ /X] .
Take arbitrary u ∈ [[([S 0 /X]S1 )]]φ and t ∈ [[Πx : [S 0 /X]S1 .[S 0 /X]S2 )]]φ . By definition, (t u) ∈ [[([u/x][S 0 /X]S2 )]]φ = [[[S 0 /X]([u/x]S2 )]]φ . By IH, [[([S 0 /X]S1 )]]φ =[[S1 ]]φ[[[S 0 ]]φ /X] and [[[S 0 /X]([u/x]S2 )]]φ = [[[u/x]S2 ]]φ[[[S 0 ]]φ /X] . So t ∈ [[Πx : S1 .S2 ]]φ[[[S 0 ]]φ /X] .
The other direction is similar.
Case: S = A
We have R(n×m) (t1 , ..., tn , [S 0 /X]T1 , ..., [S 0 /X]Tm ) ∈ ETypes. If ∀i ∈ {1, 2, ..., m}, X ∈/F V (Ti ), then it is trivially true. Otherwise we have S 0 ∈ Types. We need toshow[[R(n×m) (t1 , ..., tn , [S 0 /X]T1 , ..., [S 0 /X]Tm )]]φ =[[R(n×m) (t1 , ..., tn , T1 , ..., Tm )]]φ[[[S 0 ]]φ /X] .
By definition, we need to show
(t1 , ..., tn , [[[S 0 /X]T1 ]]φ , ..., [[[S 0 /X]Tm ]]φ ) ∈ IR(n×m) ⇔(t1 , ..., tn , [[T1 ]]φ[[[S 0 ]]φ /X] , ..., [[Tm ]]φ[[[S 0 ]]φ /X] ) ∈ IR(n×m)
which is true because lemma 3.
A.6

Proof of Theorem 2

proof By induction on the typing derivation of ∆ ` t : S
Case:(x : S) ∈ ∆ ∆ ` OK∆`x:S
By definition of (σ, δ) ∈ [∆], there exists t such that t ∈ [[σ(S)]]δ . Thus (x, t) ∈ σ.
So σ x = t ∈ [[σ(S)]]δ .
Case:∆ ` t1 : Πx.S1 .S2 ∆ ` t2 : S1
∆ ` t1 t2 : [t2 /x]S2

We need to prove that σ(t1 t2 ) ∈ [[σ([t2 /x]S2 )]]δ . By IH, for any (σ, δ) ∈ [∆], σ t1 ∈[[Πx : σS1 .σS2 ]]δ and σ t2 ∈ [[σS1 ]]δ . Then from definition of [[Πx : σS1 .σS2 ]]δ , wehave (σt1 )(σt2 ) = σ(t1 t2 ) ∈ [[[σ(t2 )/x](σS2 )]]δ . So we need to show [[σ([t2 /x]S2 )]]δ =[[[σ(t2 )/x](σS2 )]]δ , which is true.
Case:∆, x : S1 ` t : S2
∆ ` λx.t : Πx : S1 .S2
We need to show that for any (σ, δ) ∈ [∆], we have σ(λx.t) = λx.(σ t) ∈[[Πx : σS1 .σS2 ]]δ . First, we know that λx.(σ t) ∈ V. Then by definition of[[Πx : σS1 .σS2 ]]δ ,we need to show for arbitrary u ∈ [[σS1 ]]δ , (λx.(σ t)) u ∈[[[u/x](σS2 )]]δ . u is closed by CR 1. By LTR-CBN, we have (λx.(σ t)) u ;σ[u/x]t. Since u ∈ [[σS1 ]]δ ,(σ ∪ {(x, u)}, δ) ∈ [∆, x : S1 ]. By IH, σ[u/x](t) ∈[[(σ[u/x]S2 )]]δ . Since (λx.(σ t)) u is closed, by CR 3, (λx.(σ t)) u ∈ [[(σ[u/x]S2 )]]δ .
So it is the case.
Notice that if we use LTR-CBV as underlying operational semantics, to show
λx.(σ t) ∈ [[Πx : σS1 .σS2 ]]δ , we need to show for any u ∈ [[σS1 ]]δ , (λx.(σ t)) u ∈∗[[[u/x](σS2 )]]δ . Since we use CBV, we have (λx.(σ t)) u ; (λx.(σ t)) v ; [v/x]σt.
Since v ∈ [[σS1 ]]δ , by IH and CR3, we have (λx.(σ t)) u ∈ [[(σ[v/x]S2 )]]δ . Thus
we need another lemma stating: if t ; t0 , then [[[t/x]S]]δ = [[[t0 /x]S2 ]]δ . Thus it
is more complicated in this situation.
Case:∆, X ` t : S∆ ` t : ∀X.S
We need to show for any (σ, δ) ∈ [∆], σ(t) ∈ [[σ∀X.S]]δ . By definition of[[σ∀X.S]]δ , we just need to show for arbitrary R ∈ <, σ(t) ∈ [[σS]]δ[R/X] . By
IH, for (σ, δ ∪ {(X, R)}) ∈ [∆], we have σ(t) ∈ [[(σS)]]δ[R/X] . So it is the case.
Case:∆ ` t : ∀X.S

[S 0 /X]S ∈ ETypes F V ar(S 0 ) ⊆ dom(∆)∆ ` t : ([S 0 /X]S)We need to show for any (σ, δ) ∈ [∆], σ(t) ∈ [[([σS 0 /X]σS)]]δ . By IH, we knowthat σ(t) ∈ [[(∀X.σS)]]δ . By definition, for any R ∈ <, σ(t) ∈ [[(σS)]]δ[R/X] . Since[[σS 0 ]]δ is a reducibility candidate, we have σ(t) ∈ [[(σS)]]δ[[[σS 0 ]]δ /X] . By lemma
5 (Substitution Lemma), we know [[([σS 0 /X]σS)]]δ = [[(σS)]]δ[[[σS 0 ]]δ /X] . So it is
the case.

Case:A∈D

FVar(A) ⊆ dom(∆) ∆ ` OK
∆ ` axiom : A

We need to show if (σ, δ) ∈ [∆], dom(∆) = FVar(A) and A ∈ D, then axiom ∈[[σA]]δ . Let A = R(n×m) (t1 , ..., tn , T1 , ..., Tm ). Thus we need to show (σt1 , ..., σtn , [[σT1 ]]δ , ..., [[σTm ]]δ ) ∈IR(n×m) . By the soundness of reflective relational sentences, we know it is
the case.
Case:
∆`t:T

∆ ` t0 : A E(∆, t, t0 , A, T, T 0 )A-elim∆ ` t : T0

We have (σ, δ) ∈ [∆], σ(t) ∈ [[σT ]]δ , σ(t0 ) ∈ [[σA]]δ and E(∆, t, t0 , A, T, T 0 ). We
know that it is the case by Soundness of elimination relation.