1

# A Two-Level Linear Dependent Type Theory

Qiancheng Fu  Boston UniversityBostonMAUSA<EMAIL_ADDRESS>and  Hongwei Xi  Boston
UniversityBostonMAUSA<EMAIL_ADDRESS>
###### Abstract.

We present a type theory combining both linearity and dependency by
stratifying typing rules into a level for logics and a level for programs. The
distinction between logics and programs decouples their semantics, allowing
the type system to assume tight resource bounds. A natural notion of
irrelevancy is established where all proofs and types occurring inside
programs are fully erasable without compromising their operational behavior.
Through a heap-based operational semantics, we show that extracted programs
always make computational progress and run memory clean. Additionally,
programs can be freely reflected into the logical level for conducting deep
proofs in the style of standard dependent type theories. This enables one to
write resource safe programs and verify their correctness using a unified
language.

type theory, linear logic, computational relevancy, heap semantics

††journal: PACMPL††journalnumber: CONF††journalyear: 2023††publicationmonth:
1††copyright: none

##  1\. Introduction

Constructing programs and proving their properties are primary functions of
computer science. It did not take long for researchers to realize that a deep
connection exists between these activities. Proofs can be viewed as programs
mapping assumptions to conclusions and programs can be viewed as proofs of the
propositions induced by types. This realization lead to the Curry-Howard
correspondence viewpoint which identifies proofs and programs as the same
mathematical objects. Dependent type theories (Martin-Löf, 1975; Coquand and
Huet, 1988; Luo, 1994) make this connection even more concrete by expressing
proofs and programs using a single unified language.

Despite these theoretical observations, the generality of the Curry-Howard
correspondence is still a contentious subject. It does not take much time to
notice that the focal points of theorem proving and program construction are
different. On the one hand, the value of a proof lies in its ability to assert
the validity of a proposition by being assigned the type corresponding to this
proposition. In other words, the reduction behavior (computation) of a proof
is not as important as the fact that it is well-typed. Proofs utilizing
classical axioms such as the law of excluded middle or the axiom of choice may
not reduce at all. On the other hand, the value of a program lies in its
ability to perform computation and transform the world around it (sometimes
irreversibly). Many programming languages such as C do not have clear analogs
in the proof theoretic world and yet have greatly impacted modern society
solely through their computational capabilities.

As a step towards bridging the gap between proofs and programs, we introduce
the dependent type theory TLL whose typing rules are stratified into a logical
level and a program level. Now that proofs and programs are no longer bound
together in a monolithic type system, typing rules can be refined to
characterize their subjects of interest more precisely. At the logical level,
the typing rules here are concerned with the formation of propositions (types)
and their proofs (terms). Overall, the logical level is similar to Martin-Löf
type theory (Martin-Löf, 1975) and enjoys many of the same meta theoretical
properties. For the typing rules at the program level, they support an
intrinsic notion of resources inspired by Linear Logic (Girard, 1987) to
encode irreversible real world interactions. Due to the fact that the
operational semantics of the two levels can be decoupled, we choose a call-by-
value style semantics for programs as this allows the program typing rules to
assume tight resource bounds. Additionally, TLL types are allowed to depend on
linearly typed programs in a computationally irrelevant manner. This enables
one to reason about resources hypothetically without actually consuming them.

In order to show that TLL guarantees productive programs and safe resource
usage, we develop a type directed erasure procedure and a heap semantics
inspired by Turner and Wadler (Turner and Wadler, 1999). During erasure, the
syntax tree of a well-typed program is stripped of all type annotations and
computationally irrelevant terms. The program extracted from erasure is then
evaluated using our heap semantics. As the program evaluates, heap cells are
dynamically allocated and freed when linearly typed values are constructed and
consumed. We prove that our calculus is sound with regards to this erasure
procedure and heap semantics, ensuring evaluation progress and safe memory
usage at runtime.

All lemmas and theorems reported in this paper are formalized and proven
correct in Coq (The Coq Development Team, 2020). We also implement a compiler
in OCaml that compiles TLL programs into C. Proofs, source code and example
programs are available in our git repository 111https://github.com/qcfu-
bu/TLL-arxiv-repo.

In summary, we make the following contributions:

  * •

First, we design TLL, a two-level linear dependent type system. By stratifying
the typing rules into a logical level and a program level, we are able to
characterize proofs and programs more precisely.

  * •

Second, we study the meta-theoretical properties of the two levels. We show
that the logical level exhibits qualities such as confluence and strong
normalization that make it suitable for logical reasoning.

  * •

Furthermore, we design an erasure procedure and heap semantics that model the
behavior of programs at runtime. Using this semantics, we show programs
extracted from erasure run memory clean.

  * •

The entire calculus with its meta theories is formalized and proven correct in
Coq. We also implement a compiler in OCaml with many supporting examples.

##  2\. Overall Structure

The syntax of TLL is presented in Figure 2.

The typing rules of TLL are stratified into a level for logics and a level for
programs. This is expressed formally through the two judgments depicted in
Figure 1. The logical typing judgment ${\Gamma\vdash m:A}$ states that term
$m$ has type $A$ under logical context $\Gamma$. The program typing judgment
${\Gamma;\Delta\vdash m:A}$ states that term $m$ has type $A$ under logical
context $\Gamma$ and program context $\Delta$.

$\displaystyle\Gamma\vdash m:A$ $\displaystyle\Gamma;\Delta\vdash m:A$ Figure
1. Logical and Program Typing

TLL utilizes two sorts L and U to distinguish between the modalities of types
(linear and non-linear respectively). When an arbitrary type $A$ is of the
sort L, we say that this type is linear. If $A$ is of sort U, we say that this
type is non-linear. In order to avoid Girard’s paradox, sorts can be endowed
with universe levels in the usual way, but we do not do so in this paper for
the sake of presentation clarity.

From a logical typing perspective, modality has no effect. This follows the
intuition that hypothetical reasoning about resources does not consume them.
The type system at the logical level essentially boils down to standard
dependent type theory with extra modality and relevancy annotations.

At the program level, the modalities of types come into effect.
Computationally relevant terms of linear types must be used exactly once and
terms which are computationally irrelevant or of non-linear types can be used
freely. This is accomplished by carefully controlling how contraction and
weakening rules are applied to the program context $\Delta$.

For well-typed programs, a type directed erasure procedure can be carried out
to remove all type annotations and sub-terms occurring in computationally
irrelevant positions. The erasure soundness theorems guarantee that programs
extracted by erasure always make computational progress in a manner that is
compatible with their original non-erased counterparts.

sorts | $s,r,t$ | ::= |  U | L
---|---|---|---
terms | $m,n,A,B$ | ::= |  $x$ | $s$
|  |  | |  $\Pi_{t}({x:A}).{B}$ | $\Pi_{t}\\{{x:A}\\}.{B}$
|  |  | |  $\lambda_{t}({x:A}).{m}$ | $\lambda_{t}\\{{x:A}\\}.{m}$
|  |  | |  $m\ n$ | $\square$ | ${*l}$
Figure 2. Syntax of TLL

##  3\. Logical Typing

This section describes the typing rules in the logical level. Some of these
rules will appear to be redundant as type modality and computational relevancy
hold no weight at the logical level where essentially everything is
computationally irrelevant. However, the importance of these rules lies in
their interactions with program typing which is presented in Section 4.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
5.82657pt\vbox{\vbox{}\hbox{\hskip-5.82655pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon\vdash$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
53.36882pt\vbox{\hbox{\hskip-53.3688pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash A:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\Gamma$}}}}}\vbox{}}}\over\hbox{\hskip
18.0094pt\vbox{\vbox{}\hbox{\hskip-18.00938pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash$}}}}}}$
Figure 3. Logical Context

###  3.1. Type Formation

The type formation rules presented in Figure 4 appear at the logical level.
They determine the canonical forms of types. An obvious departure from
standard formalizations of dependent type theory is the presence of two kinds
of $\Pi$-types.

The first of these is the $\Pi{0}$-type of the form $\Pi_{t}\\{{x:A}\\}.{B}$.
We refer to the $\lambda$-terms inhabiting $\Pi{0}$-types at the program level
as $\lambda{0}$-programs. For $\lambda{0}$-programs, their arguments may only
be used irrelevantly within their bodies. This is similar in spirit to the
$\Lambda$-quantifier of System F where type parameterized terms behave
computationally the same regardless of the choice of type instantiation.
However, $\Pi{0}$-types are richer than $\Lambda$-quantifiers in the sense
that they can depend on arbitrary terms and not just types.

The $\Pi{1}$-type of the form $\Pi_{t}({x:A}).{B}$ is the usual function type.
Similarly to the $\Pi{0}$-type case, we refer to the $\lambda$-terms
inhabiting $\Pi{1}$-types at the program level as $\lambda{1}$-programs. The
arguments of $\lambda{1}$-programs are allowed to be used relevantly in their
bodies.

$\displaystyle\displaystyle{\hbox{\hskip
6.81252pt\vbox{\hbox{\hskip-6.8125pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash$}}}\vbox{}}}\over\hbox{\hskip
16.04689pt\vbox{\vbox{}\hbox{\hskip-16.04689pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
s:\text{U}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
55.10059pt\vbox{\hbox{\hskip-55.10057pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
A:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
B:r$}}}}\vbox{}}}\over\hbox{\hskip
36.05849pt\vbox{\vbox{}\hbox{\hskip-36.05849pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\Pi_{t}\\{{x:A}\\}.{B}:t$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
55.10059pt\vbox{\hbox{\hskip-55.10057pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
A:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
B:r$}}}}\vbox{}}}\over\hbox{\hskip
34.55847pt\vbox{\vbox{}\hbox{\hskip-34.55847pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\Pi_{t}({x:A}).{B}:t$}}}}}}$
Figure 4. Type Formation

One final detail that we want to emphasize about $\Pi$-types in TLL is the
sort annotation $t$. It is clear from the typing rules here that sort $s$ of
the domain, sort $r$ of the codomain and $t$ are not correlated. The $t$
annotation controls the modality of the overall $\Pi$-type intrinsically,
meaning that if $t$ is set to L, then the $\lambda$-programs inhabiting this
type must be applied exactly once. In Section 4, we will see how the $t$
annotation imposes constraints on $\lambda$-program construction.

###  3.2. Logical Terms

The typing rules for logical terms are presented in Figure 5. We can see from
the lack of sub-structural restrictions and the symmetry between the rules
concerning $\Pi{0}$-types and $\Pi{1}$-types that the terms at the logical
level are just Martin-Löf terms (Martin-Löf, 1975) with extra annotations. The
relation ${A}\simeq{B}$ asserted by the last rule is the usual definitional
equality relation stating that $A$ and $B$ are convertible through logical
reductions (Section 6.1).

$\displaystyle\displaystyle{\hbox{\hskip
33.82193pt\vbox{\hbox{\hskip-33.82191pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x:A\in\Gamma$}}}}\vbox{}}}\over\hbox{\hskip
17.7594pt\vbox{\vbox{}\hbox{\hskip-17.75938pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
x:A$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
30.59952pt\vbox{\hbox{\hskip-30.59952pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
m:B$}}}\vbox{}}}\over\hbox{\hskip
57.86646pt\vbox{\vbox{}\hbox{\hskip-57.86646pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\lambda_{t}\\{{x:A}\\}.{m}:\Pi_{t}\\{{x:A}\\}.{B}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
30.59952pt\vbox{\hbox{\hskip-30.59952pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
m:B$}}}\vbox{}}}\over\hbox{\hskip
54.86642pt\vbox{\vbox{}\hbox{\hskip-54.86642pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\lambda_{t}({x:A}).{m}:\Pi_{t}({x:A}).{B}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
66.52313pt\vbox{\hbox{\hskip-66.52313pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:\Pi_{t}\\{{x:A}\\}.{B}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:A$}}}}\vbox{}}}\over\hbox{\hskip
36.37663pt\vbox{\vbox{}\hbox{\hskip-36.37663pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m\ n:B[n/x]$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
65.02312pt\vbox{\hbox{\hskip-65.02312pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:\Pi_{t}({x:A}).{B}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:A$}}}}\vbox{}}}\over\hbox{\hskip
36.37663pt\vbox{\vbox{}\hbox{\hskip-36.37663pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m\ n:B[n/x]$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
65.21364pt\vbox{\hbox{\hskip-65.21364pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
B:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{A}\simeq{B}$}}}}}\vbox{}}}\over\hbox{\hskip
19.40263pt\vbox{\vbox{}\hbox{\hskip-19.40263pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:B$}}}}}}$ Figure 5. Logical Terms

##  4\. Program Typing

The typing of programs is where our preparation at the logical level pays off.
Due to the sub-structural nature of program typing, we must first understand
the formation of program contexts and the constraints that can be imposed upon
them before we can progress further into the presentation.

###  4.1. Program Context

A program context $\Delta$ is a sequence of triples in the form
${x:_{s}A,y:_{r}B,\ldots}$ where each triple is comprised of a fresh variable,
a sort and a type. The well-formation of a program context $\Delta$ is defined
under a logical context $\Gamma$ as the judgment ${\Gamma;\Delta\vdash}$ whose
rules are formally presented in Figure 6. Basically, for a well-formed program
context according to ${\Gamma;\Delta\vdash}$, each entry ${x:_{s}A}$ in
$\Delta$ must be correspondingly well-sorted at the logical level as
${\Gamma\vdash A:s}$. We can already see here a major role of the logical
level: it provides the types that programs inhabit.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
9.65312pt\vbox{\vbox{}\hbox{\hskip-9.65312pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon;\epsilon\vdash$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
59.11882pt\vbox{\hbox{\hskip-59.11882pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash A:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\Gamma$}}}}}\vbox{}}}\over\hbox{\hskip
35.38754pt\vbox{\vbox{}\hbox{\hskip-35.38753pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A;\Delta,x:_{s}A\vdash$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
59.11882pt\vbox{\hbox{\hskip-59.11882pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash A:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\Gamma$}}}}}\vbox{}}}\over\hbox{\hskip
23.7594pt\vbox{\vbox{}\hbox{\hskip-23.7594pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A;\Delta\vdash$}}}}}}$
Figure 6. Program Context

We can see from the second and third rules in Figure 6 that given judgment
${\Gamma;\Delta\vdash}$, the program context $\Delta$ forms an annotated sub-
context of the logical context $\Gamma$. For the sake of readability, we
implicitly assume that ${x\notin\Delta}$ whenever the notation
${\Gamma,x:A;\Delta}$ is used.

###  4.2. Context Management

Careful context management lies at the heart of sub-structural type systems.
For this purpose, we introduce context merge ${\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}}$ and context constraint ${\Delta\triangleright s}$
whose rules are listed in Figure 7 and Figure 8 respectively.

Context merge ${\Delta_{1}\mathbin{\mathaccent 0{\cdot}\cup}\Delta_{2}}$ is a
partial function that applies the contraction rule to overlapping U sorted
triples in program contexts $\Delta_{1}$ and $\Delta_{2}$. For L sorted
triples, they must occur uniquely in either $\Delta_{1}$ or $\Delta_{2}$ but
never both. Whenever we write ${\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}}$ inside typing rules, we implicitly assert that
context merging is well-defined for $\Delta_{1}$ and $\Delta_{2}$.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
15.7297pt\vbox{\vbox{}\hbox{\hskip-15.72969pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon\mathbin{\mathaccent
0{\cdot}\cup}\epsilon=\epsilon$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
43.96695pt\vbox{\hbox{\hskip-43.96693pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}=\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\Delta$}}}}\vbox{}}}\over\hbox{\hskip
71.5307pt\vbox{\vbox{}\hbox{\hskip-71.53069pt\hbox{\hbox{$\displaystyle\displaystyle(\Delta_{1},x:_{\text{U}}A)\mathbin{\mathaccent
0{\cdot}\cup}(\Delta_{2},x:_{\text{U}}A)=(\Delta,x:_{\text{U}}A)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
43.96695pt\vbox{\hbox{\hskip-43.96693pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}=\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\Delta$}}}}\vbox{}}}\over\hbox{\hskip
53.81381pt\vbox{\vbox{}\hbox{\hskip-53.8138pt\hbox{\hbox{$\displaystyle\displaystyle(\Delta_{1},x:_{\text{L}}A)\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}=(\Delta,x:_{\text{L}}A)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
43.96695pt\vbox{\hbox{\hskip-43.96693pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}=\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
x\notin\Delta$}}}}\vbox{}}}\over\hbox{\hskip
55.06381pt\vbox{\vbox{}\hbox{\hskip-55.0638pt\hbox{\hbox{$\displaystyle\displaystyle\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}(\Delta_{2},x:_{\text{L}}A)=(\Delta,x:_{\text{L}}A)$}}}}}}$
Figure 7. Context Merge

For the sort indexed context constraint ${\Delta\triangleright s}$, if
${s=\text{U}}$ then all triples in $\Delta$ must be U annotated. In this
situation, we know from context well-formation that all types in $\Delta$ must
be non-linear. On the other hand, if ${s=\text{L}}$ then triples in $\Delta$
may be of both sorts. This parameterized behavior allows context constraints
appearing in typing rules to work for both linear and non-linear modalities.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
8.18594pt\vbox{\vbox{}\hbox{\hskip-8.18594pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon\triangleright
s$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
10.37503pt\vbox{\hbox{\hskip-10.37502pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright\text{U}$}}}\vbox{}}}\over\hbox{\hskip
22.71191pt\vbox{\vbox{}\hbox{\hskip-22.7119pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,x:_{\text{U}}A\triangleright\text{U}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
9.81253pt\vbox{\hbox{\hskip-9.81252pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright\text{L}$}}}\vbox{}}}\over\hbox{\hskip
21.44066pt\vbox{\vbox{}\hbox{\hskip-21.44066pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,x:_{s}A\triangleright\text{L}$}}}}}}$
Figure 8. Context Constraint

###  4.3. General Typing

At this point we are ready to begin the discussion on typing rules at the
program level properly. An immediate difference between the program level and
logical level is the lack of type formation rules at the program level. From
TLL’s perspective, types are hypothetical entities whose purpose is to mediate
program composition. All the type formation rules for deriving the types of
programs are defined at the logical level.

The first two rules at the program level are presented in Figure 9 concerning
variable typing and type conversion respectively. In the variable typing rule
we see that the program context $\Delta$ must contain the program variable
${x:_{s}A}$ of interest. Furthermore, the rest of the program context is
subject to constraint ${\Delta/\\{x:_{s}A\\}\triangleright\text{U}}$ which
inhibits weakening the context with variables of linear types. The conversion
rule states that a program of type $A$ can be viewed as a program of type $B$
provided that $A$ and $B$ are definitionally equal and $B$ is well-sorted at
the logical level.

$\displaystyle\displaystyle{\hbox{\hskip
76.69388pt\vbox{\hbox{\hskip-76.69388pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle x:_{s}A\in\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta/\\{x:_{s}A\\}\triangleright\text{U}$}}}}}\vbox{}}}\over\hbox{\hskip
23.5094pt\vbox{\vbox{}\hbox{\hskip-23.5094pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
x:A$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
70.96365pt\vbox{\hbox{\hskip-70.96364pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
B:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{A}\simeq{B}$}}}}}\vbox{}}}\over\hbox{\hskip
25.15265pt\vbox{\vbox{}\hbox{\hskip-25.15263pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:B$}}}}}}$ Figure 9. General Program Typing

###  4.4. Irrelevance Quantification

In Section 3.1 we introduced $\Pi{0}$-types and $\Pi{1}$-types. Figure 10
shows how $\lambda{0}$-programs inhabiting $\Pi{0}$-types are constructed
along with their corresponding application rule.

$\displaystyle\displaystyle{\hbox{\hskip
54.97456pt\vbox{\hbox{\hskip-54.97455pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A;\Delta\vdash
m:B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright
t$}}}}\vbox{}}}\over\hbox{\hskip
63.61647pt\vbox{\vbox{}\hbox{\hskip-63.61646pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\lambda_{t}\\{{x:A}\\}.{m}:\Pi_{t}\\{{x:A}\\}.{B}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
72.27315pt\vbox{\hbox{\hskip-72.27313pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:\Pi_{t}\\{{x:A}\\}.{B}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:A$}}}}\vbox{}}}\over\hbox{\hskip
42.12665pt\vbox{\vbox{}\hbox{\hskip-42.12663pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m\ n:B[n/x]$}}}}}}$ Figure 10. Irrelevance Quantification

Observe that in the premise of the $\lambda{0}$-program construction rule,
only the logical context is expanded with the parameter as ${\Gamma,x:A}$
whereas the program context $\Delta$ is left unchanged. The body of the
$\lambda{0}$-program $m$ does not have access to $x$ through the program
context, so according to the program variable rule $x$ cannot be typed
directly as a program in $m$. However, type annotations and irrelevant terms
require only the presence of the logical context which is why $x$ can still be
used irrelevantly in $m$. The side condition ${\Delta\triangleright t}$
ensures that if $\Delta$ contains linear variables, they cannot be trivially
duplicated by simply packing them into a non-linear $\lambda{0}$-program.

The application rule for $\lambda{0}$-programs presents an interesting
situation where its premise requires that $m$ be typed at the program level
and $n$ be typed at the logical level. If $m$ is a $\lambda{0}$-program, then
the parameter of $m$ can only be used irrelevantly inside its body. Due to the
fact that $n$ will always land in computationally irrelevant positions after
$\beta$-reduction, all of $n$ is considered to be irrelevant as well.

###  4.5. Relevance Quantification

The rules governing the creation and application of $\lambda{1}$-programs are
presented in Figure 11. They are similar to their irrelevance counterparts
with some subtle yet important differences.

In the premise of the introduction rule for $\lambda{1}$-programs, we see that
both the logical context and program context are expanded with the parameter
as ${\Gamma,x:A}$ and ${\Delta,x:_{s}A}$ respectively. This means that $m$ can
utilize $x$ both irrelevantly inside type annotations and also relevantly as a
sub-program. Furthermore, if $s=\text{L}$, the argument $x$ must be used
exactly once inside $m$ because linearly typed variables cannot be discarded
from the program context through weakening nor duplicated through contraction.
In the case that $s=\text{U}$, the argument $x$ may be used freely inside $m$
as the structural rules are admissible on variables with non-linear types.

Since the introduction rule establishes that the arguments of
$\lambda{1}$-programs can be used relevantly inside their bodies, the
application rule must account for linear resources used by the applied
argument. We can see this taking place here as the argument $n$ must be typed
at the program level with program context $\Delta_{2}$. Additionally, the
program context $\Delta_{1}$ of $m$ is merged together with $\Delta_{2}$ as
${\Delta_{1}\mathbin{\mathaccent 0{\cdot}\cup}\Delta_{2}}$ in the conclusion.

$\displaystyle\displaystyle{\hbox{\hskip
66.60269pt\vbox{\hbox{\hskip-66.60269pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A;\Delta,x:_{s}A\vdash
m:B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright
t$}}}}\vbox{}}}\over\hbox{\hskip
60.61644pt\vbox{\vbox{}\hbox{\hskip-60.61642pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\lambda_{t}({x:A}).{m}:\Pi_{t}({x:A}).{B}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
76.54314pt\vbox{\hbox{\hskip-76.54314pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{1}\vdash
m:\Pi_{t}({x:A}).{B}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{2}\vdash
n:A$}}}}\vbox{}}}\over\hbox{\hskip
51.39667pt\vbox{\vbox{}\hbox{\hskip-51.39665pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}\vdash m\ n:B[n/x]$}}}}}}$ Figure 11. Relevance
Quantification

Careful readers may have noticed the possibility for a seemingly unsound
situation to arise in the typing rule for applications. Suppose that $m$ is a
$\lambda{1}$-program whose domain is of non-linear type $A$. This means that
the parameter of $m$ can be used freely inside its body. If $n$ uses linear
resources in $\Delta_{2}$, then substituting $n$ into the body of $m$ could
result in the duplication or leakage of resources. Unlike some prior works on
linear dependent types which strictly forbid these applications from being
well-typed (Cervesato and Pfenning, 2002) or require multiple copies of
$\Delta_{2}$ (Atkey, 2018), we provide an alternative solution where
applications of this form are sound using a single copy of $\Delta_{2}$. By
leveraging the flexibility of TLL’s two-level design, we decouple the
operational semantics of the logical level from the program level and enforce
a call-by-value style evaluation order in the program level semantics. When
using call-by-value, $n$ must first be evaluated to a value of type $A$. This
eager evaluation strategy essentially consumes all of the necessary linear
resources once before $\beta$-reduction. The final value of type $A$ that
substitutes into $m$ is guaranteed by the value stability theorem (Theorem 11)
to be resource free which allows it to be used soundly within $m$.

##  5\. Program Extraction

In this section, we describe the type directed procedure for erasing type
annotations and irrelevant terms from TLL programs. During erasure, every term
to be erased is replaced with a special constant $\square$ with no typing
information nor computational behavior. We use the judgment
${\Gamma;\Delta\vdash m\sim m^{\prime}:A}$ to formally state that a program
$m$ of type $A$ is erased to the extracted program $m^{\prime}$.

The following example shows the erasure of a program to a much simpler
extracted form where all irrelevant terms are replaced with $\square$. Notice
that the entire argument applied to the $\lambda{0}$-program is erased in the
extracted program.

$\displaystyle(\lambda_{\text{L}}\\{{A:\text{U}}\\}.{\lambda_{\text{L}}({x:A}).{x}})\
(\Pi_{\text{U}}\\{{B:\text{L}}\\}.{\Pi_{\text{U}}({x:B}).{B}})\sim$
$\displaystyle(\lambda_{\text{L}}\\{{A:\square}\\}.{\lambda_{\text{L}}({x:\square}).{x}})\
\square$

###  5.1. General Extraction

The erasure judgment is defined in a similar fashion to program typing. We
begin by presenting the erasure rules for variables and type conversion in
Figure 12.

$\displaystyle\displaystyle{\hbox{\hskip
76.69388pt\vbox{\hbox{\hskip-76.69388pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle x:_{s}A\in\Delta$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta/\\{x:_{s}A\\}\triangleright\text{U}$}}}}}\vbox{}}}\over\hbox{\hskip
32.08128pt\vbox{\vbox{}\hbox{\hskip-32.08128pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
x\sim x:A$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
80.35771pt\vbox{\hbox{\hskip-80.3577pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m\sim m^{\prime}:A$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash B:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle{A}\simeq{B}$}}}}}\vbox{}}}\over\hbox{\hskip
34.5467pt\vbox{\vbox{}\hbox{\hskip-34.54669pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m\sim m^{\prime}:B$}}}}}}$ Figure 12. General Erasure

Program variables are considered atomic by erasure in the sense that they do
not contain irrelevant sub-terms. So erasure is an identity operation when
applied to program variables. The type conversion erasure rule states that if
a program $m$ of type $A$ can be extracted to $m^{\prime}$ and $A$ is
definitionally equal to some well-sorted type $B$, then $m$ can be viewed as a
program of type $B$ and still be extracted to $m^{\prime}$.

###  5.2. Irrelevance Erasure

The rules for performing erasure on $\lambda{0}$-programs and their
applications are presented in Figure 13, both of which mimic their program
typing counterparts.

$\displaystyle\displaystyle{\hbox{\hskip
64.36862pt\vbox{\hbox{\hskip-64.3686pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A;\Delta\vdash
m\sim m^{\prime}:B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright
t$}}}}\vbox{}}}\over\hbox{\hskip
92.61743pt\vbox{\vbox{}\hbox{\hskip-92.61743pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\lambda_{t}\\{{x:A}\\}.{m}\sim\lambda_{t}\\{{x:\square}\\}.{m^{\prime}}:\Pi_{t}\\{{x:A}\\}.{B}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
81.6672pt\vbox{\hbox{\hskip-81.66719pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m\sim m^{\prime}:\Pi_{t}\\{{x:A}\\}.{B}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:A$}}}}\vbox{}}}\over\hbox{\hskip
58.5207pt\vbox{\vbox{}\hbox{\hskip-58.5207pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m\ n\sim m^{\prime}\ \square:B[n/x]$}}}}}}$ Figure 13. Irrelevance Erasure

###  5.3. Relevance Erasure

Erasure for $\lambda{1}$-programs and their applications can be carried out in
an inductive manner as depicted in Figure 14. Both of these rules are
straightforward as they simply push the erasure procedure structurally into
their sub-programs.

$\displaystyle\displaystyle{\hbox{\hskip
75.99675pt\vbox{\hbox{\hskip-75.99675pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A;\Delta,x:_{s}A\vdash
m\sim m^{\prime}:B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright
t$}}}}\vbox{}}}\over\hbox{\hskip
88.11739pt\vbox{\vbox{}\hbox{\hskip-88.11739pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\lambda_{t}({x:A}).{m}\sim\lambda_{t}({x:\square}).{m^{\prime}}:\Pi_{t}({x:A}).{B}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
94.08125pt\vbox{\hbox{\hskip-94.08125pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{1}\vdash
m\sim m^{\prime}:\Pi_{t}({x:A}).{B}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{2}\vdash n\sim
n^{\prime}:A$}}}}\vbox{}}}\over\hbox{\hskip
66.43477pt\vbox{\vbox{}\hbox{\hskip-66.43477pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}\vdash m\ n\sim m^{\prime}\ n^{\prime}:B[n/x]$}}}}}}$
Figure 14. Relevance Erasure

##  6\. Operational Semantics

The exposition up until this point has been solely concerned with the static
aspects of TLL such as typing and erasure. We now turn our focus to TLL’s
dynamic behavior by endowing it with two separate operational semantics: one
for the logical level and the other for the program level. We use the relation
${m\leadsto n}$ for logical reductions and the relation
${m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n}$ for program
reductions.

###  6.1. Logical Reductions

The reductions carried out by terms in the logical level are entirely
standard. Figure 15 presents an excerpt of the logical reduction rules where
many of the uninteresting structural cases have been elided. Unlike the
reductions at the program level which are carried out using a call-by-value
style evaluation order, the reductions at the logical level are not restricted
to any particular evaluation order. The confluence theorem (Theorem 1) for
logic level reductions ensures that for any arbitrary term, every reduction
strategy can ultimately be joined at a common term. Coupled with the fact that
logical reductions are strongly normalizing (Theorem 7) for well-typed logical
terms, one can check the definitional equality of two terms by comparing their
normal forms.

$\displaystyle\displaystyle{\hbox{\hskip
15.59512pt\vbox{\hbox{\hskip-15.59511pt\hbox{\hbox{$\displaystyle\displaystyle
m\leadsto m^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
25.49724pt\vbox{\vbox{}\hbox{\hskip-25.49722pt\hbox{\hbox{$\displaystyle\displaystyle
m\ n\leadsto m^{\prime}\ n$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
13.09512pt\vbox{\hbox{\hskip-13.09511pt\hbox{\hbox{$\displaystyle\displaystyle
n\leadsto n^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
25.49724pt\vbox{\vbox{}\hbox{\hskip-25.49722pt\hbox{\hbox{$\displaystyle\displaystyle
m\ n\leadsto m\ n^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
54.85803pt\vbox{\vbox{}\hbox{\hskip-54.85803pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda_{t}\\{{x:A}\\}.{m})\
n\leadsto m[n/x]$}}}}}}$ $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
53.35802pt\vbox{\vbox{}\hbox{\hskip-53.35802pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda_{t}({x:A}).{m})\
n\leadsto m[n/x]$}}}}}}$ Figure 15. Logical Reductions (Excerpt)

###  6.2. Program Reductions

As we have mentioned previously, the program level operational semantics
utilizes a call-by-value style evaluation order. Figure 16 lists the various
value forms. We consider program variables to be values in order to allow user
assumed constants to be passed around.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
14.19537pt\vbox{\vbox{}\hbox{\hskip-14.19536pt\hbox{\hbox{$\displaystyle\displaystyle
x~{}\textit{value}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
35.05646pt\vbox{\vbox{}\hbox{\hskip-35.05646pt\hbox{\hbox{$\displaystyle\displaystyle\lambda_{t}\\{{x:A}\\}.{m}~{}\textit{value}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
33.55644pt\vbox{\vbox{}\hbox{\hskip-33.55644pt\hbox{\hbox{$\displaystyle\displaystyle\lambda_{t}({x:A}).{m}~{}\textit{value}$}}}}}}$
Figure 16. Program Values

The reduction rules at the program level are given in Figure 17. Due to the
fact that types and irrelevant terms are computationally inert, there are
significantly fewer reduction rules at the program level than at the logical
level. Among the reductions here are the $\beta_{0}$-reduction for
$\lambda{0}$-programs and $\beta_{1}$-reduction for $\lambda{1}$-programs.

From the program level typing rules we know that arguments applied to
$\lambda{0}$-programs must be irrelevant terms. So due to its purely
hypothetical nature, the irrelevant argument $n$ here will never consume
actual resources. This claim is reinforced by the fact that after erasure, $n$
will be $\square$, which is completely devoid of operational behavior. Thus it
is sound for the $\beta_{0}$-reduction to immediately substitute $n$ into $m$
without evaluation.

$\displaystyle\displaystyle{\hbox{\hskip
25.30328pt\vbox{\hbox{\hskip-25.30327pt\hbox{\hbox{$\displaystyle\displaystyle
m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}m^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
35.2054pt\vbox{\vbox{}\hbox{\hskip-35.20538pt\hbox{\hbox{$\displaystyle\displaystyle
m\ n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}m^{\prime}\
n$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
22.80328pt\vbox{\hbox{\hskip-22.80327pt\hbox{\hbox{$\displaystyle\displaystyle
n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
35.2054pt\vbox{\vbox{}\hbox{\hskip-35.20538pt\hbox{\hbox{$\displaystyle\displaystyle
m\ n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}m\
n^{\prime}$}}}}}}$ $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
64.5662pt\vbox{\vbox{}\hbox{\hskip-64.5662pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda_{t}\\{{x:A}\\}.{m})\
n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}m[n/x]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
13.9662pt\vbox{\hbox{\hskip-13.96619pt\hbox{\hbox{$\displaystyle\displaystyle
v~{}\textit{value}$}}}\vbox{}}}\over\hbox{\hskip
62.34947pt\vbox{\vbox{}\hbox{\hskip-62.34947pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda_{t}({x:A}).{m})\
v\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}m[v/x]$}}}}}}$
Figure 17. Program Reductions

In Section 4.5 we have explained that the call-by-value style operational
semantics at the program level allows us to assume tight resource bounds when
defining the typing rules for $\lambda{1}$-program application. This statement
is realized by the $\beta_{1}$-reduction rule which requires the applied
argument $v$ to be a value. Now that $v$ is a value, the resources contained
within $v$ are upper bound by the value stability theorem (Theorem 11). So it
is sound for the $\beta_{1}$-reduction to substitute $v$ into $m$.

##  7\. Meta Theory

In this section we study the meta-theoretic properties of TLL. We organize the
presentation into three subsections which are concerned with logical level
theories, program level theories and program extraction theories respectively.

###  7.1. Logical Theories

The first theorem of the logical level is that of confluence. As described in
Section 6.1, logical reductions do not have a fixed evaluation order so
confluence is necessary to join together different reduction paths. This is
especially important from an implementation perspective where definitional
equality is checked by reducing terms to their normal forms. If confluence is
not admissible, then certain reduction strategies may lead to a loss of valid
definitional equalities. To prove the confluence theorem, we use the standard
technique of showing the diamond property for parallelized logical reductions.

###### Theorem 1 (Confluence of Logical Reductions).

If ${m\leadsto^{*}m_{1}}$ and ${m\leadsto^{*}m_{2}}$, then there exists $n$
such that ${m_{1}\leadsto^{*}n}$ and ${m_{2}\leadsto^{*}n}$.

At the logical level, types are terms inhabiting sorts. The type validity
theorem shows that the types of terms are indeed valid types according to this
definition. Besides substantiating the design of TLL as a dependent type
system, the type validity theorem also provides a great deal of utility when
proving other theorems as it allows types to be viewed as terms. This enables
various inversion lemmas to be applicable to types.

###### Theorem 2 (Type Validity).

For any logical typing ${\Gamma\vdash m:A}$, there exists sort $s$ such that
${\Gamma\vdash A:s}$ is derivable.

The sort of a TLL type determines its modality. A type inhabiting the L sort
is linear and a type inhabiting the U sort is non-linear. With the sorts of
types playing such a crucial role in the sub-structural type system at the
program level, it is important to show that no ambiguity arises when assigning
sorts to types at the logical level. The sort uniqueness theorem states that
the sort of a particular type is unique thus preventing contradictory
situations where a type is both L sorted and U sorted. When viewed in
conjunction with type validity, these theorems show that there always exists a
unique sort for the type of a term to inhabit.

###### Theorem 3 (Sort Uniqueness).

If there are logical typings ${\Gamma\vdash A:s}$ and ${\Gamma\vdash A:t}$,
then $s=t$.

The standard subject reduction theorem is admissible for well-typed logical
terms. This means that the types of logical terms are preserved by reductions.
Properties and theorems that are derived from the logical typing judgment can
be propagated across reductions as well. Furthermore, subject reduction also
ensures that a reduction based definitional equality checker never alters the
types of its candidates.

###### Theorem 4 (Logical Subject Reduction).

If there are logical typing ${\Gamma\vdash m:A}$ and reduction ${m\leadsto
n}$, then ${\Gamma\vdash n:A}$ is derivable.

Finally, we have the strong normalization theorem at the logical level.
Assuming that sorts are always implicitly labeled with universe levels in the
usual way (i.e., $s_{l}:\text{U}_{l+1}$), then universe inconsistencies can be
ruled out by the type system. At this point, the logical level of TLL can be
modeled in Martin-Löf type theory (MLTT) (Martin-Löf, 1975) in a
straightforward manner that preserves its reduction behavior. The rules for
carrying out the modeling procedure are given formally in Figure 18.
Basically, an MLTT model of logical TLL collapses the two sorts into one and
inductively strips terms of their modality and relevancy annotations.

$\displaystyle\llbracket{x}\rrbracket$ $\displaystyle=x$
$\displaystyle\llbracket{\text{U}}\rrbracket$ $\displaystyle=\text{Type}$
$\displaystyle\llbracket{\text{L}}\rrbracket$ $\displaystyle=\text{Type}$
$\displaystyle\llbracket{\Pi_{t}\\{{x:A}\\}.{B}}\rrbracket$
$\displaystyle=\Pi(x:\llbracket{A}\rrbracket).\llbracket{B}\rrbracket$
$\displaystyle\llbracket{\Pi_{t}({x:A}).{B}}\rrbracket$
$\displaystyle=\Pi(x:\llbracket{A}\rrbracket).\llbracket{B}\rrbracket$
$\displaystyle\llbracket{\lambda_{t}\\{{x:A}\\}.{B}}\rrbracket$
$\displaystyle=\lambda(x:\llbracket{A}\rrbracket).\llbracket{B}\rrbracket$
$\displaystyle\llbracket{\lambda_{t}({x:A}).{B}}\rrbracket$
$\displaystyle=\lambda(x:\llbracket{A}\rrbracket).\llbracket{B}\rrbracket$
$\displaystyle\llbracket{m\ n}\rrbracket$
$\displaystyle=\llbracket{m}\rrbracket\ \llbracket{n}\rrbracket$ Figure 18.
Logical TLL in Martin-Löf

After naturally extending the modeling procedure to all types appearing in TLL
logical contexts, the following two lemmas can be proven. These results show
that this model is indeed sound with regards to logical reduction. By virtue
of the strong normalization property for MLTT (Coquand and Spiwack, 2006), TLL
must be strongly normalizing as well.

###### Lemma 0 (Logical Type Model).

Given a TLL logical typing judgment ${\Gamma\vdash_{\text{TLL}}m:A}$, the
judgment
${\llbracket{\Gamma}\rrbracket\vdash_{\text{MLTT}}\llbracket{m}\rrbracket:\llbracket{A}\rrbracket}$
can be derived in Martin-Löf type theory.

###### Lemma 0 (Logical Reduction Model).

Given a TLL logical reduction ${m\leadsto_{\text{TLL}}n}$, the reduction
${\llbracket{m}\rrbracket\leadsto_{\text{MLTT}}\llbracket{n}\rrbracket}$ can
be derived in Martin-Löf type theory.

###### Theorem 7 (Logical Strong Normalization).

For any TLL term $m$ with logical typing ${\Gamma\vdash m:A}$, it is strongly
normalizing.

###  7.2. Program Theories

TLL prohibits weakening the program context with variables of linear types to
prevent the discarding of resources. However, the logical context can be
independently weakened by itself since hypothetical resources can always be
assumed freely. Moreover, weakening is admissible for the program context if
the weakened variable is of non-linear type. These observations are expressed
formally in the following pair of weakening lemmas.

###### Lemma 0 (Program 0-Weakening).

For valid program typing ${\Gamma;\Delta\vdash m:A}$ and logical typing
${\Gamma\vdash B:s}$, the judgment ${\Gamma,x:B;\Delta\vdash m:A}$ is
derivable for any $x\notin\Gamma$.

###### Lemma 0 (Program 1-Weakening).

For valid program typing ${\Gamma;\Delta\vdash m:A}$ and logical typing
${\Gamma\vdash B:\text{U}}$, the judgment
${\Gamma,x:B;\Delta,x:_{\text{U}}B\vdash m:A}$ is derivable for any
$x\notin\Gamma$.

A common drawback of stratified type systems is the lack of code sharing
between language fragments. Structures performing similar tasks must be
implemented independently in the different layers of the language. Libraries
with large amounts of redundant code can become difficult to scale and
maintain so it is important to reduce code duplication to the best of our
abilities. The program reflection theorem tackles the code redundancy problem
by allowing us to freely reflect well-typed programs into the logical level.
This essentially allows the sharing of all code written in the program level
with the logical level.

###### Theorem 10 (Program Reflection).

For any program typing ${\Gamma;\Delta\vdash m:A}$, logical typing
${\Gamma\vdash m:A}$ is derivable.

Arbitrary TLL programs may utilize linear resources to compute a final non-
linear value. So despite these programs being of non-linear types, they cannot
be freely duplicated without breaking the no-contraction principle. However
for programs in value form, the value stability theorem gives an upper bound
on the resources they are allowed to consume. For a linearly typed value, it
will always be used exactly once and consequently any resource held by the
value is used exactly once as well. For values of non-linear type, the context
constraint ${\Delta\triangleright\text{U}}$ prevents resources from occurring
inside the value which allows it to be duplicated soundly.

###### Theorem 11 (Value Stability).

If there is value $v$ with program typing ${\Gamma;\Delta\vdash v:A}$ and
${\Gamma\vdash A:s}$, then ${\Delta\triangleright s}$.

The program level supports its own version of the subject reduction theorem
that is defined on the program typing judgment and program reductions.
Although there are less typing rules at the program level when compared to the
logical level, the program subject reduction is more difficult to prove than
its logical counterpart. This is due to the necessity of carefully tracking
changes in the program context during variable substitution. The two following
lemmas describe the interactions between substitution and contexts.

###### Lemma 0 (Program 0-Substitution).

If there are program typing ${\Gamma,x:A;\Delta\vdash m:B}$ and logical typing
${\Gamma\vdash n:A}$, then ${\Gamma;\Delta\vdash m[n/x]:B[n/x]}$ is derivable.

###### Lemma 0 (Program 1-Substitution).

If there are program typings ${\Gamma,x:A;\Delta_{1},x:_{s}A\vdash m:B}$ and
${\Gamma;\Delta_{2}\vdash n:A}$ and context constraint
${\Delta_{2}\triangleright s}$, then ${\Gamma;\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}\vdash m[n/x]:B[n/x]}$ is derivable.

###### Theorem 14 (Program Subject Reduction).

For any program typing ${\epsilon;\epsilon\vdash m:A}$ and reduction
${m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n}$, there is
${\epsilon;\epsilon\vdash n:A}$.

To show that well-typed programs “cannot go wrong”, we prove the following
progress theorem. When viewed together with the program subject reduction
theorem, it is clear that closed TLL programs will not get stuck during
evaluation.

###### Theorem 15 (Program Progress).

If there is program typing ${\epsilon;\epsilon\vdash m:A}$, then $m$ is either
a value or there exists $n$ such that
${m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n}$.

###  7.3. Program Extraction

Introduced in Section 5, the program erasure procedure is carried out by
inductively erasing type annotations and irrelevant terms occurring inside
programs. The erasure existence theorem shows that extraction is well-defined
for all well-typed TLL programs.

###### Theorem 16 (Erasure Existence).

For any well typed program ${\Gamma;\Delta\vdash m:A}$, there exists an
extracted version of it $m^{\prime}$ such that the erasure relation
${\Gamma;\Delta\vdash m\sim m^{\prime}:A}$ is derivable.

After erasure has been successfully carried out on well-type programs, the
extracted results retain only the relevant parts of the original program. It
is now important to show that these extracted programs still behave as
expected of their original selves computationally. We accomplish this by
proving instrumented subject reduction and progress theorems.

The first theorem to establish the connection between original programs and
their extracted forms is the erasure subject reduction theorem. Erasure
subject reduction tells us that if a program reduction
${m^{\prime}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n^{\prime}}$ can be
triggered for the extracted $m^{\prime}$ of a well-typed program $m$, then
there exists a well-type program $n$ that extracts to $n^{\prime}$ and the
reduction ${m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n}$ exists on the
original forms.

###### Theorem 17 (Erasure Subject Reduction).

For any erasure relation ${\epsilon;\epsilon\vdash m\sim m^{\prime}:A}$ and
reduction
${m^{\prime}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n^{\prime}}$, there
exists program $n$ such that the following diagram commutes.

${{\epsilon;\epsilon}}$${m}$${{m^{\prime}}}$${A}$${{\epsilon;\epsilon}}$${n}$${{n^{\prime}}}$${A}$$\scriptstyle{\sim}$$\scriptstyle{\vdash}$$\scriptstyle{:}$${\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$${\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}}$$\scriptstyle{\vdash}$$\scriptstyle{:}$$\scriptstyle{\sim}$

Through the erasure progress theorem we show that the extracted forms of well-
typed programs exhibit the same property of never getting stuck during
evaluation.

###### Theorem 18 (Erasure Progress).

If there is erasure relation ${\epsilon;\epsilon\vdash m\sim m^{\prime}:A}$,
then $m^{\prime}$ is a value or there exists $n^{\prime}$ such that
$m^{\prime}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n^{\prime}$.

##  8\. Heap Semantics

In order to realize the abstract notion of linear resource, we develop a heap
semantics in the style of Turner and Wadler (Turner and Wadler, 1999) where
heap memory serves as resource to the language runtime. At the heart of the
semantics is the following heap indexed reduction relation.

$\displaystyle
H_{1};m_{1}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H_{2};m_{2}$

The term $m_{1}$ here is an extracted program that may contain pointers to
cells in heap $H_{1}$ storing values. As $m_{1}$ evaluates, new cells in the
heap are allocated to store intermediate values that are generated. The
effects of a single evaluation step are reflected in the updated heap $H_{2}$
and program $m_{2}$. If evaluating $m_{1}$ requires dereferencing pointers,
then depending on the modality of the pointed to cell, the heap is either
unchanged for non-linear cells or deallocated for linear cells. Such a
semantics closely models low level implementations of functional languages
where heap memory is dynamically allocated to store closures and other various
data structures. Through this heap semantics we show that linearity enforces
safe memory usage and that linearly typed programs are guaranteed to run
memory clean without the need for runtime garbage collection.

###  8.1. Heaps

Heaps $H$ are maps from unique locations $l$ to sort annotated values.
Generally, a heap is of the following form:

$\displaystyle
H::=\\{l_{1}\mapsto_{s_{1}}v_{1},l_{2}\mapsto_{s_{2}}v_{2},\ldots,l_{k}\mapsto_{s_{k}}v_{k}\\}$

Each entry ${l_{i}\mapsto_{s_{i}}v_{i}}$ denotes a mapping from location
$l_{i}$ to value $v_{i}$ of $s_{i}$ modality. In particular, if
$s_{i}=\text{U}$ then looking up location $l_{i}$ in the heap will not cause
any changes. However, if $s_{i}=\text{L}$ then looking up location $l_{i}$ in
the heap will remove the mapping from the heap. Formally, we introduce the
relation $\textit{lookup}({H_{1}},{l},{v},{H_{2}})$ with rules presented in
Figure 19, stating that looking up location $l$ in heap $H_{1}$ results in
value $v$ and heap $H_{2}$. Depending on the mapping modality between $l$ and
$m$, the resulting heap $H_{2}$ after lookup is equal to either $H_{1}$ in the
U case or $H_{1}/\\{l\mapsto_{\text{L}}v\\}$ in the L case.

$\displaystyle\displaystyle{\hbox{\hskip
20.02022pt\vbox{\hbox{\hskip-20.0202pt\hbox{\hbox{$\displaystyle\displaystyle(l\mapsto_{\text{U}}v)\in
H$}}}\vbox{}}}\over\hbox{\hskip
32.48648pt\vbox{\vbox{}\hbox{\hskip-32.48648pt\hbox{\hbox{$\displaystyle\displaystyle\textit{lookup}({H},{l},{v},{H})$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
19.70522pt\vbox{\hbox{\hskip-19.7052pt\hbox{\hbox{$\displaystyle\displaystyle(l\mapsto_{\text{L}}v)\in
H$}}}\vbox{}}}\over\hbox{\hskip
47.08546pt\vbox{\vbox{}\hbox{\hskip-47.08546pt\hbox{\hbox{$\displaystyle\displaystyle\textit{lookup}({H},{l},{v},{H/\\{l\mapsto_{\text{L}}v\\}})$}}}}}}$
Figure 19. Heap Lookup

Notice that the entries ${l\mapsto_{s}v}$ of heaps are similar to the triples
${x:_{s}A}$ of program contexts. While one maps locations to values, the other
maps variables to types. Both kinds of mappings are annotated by sort $s$.
Taking advantage of these commonalities, we overload the merge operator
${H_{1}\mathbin{\mathaccent 0{\cdot}\cup}H_{2}}$ and constraint
${H\triangleright s}$ to work for heaps as well. So instead of operating over
variables in contexts, they operate over locations in heaps.

###  8.2. Heap Reductions

The rules of heap reductions are presented in Figure 20. These rules
essentially form a modified version of the program level call-by-value
semantics. When a program is evaluated to value $v$, a memory cell at a fresh
location $l$ in the heap is allocated to store $v$. For example, since
$\lambda$-programs are considered values, a fresh cell with the same modality
as the $\lambda$-program is allocated to store it. Now if a pointer expression
${*l}$ is encountered, we know that it points to a value located in the heap.
The application rules utilize this fact to enforce the call-by-value
evaluation order for relevant applications.

$\displaystyle\displaystyle{\hbox{\hskip
11.41249pt\vbox{\hbox{\hskip-11.41249pt\hbox{\hbox{$\displaystyle\displaystyle
l\notin H$}}}\vbox{}}}\over\hbox{\hskip
92.55913pt\vbox{\vbox{}\hbox{\hskip-92.55913pt\hbox{\hbox{$\displaystyle\displaystyle
H;\lambda_{t}\\{{x:\square}\\}.{m}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H\cup\\{l\mapsto_{t}\lambda_{t}\\{{x:\square}\\}.{m}\\};{*l}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
11.41249pt\vbox{\hbox{\hskip-11.41249pt\hbox{\hbox{$\displaystyle\displaystyle
l\notin H$}}}\vbox{}}}\over\hbox{\hskip
89.5591pt\vbox{\vbox{}\hbox{\hskip-89.5591pt\hbox{\hbox{$\displaystyle\displaystyle
H;\lambda_{t}({x:\square}).{m}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox