11institutetext: Graduate School of Informatics, Kyoto University, Kyoto,
Japan
11email<EMAIL_ADDRESS>
11email<EMAIL_ADDRESS>
# A Dependently Typed Multi-Stage Calculus

Akira Kawata 11 Atsushi Igarashi 11 0000-0002-5143-9764

###### Abstract

We study a dependently typed extension of a multi-stage programming language à
la MetaOCaml, which supports quasi-quotation and cross-stage persistence for
manipulation of code fragments as first-class values and an evaluation
construct for execution of programs dynamically generated by this code
manipulation. Dependent types are expected to bring to multi-stage programming
enforcement of strong invariant—beyond simple type safety—on the behavior of
dynamically generated code. An extension is, however, not trivial because such
a type system would have to take stages of types—roughly speaking, the number
of surrounding quotations—into account.

To rigorously study properties of such an extension, we develop
$\lambda^{\textrm{MD}}$, which is an extension of Hanada and Igarashi’s typed
calculus $\lambda^{\triangleright\%}$ with dependent types, and prove its
properties including preservation, confluence, strong normalization for full
reduction, and progress for staged reduction. Motivated by code generators
that generate code whose type depends on a value from outside of the
quotations, we argue the significance of cross-stage persistence in
dependently typed multi-stage programming and certain type equivalences that
are not directly derived from reduction rules.

###### Keywords:

multi-stage programming, cross-stage persistence, dependent types

##  1 Introduction

###  1.1 Multi-stage Programming and MetaOCaml

Multi-stage programming makes it easier for programmers to implement
generation and execution of code at run time by providing language constructs
for composing and running pieces of code as first-class values. A promising
application of multi-stage programming is (run-time) code specialization,
which generates program code specialized to partial inputs to the program and
such applications are studied in the literature [17, 20, 29].

MetaOCaml [6, 18] is an extension of OCaml111http://ocaml.org with special
constructs for multi-stage programming, including brackets and escape, which
are (hygienic) quasi-quotation, and run, which is similar to eval in Lisp, and
cross-stage persistence (CSP) [31]. Programmers can easily write code
generators by using these features. Moreover, MetaOCaml is equipped with a
powerful type system for safe code generation and execution. The notion of
code types is introduced to prevent code values that represent ill-typed
expressions from being generated. For example, a quotation of expression 1 + 1
is given type int code and a code-generating function, which takes a code
value $c$ as an argument and returns $c\texttt{ + }c$, is given type int code
-> int code so that it cannot be applied to, say, a quotation of "Hello",
which is given type string code. Ensuring safety for `run` is more challenging
because code types by themselves do not guarantee that the execution of code
values never results in unbound variable errors. Taha and Nielsen [30]
introduced the notion of environment classifiers to address the problem,
developed a type system to ensure not only type-safe composition but also
type-safe execution of code values, and proved a type soundness theorem (for a
formal calculus $\lambda^{\alpha}$ modeling a pure subset of MetaOCaml).

However, the type system, which is based on the Hindley–Milner polymorphism
[23], is not strong enough to guarantee invariant beyond simple types. For
example, Kiselyov [17] demonstrates specialization of vector/matrix
computation with respect to the sizes of vectors and matrices in MetaOCaml but
the type system of MetaOCaml cannot prevent such specialized functions from
being applied to vectors and matrices of different sizes.

###  1.2 Multi-stage Programming with Dependent Types

One natural idea to address this problem is the introduction of dependent
types to express the size of data structures in static types [34]. For
example, we could declare vector types indexed by the size of vectors as
follows.

        Vector :: Int -> *

`Vector` is a type constructor that takes an integer (which represents the
length of vectors): for example, `Vector 3` is the type for vectors whose
lengths are 3. Then, our hope is to specialize vector/matrix functions with
respect to their size and get a piece of function code, whose type respects
the given size, _provided at specialization time_. For example, we would like
to specialize a function to add two vectors with respect to the size of
vectors, that is, to implement a code generator that takes a (nonnegative)
integer $n$ as an input and generates a piece of function code of type
`(Vector `$n$` -> Vector `$n$` -> Vector `$n$`) code`.

###  1.3 Our Work

In this paper, we develop a new multi-stage calculus $\lambda^{\textrm{MD}}$
by extending the existing multi-stage calculus $\lambda^{\triangleright\%}$
[14] with dependent types and study its properties. We base our work on
$\lambda^{\triangleright\%}$, in which the four multi-stage constructs are
handled slightly differently from MetaOCaml, because its type system and
semantics are arguably simpler than $\lambda^{\alpha}$ [30], which formalizes
the design of MetaOCaml more faithfully. Dependent types are based on
$\lambda\textrm{LF}$ [1], which has one of the simplest forms of dependent
types. Our technical contributions are summarized as follows:

  * •

We give a formal definition of $\lambda^{\textrm{MD}}$ with its syntax, type
system and two kinds of reduction: full reduction, allowing reduction of any
redex, including one under $\lambda$-abstraction and quotation, and staged
reduction, a small-step call-by-value operational semantics that is closer to
the intended multi-stage implementation.

  * •

We show preservation, strong normalization, and confluence for full reduction;
and show unique decomposition (and progress as its corollary) for staged
reduction.

The combination of multi-stage programming and dependent types has been
discussed by Pasalic, Taha, and Sheard [26] and Brady and Hammond [5] but, to
our knowledge, our work is a first formal calculus of full-spectrum
dependently typed multi-stage programming with all the key constructs
mentioned above.

####  1.3.1 Organization of the Paper.

The organization of this paper is as follows. Section 2 gives an informal
overview of $\lambda^{\textrm{MD}}$. Section 3 defines $\lambda^{\textrm{MD}}$
and Section 4 shows properties of $\lambda^{\textrm{MD}}$. Section 5 discusses
related work and Section 6 concludes the paper with discussion of future work.
For reference, we give the full definition of $\lambda^{\textrm{MD}}$ and
proofs of properties in the Appendix.

##  2 Informal Overview of $\lambda^{\textrm{MD}}$

We describe our calculus $\lambda^{\textrm{MD}}$ informally.
$\lambda^{\textrm{MD}}$ is based on $\lambda^{\triangleright\%}$ [14] by
Hanada and Igarashi and so we start with a review of
$\lambda^{\triangleright\%}$.

###  2.1 $\lambda^{\triangleright\%}$

In $\lambda^{\triangleright\%}$, brackets (quasi-quotation) and escape
(unquote) are written ${\mathop{\blacktriangleright}}_{\alpha}M$ and
${\mathop{\blacktriangleleft}}_{\alpha}M$, respectively. For example,
${\mathop{\blacktriangleright}}_{\alpha}(1+1)$ represents code of expression
$1+1$ and thus evaluates to itself. Escape
${\mathop{\blacktriangleleft}}_{\alpha}M$ may appear under
${\mathop{\blacktriangleright}}_{\alpha}$; it evaluates $M$ to a code value
and splices it into the surrounding code fragment. Such splicing is expressed
by the following reduction rule:

$\displaystyle{\mathop{\blacktriangleleft}}_{\alpha}({\mathop{\blacktriangleright}}_{\alpha}M)\longrightarrow
M.$

The subscript $\alpha$ in ${\mathop{\blacktriangleright}}_{\alpha}$ and
${\mathop{\blacktriangleleft}}_{\alpha}$ is a stage variable222In Hanada and
Igarashi [14], it was called a transition variable, which is derived from
correspondence to modal logic, studied by Tsukada and Igarashi [32]. and a
sequence of stage variables is called a stage. Intuitively, a stage represents
the depth of nested brackets. Stage variables can be abstracted by
$\Lambda\alpha.M$ and instantiated by an application $M\ A$ to stages. For
example, $\Lambda\alpha.{\mathop{\blacktriangleright}}_{\alpha}((\lambda
x:\textrm{Int}.x+10)\ 5)$ is a code value, where $\alpha$ is abstracted. If it
is applied to $A=\alpha_{1}\cdots\alpha_{n}$,
${\mathop{\blacktriangleright}}_{\alpha}$ becomes
${\mathop{\blacktriangleright}}_{\alpha_{1}}\cdots{\mathop{\blacktriangleright}}_{\alpha_{n}}$;
in particular, if $n=0$, ${\mathop{\blacktriangleright}}_{\alpha}$ disappears.
So, an application of
$\Lambda\alpha.{\mathop{\blacktriangleright}}_{\alpha}((\lambda
x:\textrm{Int}.x+10)\ 5)$ to the empty sequence $\varepsilon$ reduces to
(unquoted) $(\lambda x:\textrm{Int}.x+10)\ 5$ and to 15. In other words,
application of a $\Lambda$-abstraction to $\varepsilon$ corresponds to run.
This is expressed by the following reduction rule:

$\displaystyle(\Lambda\alpha.M)\ A\longrightarrow M[\alpha\mapsto A]$

where stage substitution $[\alpha\mapsto A]$ manipulates the nesting of
${\mathop{\blacktriangleright}}_{\alpha}$ and
${\mathop{\blacktriangleleft}}_{\alpha}$ (and also $\%_{\alpha}$ as we see
later).

Cross-stage persistence (CSP), which is an important feature of
$\lambda^{\triangleright\%}$, is a primitive to embed values (not necessarily
code values) into a code value. For example, a
$\lambda^{\triangleright\%}$-term

$M_{1}=\lambda
x:\textrm{Int}.\Lambda\alpha.({\mathop{\blacktriangleright}}_{\alpha}((\%_{\alpha}x)*2))$

takes an integer $x$ as an input and returns a code value, into which $x$ is
embedded. If $M_{1}$ is applied to $38+4$ as in

$M_{2}=(\lambda
x:\textrm{Int}.\Lambda\alpha.({\mathop{\blacktriangleright}}_{\alpha}((\%_{\alpha}x)*2)))\
(38+4),$

then it evaluates to
$M_{3}=\Lambda\alpha.({\mathop{\blacktriangleright}}_{\alpha}((\%_{\alpha}42)*2))$.
According to the semantics of $\lambda^{\triangleright\%}$, the subterm
$\%_{\alpha}42$ means that it waits for the surrounding code to be run (by an
application to $\varepsilon$) and so it does not reduce further. If $M_{3}$ is
run by application to $\varepsilon$, substitution of $\varepsilon$ for
$\alpha$ eliminates ${\mathop{\blacktriangleright}}_{\alpha}$ and
$\%_{\alpha}$ and so $42*2$, which reduces to 84, is obtained. CSP is
practically important because one can call library functions from inside
quotations.

The type system of $\lambda^{\triangleright\%}$ uses code types—the type of
code of type $\tau$ is written ${\mathop{\triangleright}}_{\alpha}\tau$—for
typing ${\mathop{\blacktriangleright}}_{\alpha}$,
${\mathop{\blacktriangleleft}}_{\alpha}$ and $\%_{\alpha}$. It takes stages
into account: a variable declaration (written $x:\tau@A$) in a type
environment is associated with its declared stage $A$ as well as its type
$\tau$ and the type judgement of $\lambda^{\triangleright\%}$ is of the form
$\Gamma\vdash M:\tau@A$, in which $A$ stands for the stage of term $M$.333In
Hanada and Igarashi [14], it is written $\Gamma\vdash^{A}M:\tau$.  For
example, $y:\textrm{Int}@\alpha\vdash(\lambda
x:\textrm{Int}.y):\textrm{Int}\to\textrm{Int}@\alpha$ holds, but
$y:\textrm{Int}@\alpha\vdash(\lambda
x:\textrm{Int}.y):\textrm{Int}\to\textrm{Int}@\varepsilon$ does not because
the latter uses $y$ at stage $\varepsilon$ but $y$ is declared at $\alpha$.
Quotation ${\mathop{\blacktriangleright}}_{\alpha}M$ is given type
${\mathop{\triangleright}}_{\alpha}\tau$ at stage $A$ if $M$ is given type
$\tau$ at stage $A\alpha$; unquote ${\mathop{\blacktriangleleft}}_{\alpha}M$
is given type $\tau$ at stage $A\alpha$ if $M$ is given type
${\mathop{\triangleright}}_{\alpha}\tau$ at stage $A\alpha$; and CSP
$\%_{\alpha}M$ is give type $\tau$ at stage $A\alpha$ if $M$ is given type
$\tau$ at $A$. These are expressed by the following typing rules.

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
M:\tau@{A\alpha}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{\mathop{\blacktriangleright}}_{\alpha}M:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
M:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash{\mathop{\blacktriangleleft}}_{\alpha}M:\tau@{A\alpha}\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash\%_{\alpha}M:\tau@{A\alpha}\end{array}}$

###  2.2 Extending $\lambda^{\triangleright\%}$ with Dependent Types

In this paper, we add a simple form of dependent types—à la Edinburgh LF [15]
and $\lambda\textrm{LF}$ [1]—to $\lambda^{\triangleright\%}$. Types can be
indexed by terms as in Vector in Section 1 and $\lambda$-abstractions can be
given dependent function types of the form $\Pi x:\tau.\sigma$ but we do not
consider type operators (such as $\texttt{list }\tau$) or abstraction over
type variables. We introduce kinds to classify well-formed types and
equivalences for kinds, types, and terms—as in other dependent type
systems—but we have to address a question how the notion of stage (should)
interact with kinds and types.

On the one hand, base types such as Int should be able to be used at every
stage as in $\lambda^{\triangleright\%}$ so that $\lambda
x:\textrm{Int}.\Lambda\alpha.{\mathop{\blacktriangleright}}_{\alpha}\lambda
y:\textrm{Int}.M$ is a valid term (here, Int is used at $\varepsilon$ and
$\alpha$). Similarly for indexed types such as Vector 4. On the other hand, it
is not immediately clear how a type indexed by a variable, which can be used
only at a declared stage, can be used. For example, consider

${\mathop{\blacktriangleright}}_{\alpha}(\lambda
x:\textrm{Int}.({\mathop{\blacktriangleleft}}_{\alpha}(\lambda y:\text{Vector
}x.M)N))\text{ and }\lambda
x:\textrm{Int}.{\mathop{\blacktriangleright}}_{\alpha}(\lambda y:\text{Vector
}x.M).$

Is Vector $x$ a legitimate type at $\varepsilon$ (and $\alpha$, resp.) even if
$x:\textrm{Int}$ is declared at stage $\alpha$ (and $\varepsilon$, resp.)? We
will give our answer to this question in two steps.

First, type-level constants such as Int and Vector can be used at every stage
in $\lambda^{\textrm{MD}}$. Technically, we introduce a signature that
declares kinds of type-level constants and types of constants. For example, a
signature for the Boolean type and constants is given as follows
$\textrm{Bool}::*,\text{true}:\textrm{Bool},\text{false}:\textrm{Bool}$ (where
$*$ is the kind of proper types). Declarations in a signature are not
associated to particular stages; so they can be used at every stage.

Second, an indexed type such as Vector 3 or Vector $x$ is well formed only at
the stage(s) where the index term is well-typed. Since constant $3$ is well-
typed at every stage (if it is declared in the signature), Vector 3 is a well-
formed type at every stage, too. However, Vector $M$ is well-formed only at
the stage where index term $M$ is typed. Thus, the kinding judgment of
$\lambda^{\textrm{MD}}$ takes the form $\Gamma\vdash_{\Sigma}\tau::K@A$, where
stage $A$ stands for where $\tau$ is well-formed. For example, given
$\text{Vector}::\textrm{Int}\rightarrow*$ in the signature $\Sigma$,
$x:\textrm{Int}@\varepsilon\vdash_{\Sigma}\text{Vector }x::*@\varepsilon$ can
be derived but neither $x:\textrm{Int}@\alpha\vdash_{\Sigma}\text{Vector
}x::*@\varepsilon$ nor $x:\textrm{Int}@\varepsilon\vdash_{\Sigma}\text{Vector
}x::*@\alpha$ can be.

Apparently, the restriction above sounds too severe, because a term like
$\lambda x:\textrm{Int}.{\mathop{\blacktriangleright}}_{\alpha}(\lambda
y:\text{Vector }x.M)$, which models a typical code generator which takes the
size $x$ and returns code for vector manipulation specialized to the given
size, will be rejected. It seems crucial for $y$ to be given a type indexed by
$x$. We can address this problem by CSP—In fact, $\text{Vector }x$ is not well
formed at $\alpha$ under $x:\textrm{Int}@\varepsilon$ but $\text{Vector
}(\%_{\alpha}x)$ is! Thus, we can still write $\lambda
x:\textrm{Int}.{\mathop{\blacktriangleright}}_{\alpha}(\lambda y:\text{Vector
}(\%_{\alpha}x).M)$ for the typical sort of code generators.

Our decision that well-formedness of types takes stages of index terms into
account will lead to the introduction of CSP at the type level and special
equivalence rules, as we will see later.

##  3 Formal Definition of $\lambda^{\textrm{MD}}$

In this section, we give a formal definition of $\lambda^{\textrm{MD}}$,
including the syntax, full reduction, and type system. In addition to the full
reduction, in which any redex at any stage can be reduced, we also give staged
reduction, which models program execution (at $\varepsilon$-stage).

###  3.1 Syntax

We assume the denumerable set of _type-level constants_ , ranged over by
metavariables $X,Y,Z$, the denumerable set of _variables_ , ranged over by
$x,y,z$, the denumerable set of _constants_ , ranged over by $c$, and the
denumerable set of _stage variables_ , ranged over by $\alpha,\beta,\gamma$.
The metavariables $A,B,C$ range over sequences of stage variables; we write
$\varepsilon$ for the empty sequence. $\lambda^{\textrm{MD}}$ is defined by
the following grammar:

kinds $\displaystyle K,J,I,H,G$ $\displaystyle::=*\mid\Pi x:\tau.K$ types
$\displaystyle\tau,\sigma,\rho,\pi,\xi$ $\displaystyle::=X\mid\Pi
x:\tau.\sigma\mid\tau\
M\mid{\mathop{\triangleright}}_{\alpha}\tau\mid\forall\alpha.\tau$ terms
$\displaystyle M,N,L,O,P$ $\displaystyle::=c\mid x\mid\lambda x:\tau.M\ \mid
M\ N\mid{\mathop{\blacktriangleright}}_{\alpha}M$ $\displaystyle\ \ \ \
\mid{\mathop{\blacktriangleleft}}_{\alpha}M\mid\Lambda\alpha.M\mid M\
A\mid\%_{\alpha}M$ signatures $\displaystyle\Sigma$
$\displaystyle::=\emptyset\mid\Sigma,X::K\mid\Sigma,c:\tau$ type env.
$\displaystyle\Gamma$ $\displaystyle::=\emptyset\mid\Gamma,x:\tau@A$

A kind, which is used to classify types, is either $*$, the kind of proper
types (types that terms inhabit), or $\Pi x\colon\tau.K$, the kind of type
operators that takes $x$ as an argument of type $\tau$ and returns a type of
kind $K$. A type is a type-level constant $X$, which is declared in the
signature with its kind, a dependent function type $\Pi x:\tau.\sigma$, an
application $\tau\ M$ of a type (operator of $\Pi$-kind) to a term, a code
type ${\mathop{\triangleright}}_{\alpha}\tau$, or an $\alpha$-closed type
$\forall\alpha.\tau$. An example of an application of a type (operator) of
$\Pi$-kind to a term is $\text{Vector}\ 10$; it is well kinded if, say, the
type-level constant Vector has kind $\Pi x:\textrm{Int}.*$. A code type
${\mathop{\triangleright}}_{\alpha}\tau$ is for a code fragment of a term of
type $\tau$. An $\alpha$-closed type, when used with
${\mathop{\triangleright}}_{\alpha}$, represents runnable code.

Terms include ordinary (explicitly typed) $\lambda$-terms, constants, whose
types are declared in signature $\Sigma$, and the following five forms related
to multi-stage programming: ${\mathop{\blacktriangleright}}_{\alpha}M$
represents a code fragment; ${\mathop{\blacktriangleleft}}_{\alpha}M$
represents escape; $\Lambda\alpha.M$ is a stage variable abstraction; $M\ A$
is an application of a stage abstraction $M$ to stage $A$; and $\%_{\alpha}M$
is an operator for cross-stage persistence.

We adopt the tradition of $\lambda\textrm{LF}$-like systems, where types of
constants and kinds of type-level constants are globally declared in a
signature $\Sigma$, which is a sequence of declarations of the form $c:\tau$
and $X::K$. For example, when we use Boolean in $\lambda^{\textrm{MD}}$,
$\Sigma$ includes
$\textrm{Bool}::*,\textrm{true}:\textrm{Bool},\textrm{false}:\textrm{Bool}$.
Type environments are sequences of triples of a variable, its type, and its
stage. We write $\textit{dom}(\Sigma)$ and $\textit{dom}(\Gamma)$ for the set
of (type-level) constants and variables declared in $\Sigma$ and $\Gamma$,
respectively. As in other multi-stage calculi [30, 32, 14], a variable
declaration is associated with a stage so that a variable can be referenced
only at the declared stage. On the contrary, constants and type-level
constants are _not_ associated with stages; so, they can appear at any stage.
We define well-formed signatures and well-formed type environments later.

The variable $x$ is bound in $M$ by $\lambda x:\tau.M$ and in $\sigma$ by $\Pi
x:\tau.\sigma$, as usual; the stage variable $\alpha$ is bound in $M$ by
$\Lambda\alpha.M$ and $\tau$ by $\forall\alpha.\tau$. The notion of free
variables is defined in a standard manner. We write $\text{FV}(M)$ and
$\text{FSV}(M)$ for the set of free variables and the set of free stage
variables in $M$, respectively. Similarly, $\text{FV}(\tau)$,
$\text{FSV}(\tau)$, $\text{FV}(K)$, and $\text{FSV}(K)$ are defined. We
sometimes abbreviate $\Pi x:\tau_{1}.\tau_{2}$ to
$\tau_{1}\rightarrow\tau_{2}$ if $x$ is not a free variable of $\tau_{2}$. We
identify $\alpha$-convertible terms and assume the names of bound variables
are pairwise distinct.

The prefix operators
${\mathop{\triangleright}}_{\alpha},{\mathop{\blacktriangleright}}_{\alpha},{\mathop{\blacktriangleleft}}_{\alpha}$,
and $\%_{\alpha}$ are given higher precedence over the three forms $\tau\ M$,
$M\ N$, $M\ A$ of applications, which are left-associative. The binders $\Pi$,
$\forall$, and $\lambda$ extend as far to the right as possible. Thus,
$\forall\alpha.{\mathop{\triangleright}}_{\alpha}(\Pi
x:\textrm{Int}.\text{Vector}\ 5)$ is interpreted as
$\forall\alpha.({\mathop{\triangleright}}_{\alpha}(\Pi
x:\textrm{Int}.(\text{Vector}\ 5)))$; and $\Lambda\alpha.\lambda
x:\textrm{Int}.{\mathop{\blacktriangleright}}_{\alpha}x\ y$ means
$\Lambda\alpha.(\lambda
x:\textrm{Int}.({\mathop{\blacktriangleright}}_{\alpha}x)\ y)$.

##### Remark:

Basically, we define $\lambda^{\textrm{MD}}$ to be an extension of
$\lambda^{\triangleright\%}$ with dependent types. One notable difference is
that $\lambda^{\textrm{MD}}$ has only one kind of $\alpha$-closed types,
whereas $\lambda^{\triangleright\%}$ has two kinds of $\alpha$-closed types
$\forall\alpha.\tau$ and $\forall^{\varepsilon}\alpha.\tau$. We have omitted
the first kind, for simplicity, and dropped the superscript $\varepsilon$ from
the second. It would not be difficult to recover the distinction to show
properties related to program residualization [14], although they are left as
conjectures.

###  3.2 Reduction

Next, we define full reduction for $\lambda^{\textrm{MD}}$. Before giving the
definition of reduction, we define two kinds of substitutions. Substitution
$M[x\mapsto N],\tau[x\mapsto N]$ and $K[x\mapsto N]$ are ordinary capture-
avoiding substitution of term $N$ for $x$ in term $M$, type $\tau$, and kind
$K$, respectively, and we omit their definitions here. Substitution
$M[\alpha\mapsto A],\tau[\alpha\mapsto A],K[\alpha\mapsto A]$ and
$B[\alpha\mapsto A]$ are substitutions of stage $A$ for stage variable
$\alpha$ in term $M$, type $\tau$, kind $K$, and stage $B$, respectively. We
show representative cases below.

$\displaystyle(\lambda x:\tau.M)[\alpha\mapsto A]$ $\displaystyle=\lambda
x:(\tau[\alpha\mapsto A]).(M[\alpha\mapsto A])$ $\displaystyle(M\
B)[\alpha\mapsto A]$ $\displaystyle=(M[\alpha\mapsto A])\ B[\alpha\mapsto A]$
$\displaystyle({\mathop{\blacktriangleright}}_{\beta}M)[\alpha\mapsto A]$
$\displaystyle={\mathop{\blacktriangleright}}_{\beta[\alpha\mapsto
A]}M[\alpha\mapsto A]$
$\displaystyle({\mathop{\blacktriangleleft}}_{\beta}M)[\alpha\mapsto A]$
$\displaystyle={\mathop{\blacktriangleleft}}_{\beta[\alpha\mapsto
A]}M[\alpha\mapsto A]$ $\displaystyle(\%_{\beta}M)[\alpha\mapsto A]$
$\displaystyle=\%_{\beta[\alpha\mapsto A]}M[\alpha\mapsto A]$
$\displaystyle(\beta B)[\alpha\mapsto A]$ $\displaystyle=\beta(B[\alpha\mapsto
A])$ $\displaystyle(\text{if }\alpha\neq\beta)$ $\displaystyle(\beta
B)[\alpha\mapsto A]$ $\displaystyle=A(B[\alpha\mapsto A])$
$\displaystyle(\text{if }\alpha=\beta)$

Here, ${\mathop{\blacktriangleright}}_{\alpha_{1}\cdots\alpha_{n}}M$,
${\mathop{\blacktriangleleft}}_{\alpha_{1}\cdots\alpha_{n}}M$, and
$\%_{\alpha_{1}\cdots\alpha_{n}}M$ $(n\geq 0)$ stand for
${\mathop{\blacktriangleright}}_{\alpha_{1}}\cdots{\mathop{\blacktriangleright}}_{\alpha_{n}}M$,
${\mathop{\blacktriangleleft}}_{\alpha_{n}}\cdots{\mathop{\blacktriangleleft}}_{\alpha_{1}}M$,
and $\%_{\alpha_{n}}\cdots\%_{\alpha_{1}}M$, respectively. In particular,
${\mathop{\blacktriangleright}}_{\varepsilon}M={\mathop{\blacktriangleleft}}_{\varepsilon}M=\%_{\varepsilon}M=M$.
Also, it is important that the order of stage variables is reversed for
${\mathop{\blacktriangleleft}}$ and $\%$. We also define substitutions of a
stage or a term for variables in type environment $\Gamma$.

######  Definition 1 (Reduction)

The relations $M\longrightarrow_{\beta}N$,
$M\longrightarrow_{\blacklozenge}N$, and $M\longrightarrow_{\Lambda}N$ are the
least compatible relations closed under the rules below.

$\displaystyle(\lambda x:\tau.M)N$
$\displaystyle\longrightarrow_{\beta}M[x\mapsto N]$
$\displaystyle{\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}M$
$\displaystyle\longrightarrow_{\blacklozenge}M$
$\displaystyle(\Lambda\alpha.M)\ A$
$\displaystyle\longrightarrow_{\Lambda}M[\alpha\mapsto A]$

We write $M\longrightarrow M^{\prime}$ iff
$M\longrightarrow_{\beta}M^{\prime}$,
$M\longrightarrow_{\blacklozenge}M^{\prime}$, or
$M\longrightarrow_{\Lambda}M^{\prime}$ and we call $\longrightarrow_{\beta}$,
$\longrightarrow_{\blacklozenge}$, and $\longrightarrow_{\Lambda}$
$\beta$-reduction, $\blacklozenge$-reduction, and $\Lambda$-reduction,
respectively. $M\longrightarrow^{*}N$ means that there is a sequence of
reduction $\longrightarrow$ whose length is greater than or equal to 0.

The relation $\longrightarrow_{\beta}$ represents ordinary $\beta$-reduction
in the $\lambda$-calculus; the relation $\longrightarrow_{\blacklozenge}$
represents that quotation ${\mathop{\blacktriangleright}}_{\alpha}M$ is
canceled by escape and $M$ is spliced into the code fragment surrounding the
escape; the relation $\longrightarrow_{\Lambda}$ means that a stage
abstraction applied to stage $A$ reduces to the body of the abstraction where
$A$ is substituted for the stage variable. There is no reduction rule for CSP
as with Hanada and Igarashi [14]. The CSP operator $\%_{\alpha}$ disappears
when $\varepsilon$ is substituted for $\alpha$. We show an example of a
reduction sequence below. Underlines show the redexes.

$\displaystyle\hskip 28.45274pt\underline{(\lambda
f:\textrm{Int}\to\textrm{Int}.(\Lambda\alpha.{\mathop{\blacktriangleright}}_{\alpha}(\%_{\alpha}f\
1+({\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}3))\
\varepsilon))\ (\lambda x:\textrm{Int}.x)}$
$\displaystyle\longrightarrow_{\beta}(\Lambda\alpha.{\mathop{\blacktriangleright}}_{\alpha}(\%_{\alpha}(\lambda
x:\textrm{Int}.x)\
1+(\underline{{\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}3})))\
\varepsilon$
$\displaystyle\longrightarrow_{\blacklozenge}\underline{(\Lambda\alpha.{\mathop{\blacktriangleright}}_{\alpha}(\%_{\alpha}(\lambda
x:\textrm{Int}.x)\ 1+3))\ \varepsilon}$
$\displaystyle\longrightarrow_{\Lambda}\underline{(\lambda x:\textrm{Int}.x)\
1}+3$ $\displaystyle\longrightarrow_{\beta}1+3$
$\displaystyle\longrightarrow^{*}4$

###  3.3 Type System

In this section, we define the type system of $\lambda^{\textrm{MD}}$. It
consists of eight judgment forms for signature well-formedness, type
environment well-formedness, kind well-formedness, kinding, typing, kind
equivalence, type equivalence, and term equivalence. We list the judgment
forms in Figure 1. They are all defined in a mutual recursive manner. We will
discuss each judgment below.

$\displaystyle\vdash$ $\displaystyle\Sigma$ signature well-formedness
$\displaystyle\vdash_{\Sigma}$ $\displaystyle\Gamma$ type environment well-
formedness $\displaystyle\Gamma$ $\displaystyle\vdash_{\Sigma}K\text{\
kind}@A$ kind well-formedness $\displaystyle\Gamma$
$\displaystyle\vdash_{\Sigma}\tau::K@A$ kinding $\displaystyle\Gamma$
$\displaystyle\vdash_{\Sigma}M:\tau@A$ typing $\displaystyle\Gamma$
$\displaystyle\vdash_{\Sigma}K\equiv J@A$ kind equivalence
$\displaystyle\Gamma$ $\displaystyle\vdash_{\Sigma}\tau\equiv\sigma::K@A$ type
equivalence $\displaystyle\Gamma$ $\displaystyle\vdash_{\Sigma}M\equiv
N:\tau@A$ term equivalence Figure 1: Eight judgment forms of the type system
of $\lambda^{\textrm{MD}}$.

####  3.3.1 Signature and Type Environment Well-formedness.

The rules for Well-formed signatures and type environments are shown below:

$\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\vdash\emptyset\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\vdash\Sigma\quad\quad\vdash_{\Sigma}K\text{\
kind}@\varepsilon\\\
X\notin\textit{dom}(\Sigma)\end{array}}{\begin{array}[]{@{}c@{}}\vdash\Sigma,X::K\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\vdash\Sigma\quad\quad\vdash_{\Sigma}\tau::*@\varepsilon\\\
c\notin\textit{dom}(\Sigma)\end{array}}{\begin{array}[]{@{}c@{}}\vdash\Sigma,c:\tau\end{array}}$

$\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\Sigma}\emptyset\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\vdash_{\Sigma}\Gamma\quad\quad\Gamma\vdash_{\Sigma}\tau::*@A\quad\quad
x\notin\textit{dom}(\Sigma)\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\Sigma}\Gamma,x:\tau@A\end{array}}$

To add declarations to a signature, the kind/type of a (type-level) constant
has to be well-formed at stage $\varepsilon$ so that it is used at any stage.
In what follows, well-formedness is not explicitly mentioned but we assume
that all signatures and type environments are well-formed.

####  3.3.2 Kind Well-formedness and Kinding.

The rules for kind well-formedness and kinding are a straightforward
adaptation from $\lambda\textrm{LF}$ and $\lambda^{\triangleright\%}$, except
for the following rule for type-level CSP.

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\alpha\end{array}}$
(K-Csp)

Unlike the term level, type-level CSP is implicit because there is no staged
semantics for types.

####  3.3.3 Typing.

$\frac{\begin{array}[]{@{}c@{}}c:\tau\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}c:\tau@A\end{array}}$
(T-Const)
$\frac{\begin{array}[]{@{}c@{}}x:\tau@A\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}x:\tau@A\end{array}}$
(T-Var)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\sigma::*@A\quad\quad\Gamma,x:\sigma@A\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\lambda(x:\sigma).M):(\Pi(x:\sigma).\tau)@A\end{array}}$
(T-Abs)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:(\Pi(x:\sigma).\tau)@A\quad\quad\Gamma\vdash_{\Sigma}N:\sigma@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\
N:\tau[x\mapsto N]@A\end{array}}$ (T-App)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\quad\quad\Gamma\vdash_{\Sigma}\tau\equiv\sigma::K@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\sigma@A\end{array}}$
(T-Conv)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@{A\alpha}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}$
(T-${\mathop{\blacktriangleright}}$)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleleft}}_{\alpha}M:\tau@{A\alpha}\end{array}}$
(T-${\mathop{\blacktriangleleft}}$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\quad\quad\alpha\notin\rm{FTV}(\Gamma)\cup\rm{FTV}(A)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\Lambda\alpha.M:\forall\alpha.\tau@A\end{array}}$
(T-Gen)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\forall\alpha.\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\
B:\tau[\alpha\mapsto B]@A\end{array}}$ (T-Ins)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\%_{\alpha}M:\tau@{A\alpha}\end{array}}$
(T-Csp)

Figure 2: Typing Rules.

The typing rules of $\lambda^{\textrm{MD}}$ are shown in Figure 2. The rule
T-Const means that a constant can appear at any stage. The rules T-Var, T-Abs,
and T-App are almost the same as those in the simply typed lambda calculus or
$\lambda\textrm{LF}$. Additional conditions are that subterms must be typed at
the same stage (T-Abs and T-App); the type annotation/declaration on a
variable has to be a proper type of kind $*$ (T-Abs) at the stage where it is
declared (T-Var and T-Abs).

As in standard dependent type systems, T-Conv allows us to replace the type of
a term with an equivalent one. For example, assuming integers and arithmetic,
a value of type $\textrm{Vector}\ (4+1)$ can also have type $\textrm{Vector}\
5$ because of T-Conv.

The rules T-${\mathop{\blacktriangleright}}$,
T-${\mathop{\blacktriangleleft}}$, T-Gen, T-Ins, and T-Csp are constructs for
multi-stage programming. T-${\mathop{\blacktriangleright}}$ and
T-${\mathop{\blacktriangleleft}}$ are the same as in
$\lambda^{\triangleright\%}$, as we explained in Section 2. The rule T-Gen for
stage abstraction is straightforward. The condition
$\alpha\notin\rm{FTV}(\Gamma)\cup\rm{FTV}(A)$ ensures that the scope of
$\alpha$ is in $M$, and avoids capturing variables elsewhere. The rule T-Ins
is for applications of stages to stage abstractions. The rule T-Csp is for
CSP, which means that, if term $M$ is of type $\tau$ at stage $A$, then
$\%_{\alpha}M$ is of type $\tau$ at stage $A\alpha$. Note that CSP is also
applied to the type $\tau$ (although it is implicit) in the conclusion. Thanks
to implicit CSP, the typing rule is the same as in
$\lambda^{\triangleright\%}$.

####  3.3.4 Kind, Type and Term Equivalence.

Since the syntax of kinds, types, and terms is mutually recursive, the
corresponding notions of equivalence are also mutually recursive. They are
congruences closed under a few axioms for term equivalence. Thus, the rules
for kind and type equivalences are not very interesting, except that implicit
CSP is allowed. We show a few representative rules below.

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
J@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
J@A\alpha\end{array}}$ (QK-Csp)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@{A\alpha}\end{array}}$
(QT-Csp)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::(\Pi
x:\rho.K)@A\quad\quad\Gamma\vdash_{\Sigma}M\equiv
N:\rho@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\
M\equiv\sigma\ N::K[x\mapsto M]@A\end{array}}$ (QT-App)

We show the rules for term equivalence in Figure 3, omitting straightforward
rules for reflexivity, symmetry, transitivity, and compatibility. The rules
Q-$\beta$, Q-${\mathop{\blacktriangleleft}}{\mathop{\blacktriangleright}}$,
and Q-$\Lambda$ correspond to $\beta$-reduction, $\blacklozenge$-reduction,
and $\Lambda$-reduction, respectively.

$\frac{\begin{array}[]{@{}c@{}}\Gamma,x:\sigma@A\vdash_{\Sigma}M:\tau@A\quad\quad\Gamma\vdash_{\Sigma}N:\sigma@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\lambda
x:\sigma.M)\ N\equiv M[x\mapsto N]:\tau[x\mapsto N]@A\end{array}}$ (Q-$\beta$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\Lambda\alpha.M):\forall\alpha.\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\Lambda\alpha.M)\
\varepsilon\equiv
M[\alpha\mapsto\varepsilon]:\tau[\alpha\mapsto\varepsilon]@A\end{array}}$
(Q-$\Lambda$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleleft}}_{\alpha}({\mathop{\blacktriangleright}}_{\alpha}M)\equiv
N:\tau@A\end{array}}$
(Q-${\mathop{\blacktriangleleft}}{\mathop{\blacktriangleright}}$)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@{A\alpha}\quad\quad\Gamma\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\%_{\alpha}M\equiv
M:\tau@{A\alpha}\end{array}}$ (Q-%)

Figure 3: Term Equivalence Rules.

The only rule that deserves elaboration is the last rule Q-%. Intuitively, it
means that the CSP operator applied to term $M$ can be removed if $M$ is also
well-typed at the next stage $A\alpha$. For example, constants do not depend
on the stage (see T-Const) and so $\Gamma\vdash_{\Sigma}\%_{\alpha}c\equiv
c:\tau@A\alpha$ holds but variables do depend on stages and so this rule does
not apply.

####  3.3.5 Example.

We show an example of a dependently typed code generator in a hypothetical
language based on $\lambda^{\triangleright\%}$. This language provides
definitions by let, recursive functions (represented by fix), if-expressions,
and primitives cons, head, and tail to manipulate vectors. We assume that cons
is of type $\Pi n:\textrm{Int}.\textrm{Int}\to\text{Vector}\
n\to\text{Vector}\ (n+1)$, head is of type $\Pi n:\textrm{Int}.\text{Vector}\
(n+1)\to\textrm{Int}$, and tail is of type $\Pi n:\textrm{Int}.\text{Vector}\
(n+1)\to(\text{Vector}\ n)$.

Let’s consider an application, for example, in computer graphics, in which we
have potentially many pairs of vectors of the fixed (but statically unknown)
length and a function—such as vector addition—to be applied to them. This
function should be fast because it is applied many times and be safe because
just one runtime error may ruin the whole long-running calculation.

Our goal is to define the function vadd of type

$\Pi
n:\textrm{Int}.\forall\beta.{\mathop{\triangleright}}_{\beta}(\text{Vector}\
(\%_{\alpha}n)\to\text{Vector}\ (\%_{\alpha}n)\to\text{Vector}\
(\%_{\alpha}n)).$

It takes the length $n$ and returns ($\beta$-closed) code of a function to add
two vectors of length $n$. The generated code is run by applying it to
$\varepsilon$ to obtain a function of type $\text{Vector}\ n\to\text{Vector}\
n\to\text{Vector}\ n$ as expected.

We start with the helper function vadd1, which takes a stage, the length $n$
of vectors, and two quoted vectors as arguments and returns code that computes
the addition of the given two vectors:

$\textbf{let}\ \text{vadd}_{1}:\forall\alpha.\Pi
n:\textrm{Int}.{\mathop{\triangleright}}_{\alpha}\text{Vector}\
n\to{\mathop{\triangleright}}_{\alpha}\text{Vector}\
n\to{\mathop{\triangleright}}_{\alpha}\text{Vector}\ n$
---
|  $=\textbf{fix}\ f.\Lambda\alpha.\lambda n:\textrm{Int}.\ \lambda
v_{1}:{\mathop{\triangleright}}_{\alpha}\text{Vector}\ n.\ \lambda
v_{2}:{\mathop{\triangleright}}_{\alpha}\text{Vector}\ n.$
|  |  $\textbf{if}\ n=0\ \textbf{then}\ {\mathop{\blacktriangleright}}_{\alpha}\text{nil}$
|  |  $\textbf{else}\ {\mathop{\blacktriangleright}}_{\alpha}($ |  $\textbf{let}\ t_{1}=\text{tail}\ ({\mathop{\blacktriangleleft}}_{\alpha}v_{1})\ \textbf{in}$
|  |  |  $\textbf{let}\ t_{2}=\text{tail}\ ({\mathop{\blacktriangleleft}}_{\alpha}v_{2})\ \textbf{in}$
|  |  |  cons |  $(\text{head}\ ({\mathop{\blacktriangleleft}}_{\alpha}v_{1})+\text{head}\ ({\mathop{\blacktriangleleft}}_{\alpha}v_{2}))$
|  |  |  |  ${\mathop{\blacktriangleleft}}_{\alpha}(f\ (n-1)\ ({\mathop{\blacktriangleright}}_{\alpha}t_{1})\ ({\mathop{\blacktriangleright}}_{\alpha}t_{2})))$

Note that the generated code will not contain branching on $n$ or recursion.
(Here, we assume that the type system can determine whether $n=0$ when then\-
and else-branches are typechecked so that both branches can be given type
${\mathop{\triangleright}}_{\alpha}\text{Vector }n$.)

Using vadd1, the main function vadd can be defined as follows:

$\displaystyle\textbf{let}\ \text{vadd}:\Pi
n:\textrm{Int}.\forall\beta.{\mathop{\triangleright}}_{\beta}(\text{Vector}\
(\%_{\beta}n)\to\text{Vector}\ (\%_{\beta}n)\to\text{Vector}\ (\%_{\beta}n))$
$\displaystyle\hskip 17.07164pt=\lambda
n:\textrm{Int}.\Lambda\beta.{\mathop{\blacktriangleright}}_{\beta}(\lambda
v_{1}:\text{Vector}\ (\%_{\beta}n).\ \lambda v_{2}:\text{Vector}\
(\%_{\beta}n).$ $\displaystyle\hskip
179.25235pt{\mathop{\blacktriangleleft}}_{\beta}(\text{vadd}_{1}\ \beta\ n\
({\mathop{\blacktriangleright}}_{\beta}\ v_{1})\
({\mathop{\blacktriangleright}}_{\beta}\ v_{2})))$

The auxiliary function vadd1 generates code to compute addition of the formal
arguments $v_{1}$ and $v_{2}$ without branching on $n$ or recursion. As we
mentioned already, if this function is applied to a (nonnegative) integer
constant, say 5, it returns function code for adding two vectors of size 5.
The type of vadd 5, obtained by substituting 5 for $n$, is
$\forall\beta.{\mathop{\triangleright}}_{\beta}(\text{Vector}\
(\%_{\beta}5)\to\text{Vector}\ (\%_{\beta}5)\to\text{Vector}\ (\%_{\beta}5))$.
If the obtained code is run by applying to $\varepsilon$, the type of vadd 5
$\varepsilon$ is $\text{Vector}\ 5\to\text{Vector}\ 5\to\text{Vector}\ 5$ as
expected.

There are other ways to implement the vector addition function: by using
tuples instead of lists if the length for all the vectors is statically known
or by checking dynamically the lengths of lists for every pair. However, our
method is better than these alternatives in two points. First, our function,
$\text{vadd}_{1}$ can generate functions for vectors of arbitrary length
unlike the one using tuples. Second, $\text{vadd}_{1}$ has an advantage in
speed over the one using dynamic checking because it can generate an optimized
function for a given length.

We make two technical remarks before proceeding:

  1. 1.

If the generated function code is composed with another piece of code of type,
say, ${\mathop{\triangleright}}_{\gamma}\text{Vector }5$, Q-% plays an
essential role; that is, $\text{Vector }5$ and $\text{Vector }(\%_{\gamma}5)$,
which would occur by applying the generated code to $\gamma$ (instead of
$\varepsilon$), are syntactically different types but Q-% enables to equate
them. Interestingly, Hanada and Igarashi [14] rejected the idea of reduction
that removes $\%_{\alpha}$ when they developed $\lambda^{\triangleright\%}$,
as such reduction does not match the operational behavior of the CSP operator
in implementations. However, as an equational system for multi-stage programs,
the rule Q-% makes sense.

  2. 2.

By using implicit type-level CSP, the type of vadd could have been written
$\Pi
n:\textrm{Int}.\forall\beta.{\mathop{\triangleright}}_{\beta}(\text{Vector}\
n\to\text{Vector}\ n\to\text{Vector}\ n)$. In this type, Vector $n$ is given
kind at stage $\varepsilon$ and type-level CSP implicitly lifts it to stage
$\beta$. However, if a type-level constant takes two or more arguments from
different stages, term-level CSP is necessary. A matrix type (indexed by the
numbers of columns and rows) would be such an example.

###  3.4 Staged Semantics

The reduction given above is full reduction and any redexes—even under
${\mathop{\blacktriangleright}}_{\alpha}$—can be reduced in an arbitrary
order. Following previous work [14], we introduce (small-step, call-by-value)
staged semantics, where only $\beta$-reduction or $\Lambda$-reduction at stage
$\varepsilon$ or the outer-most $\blacklozenge$-reduction are allowed,
modeling an implementation.

We start with the definition of values. Since terms under quotations are not
executed, the grammar is indexed by stages.

######  Definition 2 (Values)

The family $V^{A}$ of sets of values, ranged over by $v^{A}$, is defined by
the following grammar. In the grammar, $A^{\prime}\neq\varepsilon$ is assumed.

$\displaystyle v^{\varepsilon}\in V^{\varepsilon}$ $\displaystyle::=\lambda
x:\tau.M\mid\
{\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}\mid\Lambda\alpha.v^{\varepsilon}$
$\displaystyle v^{A^{\prime}}\in V^{A^{\prime}}$ $\displaystyle::=x\mid\lambda
x:\tau.v^{A^{\prime}}\mid v^{A^{\prime}}\ v^{A^{\prime}}\mid\
{\mathop{\blacktriangleright}}_{\alpha}v^{A^{\prime}\alpha}\mid\Lambda\alpha.v^{A^{\prime}}\mid
v^{A^{\prime}}\ B$ $\displaystyle\quad\ \mid\
{\mathop{\blacktriangleleft}}_{\alpha}v^{A^{\prime\prime}}(\text{if
}A^{\prime}=A^{\prime\prime}\alpha\text{ for some
}\alpha,A^{\prime\prime}\neq\varepsilon)$ $\displaystyle\quad\ \mid\
\%_{\alpha}v^{A^{\prime\prime}}(\text{if }A^{\prime}=A^{\prime\prime}\alpha)$

Values at stage $\varepsilon$ are $\lambda$-abstractions, quoted pieces of
code, or $\Lambda$-abstractions. The body of a $\lambda$-abstraction can be
any term but the body of $\Lambda$-abstraction has to be a value. It means
that the body of $\Lambda$-abstraction must be evaluated. The side condition
for ${\mathop{\blacktriangleleft}}_{\alpha}v^{A^{\prime}}$ means that escapes
in a value can appear only under nested quotations because an escape under a
single quotation will splice the code value into the surrounding code. See
Hanada and Igarashi [14] for details.

In order to define staged reduction, we define redex and evaluation contexts.

######  Definition 3 (Redex)

The sets of $\varepsilon$-redexes (ranged over by $R^{\varepsilon}$) and
$\alpha$-redexes (ranged over by $R^{\alpha}$) are defined by the following
grammar.

$\displaystyle R^{\varepsilon}::=(\lambda x:\tau.M)\
v^{\varepsilon}\mid(\Lambda\alpha.v^{\varepsilon})\ \varepsilon$
$\displaystyle R^{\alpha}::=\
{\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}$

######  Definition 4 (Evaluation Context)

Let $B$ be either $\varepsilon$ or a stage variable $\beta$. The family of
sets $ECtx^{A}_{B}$ of evaluation contexts, ranged over by $E^{A}_{B}$, is
defined by the following grammar (in which $A^{\prime}$ stands for a non-empty
stage).

$\displaystyle E^{\varepsilon}_{B}\in ECtx^{\varepsilon}_{B}$
$\displaystyle::=\square\ (\text{if\ }B=\varepsilon)\mid E^{\varepsilon}_{B}\
M\mid v^{\varepsilon}\
E^{\varepsilon}_{B}\mid{\mathop{\blacktriangleright}}_{\alpha}E^{\alpha}_{B}\mid\Lambda\alpha.E^{\varepsilon}_{B}\mid
E^{\varepsilon}_{B}\ A$ $\displaystyle E^{A^{\prime}}_{B}\in
ECtx^{A^{\prime}}_{B}$ $\displaystyle::=\square\ (\text{if
}A^{\prime}=B)\mid\lambda x:\tau.E^{A^{\prime}}_{B}\mid E^{A^{\prime}}_{B}\
M\mid v^{A^{\prime}}\ E^{A^{\prime}}_{B}$
$\displaystyle\mid{\mathop{\blacktriangleright}}_{\alpha}E^{A^{\prime}\alpha}_{B}\mid{\mathop{\blacktriangleleft}}_{\alpha}E^{A}_{B}\
(\text{where }A\alpha=A^{\prime})$
$\displaystyle\mid\Lambda\alpha.E^{A^{\prime}}_{B}\mid E^{A^{\prime}}_{B}\
A\mid\%_{\alpha}\ E^{A}_{B}\ (\text{where }A\alpha=A^{\prime})$

The subscripts $A$ and $B$ in $E^{A}_{B}$ stand for the stage of the
evaluation context and of the hole, respectively. The grammar represents that
staged reduction is left-to-right and call-by-value and terms under $\Lambda$
are reduced. Terms at non-$\varepsilon$ stages are not reduced, except redexes
of the form
${\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}$
at stage $\alpha$. A few examples of evaluation contexts are shown below:

$\displaystyle\square\ (\lambda x:\textrm{Int}.x)$ $\displaystyle\in
ECtx^{\varepsilon}_{\varepsilon}$ $\displaystyle\Lambda\alpha.\square\
\varepsilon$ $\displaystyle\in ECtx^{\varepsilon}_{\varepsilon}$
$\displaystyle{\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}{\mathop{\blacktriangleleft}}_{\alpha}\square$
$\displaystyle\in ECtx^{\alpha}_{\varepsilon}$

We write $E^{A}_{B}[M]$ for the term obtained by filling the hole $\square$ in
$E^{A}_{B}$ by $M$.

Now we define staged reduction using the redex and evaluation contexts.

######  Definition 5 (Staged Reduction)

The staged reduction relation, written $M\longrightarrow_{s}N$, is defined by
the least relation closed under the rules below.

$\displaystyle E^{A}_{\varepsilon}[(\lambda x:\tau.M)\ v^{\varepsilon}]$
$\displaystyle\longrightarrow_{s}E^{A}_{\varepsilon}[M[x\mapsto
v^{\varepsilon}]]$ $\displaystyle
E^{A}_{\varepsilon}[(\Lambda\alpha.v^{\varepsilon})\ A]$
$\displaystyle\longrightarrow_{s}E^{A}_{\varepsilon}[v^{\varepsilon}[\alpha\mapsto
A]]$ $\displaystyle
E^{A}_{\alpha}[{\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}]$
$\displaystyle\longrightarrow_{s}E^{A}_{\alpha}[v^{\alpha}]$

This reduction relation reduces a term in a deterministic, left-to-right,
call-by-value manner. An application of an abstraction is executed only at
stage $\varepsilon$ and only a quotation at stage $\varepsilon$ is spliced
into the surrounding code—notice that, if
${\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}$ is at stage $\varepsilon$,
then the redex
${\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}$
is at stage $\alpha$. In other words, terms in brackets are not evaluated
until the terms are run and arguments of a function are evaluated before the
application. We show an example of staged reduction. Underlines show the
redexes.

$\displaystyle(\Lambda\alpha.({\mathop{\blacktriangleright}}_{\alpha}\underline{{\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}((\lambda
x:\textrm{Int}.x)\ 10))})\ \varepsilon$ $\displaystyle\longrightarrow_{s}$
$\displaystyle\underline{(\Lambda\alpha.({\mathop{\blacktriangleright}}_{\alpha}((\lambda
x:\textrm{Int}.x)\ 10)))\ \varepsilon}$ $\displaystyle\longrightarrow_{s}$
$\displaystyle\underline{(\lambda x:\textrm{Int}.x)\ 10}$
$\displaystyle\longrightarrow_{s}$ $\displaystyle 10$

##  4 Properties of $\lambda^{\textrm{MD}}$

In this section, we show the basic properties of $\lambda^{\textrm{MD}}$:
preservation, strong normalization, confluence for full reduction, and
progress for staged reduction.

The Substitution Lemma in $\lambda^{\textrm{MD}}$ is a little more complicated
than usual because there are eight judgment forms and two kinds of
substitution. The Term Substitution Lemma states that term substitution
$[z\mapsto M]$ preserves derivability of judgments. The Stage Substitution
Lemma states similarly for stage substitution $[\alpha\mapsto A]$.

We let $\mathcal{J}$ stand for the judgments $K\text{\ kind}@A$, $\tau::K@A$,
$M:\tau@A$, $K\equiv J@A$, $\tau\equiv\sigma@A$, and $M\equiv N:\tau@A$.
Substitutions $\mathcal{J}[z\mapsto M]$ and $\mathcal{J}[\alpha\mapsto A]$ are
defined in a straightforward manner. Using these notations, the two
substitution lemmas are stated as follows:

We proved the next two leammas by simultaneous induction on derivations.

######  Lemma 1 (Term Substitution)

If $\Gamma,z:\xi@B,\Delta\vdash_{\Sigma}\mathcal{J}$ and
$\Gamma\vdash_{\Sigma}N:\xi@B$, then $\Gamma,(\Delta[z\mapsto
N])\vdash_{\Sigma}\mathcal{J}[z\mapsto N]$. Similarly, if
$\vdash_{\Sigma}\Gamma,z:\xi@B,\Delta$ and $\Gamma\vdash_{\Sigma}N:\xi@B$,
then $\vdash_{\Sigma}\Gamma,(\Delta[z\mapsto N])$.

######  Lemma 2 (Stage Substitution)

If $\Gamma\vdash_{\Sigma}\mathcal{J}$, then $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}\mathcal{J}[\beta\mapsto B]$. Similarly, if
$\vdash_{\Sigma}\Gamma$, then $\vdash_{\Sigma}\Gamma[\beta\mapsto B]$.

The following Inversion Lemma is needed to prove the main theorems. As usual
[27], the Inversion Lemma enables us to infer the types of subterms of a term
from the shape of the term.

######  Lemma 3 (Inversion)

  1. 1.

If $\Gamma\vdash_{\Sigma}(\lambda x:\sigma.M):\rho$ then there are
$\sigma^{\prime}$ and $\tau^{\prime}$ such that $\rho=\Pi
x:\sigma^{\prime}.\tau^{\prime}$,
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}@A$ and
$\Gamma,x:\sigma^{\prime}@A\vdash_{\Sigma}M:\tau^{\prime}@A$.

  2. 2.

If $\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M:\tau@A$ then
there is $\sigma$ such that $\tau={\mathop{\triangleright}}_{\alpha}\sigma$
and $\Gamma\vdash_{\Sigma}M:\sigma@A$.

  3. 3.

If $\Gamma\vdash_{\Sigma}\Lambda\alpha.M:\tau$ then there is $\sigma$ such
that $\sigma=\forall\alpha.\sigma$ and $\Gamma\vdash_{\Sigma}M:\sigma@A$.

###### Proof

Each item is strengthened by statements about type equivalence. For example,
the first statement is augmented by

> If $\Gamma\vdash_{\Sigma}\rho\equiv(\Pi x:\sigma.\tau):K@A$, then there
> exist $\sigma^{\prime}$ and $\tau^{\prime}$ such that $\rho=\Pi
> x:\sigma^{\prime}.\tau^{\prime}$ and
> $\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}:K@A$ and
> $\Gamma,x:\sigma@A\vdash_{\Sigma}\tau\equiv\tau^{\prime}:J@A$.

and its symmetric version. Then, they are proved simultaneously by induction
on derivations. Similarly for the others. ∎

Thanks to Term/Stage Substitution and Inversion, we can prove Preservation
easily.

######  Theorem 4.1 (Preservation)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow M^{\prime}$, then
$\Gamma\vdash_{\Sigma}M^{\prime}:\tau@A$.

###### Proof

First, there are three cases for $M\longrightarrow M^{\prime}$. They are
$M\longrightarrow_{\beta}M^{\prime}$, $M\longrightarrow_{\Lambda}M^{\prime}$,
and $M\longrightarrow_{\blacklozenge}M^{\prime}$. For each case, we can use
straightforward induction on typing derivations. ∎

Strong Normalization is also an important property, which guarantees that no
typed term has an infinite reduction sequence. Following standard proofs (see,
e.g., [15]), we prove this theorem by translating $\lambda^{\textrm{MD}}$ to
the simply typed lambda calculus.

######  Theorem 4.2 (Strong Normalization)

If $\Gamma\vdash_{\Sigma}M_{1}:\tau@A$ then there is no infinite sequence
$(M_{i})_{i\geq 1}$ of terms such that $M_{i}\longrightarrow M_{i+1}$ for
$i\geq 1$.

###### Proof

In order to prove this theorem, we define a translation $(\cdot)^{\natural}$
from $\lambda^{\textrm{MD}}$ to the simply typed lambda calculus. Second, we
prove the $\natural$-translation preserves typing and reduction. Then, we can
prove Strong Normalization of $\lambda^{\textrm{MD}}$ from Strong
Normalization of the simply typed lambda calculus. ∎

Confluence is a property that any reduction sequences from one typed term
converge. Since we have proved Strong Normalization, we can use Newman’s Lemma
[2] to prove Confluence.

######  Theorem 4.3 (Confluence)

For any term $M$, if $M\longrightarrow^{*}M^{\prime}$ and
$M\longrightarrow^{*}M^{\prime\prime}$ then there exists
$M^{\prime\prime\prime}$ that satisfies
$M^{\prime}\longrightarrow^{*}M^{\prime\prime\prime}$ and
$M^{\prime\prime}\longrightarrow^{*}M^{\prime\prime\prime}$.

###### Proof

We can easily show Weak Church-Rosser. Use Newman’s Lemma. ∎

Now, we turn our attention to staged semantics. First, the staged reduction
relation is a subrelation of full reduction, so Subject Reduction holds also
for the staged reduction.

###### Theorem 4.4

If $M\longrightarrow_{s}M^{\prime}$, then $M\longrightarrow M^{\prime}$.

###### Proof

Easy. ∎

The following theorem Unique Decomposition ensures that every typed term is
either a value or can be uniquely decomposed to an evaluation context and a
redex, ensuring that a well-typed term is not immediately stuck and the staged
semantics is deterministic.

######  Theorem 4.5 (Unique Decomposition)

If $\Gamma$ does not have any variable declared at stage $\varepsilon$ and
$\Gamma\vdash_{\Sigma}M:\tau@A$, then either

  1. 1.

$M\in V^{A}$, or

  2. 2.

$M$ can be uniquely decomposed into an evaluation context and a redex, that
is, there uniquely exist $B,E^{A}_{B}$, and $R^{B}$ such that
$M=E^{A}_{B}[R^{B}]$.

###### Proof

We can prove by straightforward induction on typing derivations. ∎

The type environment $\Gamma$ in the statement usually has to be empty; in
other words, the term has to be closed. The condition is relaxed here because
variables at stages higher than $\varepsilon$ are considered symbols. In fact,
this relaxation is required for proof by induction to work.

Progress is a corollary of Unique Decomposition.

######  Corollary 1 (Progress)

If $\Gamma$ does not have any variable declared at stage $\varepsilon$ and
$\Gamma\vdash_{\Sigma}M:\tau@A$, then $M\in V^{A}$ or there exists
$M^{\prime}$ such that $M\longrightarrow_{s}M^{\prime}$.

##  5 Related Work

MetaOCaml is a programming language with quoting, unquoting, run, and CSP.
Kiselyov [17] describes many applications of MetaOCaml, including filtering in
signal processing, matrix-vector product, and a DSL compiler.

Theoretical studies on multi-stage programming owe a lot to seminal work by
Davies and Pfenning [11] and Davies [10], who found Curry-Howard
correspondence between multi-stage calculi and modal logic. In particular,
Davies’ $\lambda^{\circ}$ [10] has been a basis for several multi-stage
calculi with quasi-quotation. $\lambda^{\circ}$ did not have operators for run
and CSP; a few studies [3, 24] enhanced and improved $\lambda^{\circ}$ towards
the development of a type-safe multi-stage calculus with quasi-quotation, run,
and CSP, which were proposed by Taha and Sheard as constructs for multi-stage
programming [31]. Finally, Taha and Nielsen invented the concept of
environment classifiers [30] and developed a typed calculus
$\lambda^{\alpha}$, which was equipped with all the features above in a type
sound manner and formed a basis of earlier versions of MetaOCaml. Different
approaches to type-safe multi-stage programming with slightly different
constructs for composing and running code values have been studied by Kim, Yi,
and Calcagno [16] and Nanevski and Pfenning [25].

Later, Tsukada and Igarashi [32] found correspondence between a variant of
$\lambda^{\alpha}$ called $\lambda^{\mathop{\triangleright}}$ and modal logic
and showed that run could be represented as a special case of application of a
transition abstraction ($\Lambda\alpha.M$) to the empty sequence
$\varepsilon$. Hanada and Igarashi [14] developed $\lambda^{\triangleright\%}$
as an extension $\lambda^{\mathop{\triangleright}}$ with CSP.

There is much work on dependent types and most of it is affected by the
pioneering work by Martin-Löf [21]. Among many dependent type systems such as
$\lambda^{\Pi}$ [22], The Calculus of Constructions [9], and Edinburgh LF
[15], we base our work on $\lambda\textrm{LF}$ [1] (which is quite close to
$\lambda^{\Pi}$ and Edinburgh LF) due to its simplicity. It is well known that
dependent types are useful to express detailed properties of data structures
at the type level such as the size of data structures [34] and typed abstract
syntax trees [19, 33]. The vector addition discussed in Section 3 is also such
an example.

The use of dependent types for code generation is studied by Chlipala [8] and
Ebner et al. [12]. They use inductive types to guarantee well-formedness of
generated code. Aside from the lack of quasi-quotation, their systems are for
heterogeneous meta-programming and compile-time code generation and they do
not support features for run-time code generation such as run and CSP, as
$\lambda^{\textrm{MD}}$ does.

We discuss earlier attempts at incorporating dependent types into multi-stage
programming. Pasalic and Taha [26] designed $\lambda_{H\circ}$ by introducing
the concept of stage into an existing dependent type system $\lambda_{H}$
[28]. However, $\lambda_{H\circ}$ is equipped with neither run nor CSP.
Forgarty, Pasalic, Siek and Taha [13] extended the type system of MetaOCaml
with indexed types. With this extension, types can be indexed with a Coq term.
Chen and Xi [7] introduced code types augmented with information on types of
free variables in code values in order to prevent code with free variables
from being evaluated. These systems separate the language of type indices from
the term language. As a result, they do not enjoy full-spectrum dependent
types but are technically simpler because there is no need to take stage of
types into account. Brady and Hammond [5] have discussed a combination of
(full-spectrum) dependently typed programming with staging in the style of
MetaOCaml to implement a staged interpreter, which is statically guaranteed to
generate well-typed code. However, they focused on concrete programming
examples and there is no theoretical investigation of the programming language
they used.

Berger and Tratt [4] gave program logic for $\text{Mini-ML}^{\square}_{e}$
[11], which would allow fine-grained reasoning about the behavior of code
generators. However, it cannot manipulate open code which ours can deal with.

##  6 Conclusion

We have proposed a new multi-stage calculus $\lambda^{\textrm{MD}}$ with
dependent types, which make it possible for programmers to express finer-
grained properties about the behavior of code values. The combination leads to
augmentation of almost all judgments in the type system with stage
information. CSP and type equivalence (specially tailored for CSP) are keys to
expressing dependently typed practical code generators. We have proved basic
properties of $\lambda^{\textrm{MD}}$, including preservation, confluence,
strong normalization for full reduction, and progress for staged reduction.

Developing a typechecking algorithm for $\lambda^{\textrm{MD}}$ is left for
future work. We expect that most of the development is straightforward, except
for implicit CSP at the type-level and %-erasing equivalence rules.

### Acknowledgments.

We would like to thank John Toman, Yuki Nishida, and anonymous reviewers for
useful comments.

## References

  * [1] Aspinall, D., Hofmann, M.: Dependent types. In: Pierce, B.C. (ed.) Advanced topics in types and programming languages, chap. 2. MIT press (2005)
  * [2] Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)
  * [3] Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multi-stage programming. In: Federated logic conference (FLoC) satellite workshop on intuitionistic modal logics and applications (IMLA) (1999)
  * [4] Berger, M., Tratt, L.: Program Logics for Homogeneous Generative Run-Time Meta-Programming. Logical Methods in Computer Science Volume 11, Issue 1 (Mar 2015)
  * [5] Brady, E., Hammond, K.: Dependently typed meta-programming. In: Trends in Functional Programming (2006)
  * [6] Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: International Conference on Generative Programming and Component Engineering. pp. 57–76. Springer (2003)
  * [7] Chen, C., Xi, H.: Meta-programming through typeful code representation. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming. pp. 275–286. ICFP ’03, ACM, New York, NY, USA (2003)
  * [8] Chlipala, A.: Ur: Statically-typed metaprogramming with type-level record computation. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 122–133. PLDI ’10, ACM, New York, NY, USA (2010)
  * [9] Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2-3), 95–120 (Feb 1988)
  * [10] Davies, R.: A temporal-logic approach to binding-time analysis. In: Logic in Computer Science, 1996. LICS’96. Proceedings., Eleventh Annual IEEE Symposium on. pp. 184–195. IEEE (1996)
  * [11] Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001)
  * [12] Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. PACMPL 1(ICFP), 34:1–34:29 (2017)
  * [13] Fogarty, S., Pasalic, E., Siek, J., Taha, W.: Concoqtion: Indexed types now! In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation. pp. 112–121. PEPM ’07, ACM, New York, NY, USA (2007)
  * [14] Hanada, Y., Igarashi, A.: On cross-stage persistence in multi-stage programming. In: Codish, M., Sumii, E. (eds.) Functional and Logic Programming. pp. 103–118. Springer International Publishing, Cham (2014)
  * [15] Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM (JACM) 40(1), 143–184 (1993)
  * [16] Kim, I., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003). pp. 257–268 (2006)
  * [17] Kiselyov, O.: Reconciling Abstraction with High Performance: A MetaOCaml approach. NOW Publishing (2018)
  * [18] Kiselyov, O.: The design and implementation of BER metaocaml - system description. In: Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings. pp. 86–102 (2014)
  * [19] Leijen, D., Meijer, E.: Domain specific embedded compilers. In: Proc. of the 2nd Conference on Domain-Specific Languages (DSL ’99). pp. 109–122 (1999)
  * [20] Mainland, G.: Explicitly heterogeneous metaprogramming with metahaskell. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. pp. 311–322. ICFP ’12, ACM, New York, NY, USA (2012)
  * [21] Martin-Löf, P.: An intuitionistic theory of types: Predicative part. Logic Colloquium ’73 80 (01 1973)
  * [22] Meyer, A.R., Reinhold, M.B.: “Type” is not a type. In: Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. pp. 287–295. POPL ’86, ACM, New York, NY, USA (1986)
  * [23] Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348–375 (1978)
  * [24] Moggi, E., Taha, W., Benaissa, Z.E.A., Sheard, T.: An idealized MetaML: Simpler, and more expressive. In: Proc. of European Symposium on Programming (ESOP’99). Lecture Notes in Computer Science, vol. 1576, pp. 193–207 (1999)
  * [25] Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J. Funct. Program. 15(5), 893–939 (2005)
  * [26] Pasalic, E., Taha, W., Sheard, T.: Tagless staged interpreters for typed languages. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming. pp. 218–229. ICFP ’02, ACM, New York, NY, USA (2002)
  * [27] Pierce, B.C.: Types and Programming Languages. MIT Press (2002)
  * [28] Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A type system for certified binaries. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 217–232. POPL ’02, ACM, New York, NY, USA (2002)
  * [29] Taha, W.: A gentle introduction to multi-stage programming, part II. In: Generative and Transformational Techniques in Software Engineering II, International Summer School, GTTSE 2007, Braga, Portugal, July 2-7, 2007. Revised Papers. pp. 260–290 (2007)
  * [30] Taha, W., Nielsen, M.F.: Environment classifiers. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’03). pp. 26–37. ACM, New York, NY, USA (2003)
  * [31] Taha, W., Sheard, T.: MetaML and multi-stage programming with explicit annotations. Theor. Comput. Sci. 248(1-2), 211–242 (Oct 2000)
  * [32] Tsukada, T., Igarashi, A.: A Logical Foundation for Environment Classifiers. Logical Methods in Computer Science 6(4) (Dec 2010)
  * [33] Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proc. of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’03). pp. 224–235 (2003)
  * [34] Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’98). pp. 249–257 (1998)

##  Appendix 0.A Full Definition of $\lambda^{\textrm{MD}}$

###  0.A.1 Syntax

Terms $\displaystyle M,N,L,O,P$ $\displaystyle::=c\mid x\mid\lambda x:\tau.M\
\mid M\ M\mid{\mathop{\blacktriangleright}}_{\alpha}M$ $\displaystyle\ \ \ \
\mid{\mathop{\blacktriangleleft}}_{\alpha}M\mid\Lambda\alpha.M\mid M\ A\mid M\
\varepsilon\mid\%_{\alpha}M$ Types $\displaystyle\tau,\sigma,\rho,\pi,\xi$
$\displaystyle::=X\mid\Pi x:\tau.\tau\mid\tau\
M\mid{\mathop{\triangleright}}_{\alpha}M\mid\forall\alpha.\tau$ Kinds
$\displaystyle K,J,I,H,G$ $\displaystyle::=*\mid\Pi x:\tau.K$ Type
environments $\displaystyle\Gamma$
$\displaystyle::=\emptyset\mid\Gamma,x:\tau@A$ Signature $\displaystyle\Sigma$
$\displaystyle::=\emptyset\mid\Sigma,X::K$ $\displaystyle\ \ \ \
\mid\Sigma,c:\tau$ Stage variables $\displaystyle\alpha,\beta,\gamma,...$
Stage $\displaystyle A,B,C,...$ Variables $\displaystyle x,y,z,...$ Type
variables $\displaystyle X,Y,Z,...$

###  0.A.2 Reduction

$M\longrightarrow N$ Term reduction

$\displaystyle(\lambda x:\tau.M)N\longrightarrow_{\beta}M[x\mapsto N]$
$\displaystyle{\mathop{\blacktriangleleft}}_{\alpha}({\mathop{\blacktriangleright}}_{\alpha}M)\longrightarrow_{\blacklozenge}M$
$\displaystyle(\Lambda\alpha.M)\ A\longrightarrow_{\Lambda}M[\alpha\mapsto A]$

###  0.A.3 Type System

$\vdash\Sigma$ Well-formed signatures

$\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\vdash\emptyset\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\vdash\Sigma\quad\quad\vdash_{\Sigma}K\text{\
kind}@\varepsilon\quad\quad
X\notin\textit{dom}(\Sigma)\end{array}}{\begin{array}[]{@{}c@{}}\vdash\Sigma,X::K\end{array}}$

$\frac{\begin{array}[]{@{}c@{}}\vdash\Sigma\quad\quad\vdash_{\Sigma}\tau::*@\varepsilon\quad\quad
c\notin\textit{dom}(\Sigma)\end{array}}{\begin{array}[]{@{}c@{}}\vdash\Sigma,c:\tau\end{array}}$

$\vdash_{\Sigma}\Gamma$ Well-formed type environments

$\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\Sigma}\emptyset\end{array}}$
$\frac{\begin{array}[]{@{}c@{}}\vdash_{\Sigma}\Gamma\quad\quad\Gamma\vdash_{\Sigma}\tau::*@A\quad\quad
x\notin\textit{dom}(\Sigma)\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\Sigma}\Gamma,x:\tau@A\end{array}}$

$\Gamma\vdash K\text{\ kind}@A$ Well-formed kinds

$\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}*\text{\
kind}@A\end{array}}$ (W-Star)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\quad\quad\Gamma,x:\tau@A\vdash_{\Sigma}K\text{\
kind}@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\Pi
x:\tau.K)\text{\ kind}@A\end{array}}$ (W-Abs)

$\Gamma\vdash_{\Sigma}\tau::K@A$ Kinding

$\frac{\begin{array}[]{@{}c@{}}X::K\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}X::K@A\end{array}}$
(K-TConst)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\quad\quad\Gamma,x:\tau@A\vdash_{\Sigma}\sigma::J@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\Pi
x:\tau.\sigma)::(\Pi x:\tau.J)@A\end{array}}$ (K-Abs)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\sigma::(\Pi
x:\tau.K)@A\quad\quad\Gamma\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\sigma\
M::K[x\mapsto M]@A\end{array}}$ (K-App)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::K@A\quad\quad\Gamma\vdash_{\Sigma}K\equiv
J@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::J@A\end{array}}$
(K-Conv)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\alpha\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\triangleright}}_{\alpha}\tau::*@A\end{array}}$
(K-${\mathop{\triangleright}}$)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::K@A\quad\quad\alpha\notin\rm{FTV}(\Gamma)\cup\rm{FTV}(A)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\forall\alpha.\tau::K@A\end{array}}$
(K-Gen)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::*@A\alpha\end{array}}$
(K-Csp)

$\Gamma\vdash_{\Sigma}M:\tau@A$ Typing

$\frac{\begin{array}[]{@{}c@{}}c:\tau\in\Sigma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}c:\tau@A\end{array}}$
(T-Const)
$\frac{\begin{array}[]{@{}c@{}}x:\tau@A\in\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}x:\tau@A\end{array}}$
(T-Var)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\sigma::*@A\quad\quad\Gamma,x:\sigma@A\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\lambda(x:\sigma).M):(\Pi(x:\sigma).\tau)@A\end{array}}$
(T-Abs)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:(\Pi(x:\sigma).\tau)@A\quad\quad\Gamma\vdash_{\Sigma}N:\sigma@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\
N:\tau[x\mapsto N]@A\end{array}}$ (T-App)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\quad\quad\Gamma\vdash_{\Sigma}\tau\equiv\sigma::K@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\sigma@A\end{array}}$
(T-Conv)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@{A\alpha}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}$
(T-${\mathop{\blacktriangleright}}$)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleleft}}_{\alpha}M:\tau@{A\alpha}\end{array}}$
(T-${\mathop{\blacktriangleleft}}$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\quad\quad\alpha\notin\rm{FTV}(\Gamma)\cup\rm{FTV}(A)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\Lambda\alpha.M:\forall\alpha.\tau@A\end{array}}$
(T-Gen)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\forall\alpha.\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\
A:\tau[\alpha\mapsto A]@A\end{array}}$ (T-Ins)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\%_{\alpha}M:\tau@{A\alpha}\end{array}}$
(T-Csp)

$\Gamma\vdash_{\Sigma}K\equiv J@A$ Kind Equivalence

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A\quad\quad\Gamma,x:\tau@A\vdash_{\Sigma}K\equiv
J@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\Pi
x:\tau.K\equiv\Pi x:\sigma.J@A\end{array}}$ (QK-Abs)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
J@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
J@{A\alpha}\end{array}}$ (QK-Csp)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\text{\
kind}@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
K@A\end{array}}$ (QK-Refl)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
J@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}J\equiv
K@A\end{array}}$ (QK-Sym)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
J@A\quad\quad\Gamma\vdash_{\Sigma}J\equiv
I@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}K\equiv
I@A\end{array}}$ (QK-Trans)

$\Gamma\vdash_{\Sigma}S\equiv T::K@A$ Type Equivalence

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A\quad\quad\Gamma,x:\tau@A\vdash_{\Sigma}\rho\equiv\pi::*@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\Pi
x:\tau.\rho\equiv\Pi x:\sigma.\pi::*@A\end{array}}$ (QT-Abs)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::(\Pi
x:\rho.K)@A\quad\quad\Gamma\vdash_{\Sigma}M\equiv
N:\rho@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\
M\equiv\sigma\ N::K[x\mapsto M]@A\end{array}}$ (QT-App)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@{A\alpha}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\triangleright}}_{\alpha}\tau\equiv{\mathop{\triangleright}}_{\alpha}\sigma::*@A\end{array}}$
(QT-${\mathop{\triangleright}}$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A\quad\quad\alpha\notin\rm{FTV}(\Gamma)\cup\rm{FTV}(A)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\forall\alpha.\tau\equiv\forall\alpha.\sigma::*@A\end{array}}$
(QT-Gen)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@{A\alpha}\end{array}}$
(QT-Csp)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau::K@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\tau::K@A\end{array}}$
(QT-Refl)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::K@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\sigma\equiv\tau::K@A\end{array}}$
(QT-Sym)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::K@A\quad\quad\Gamma\vdash_{\Sigma}\sigma\equiv\rho::K@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\rho::K@A\end{array}}$
(QT-Trans)

$\Gamma\vdash_{\Sigma}M\equiv N:\tau@A$ Term Equivalence

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A\quad\quad\Gamma,x:\tau@A\vdash_{\Sigma}M\equiv
N:\rho@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\lambda
x:\tau.M\equiv\lambda x:\sigma.N:(\Pi x:\tau.\rho)@A\end{array}}$ (Q-Abs)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv L:(\Pi
x:\sigma.\tau)@A\quad\quad\Gamma\vdash_{\Sigma}N\equiv
O:\sigma@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\ N\equiv
L\ O:\tau[x\mapsto N]@A\end{array}}$ (Q-App)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@{A\alpha}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M\equiv{\mathop{\blacktriangleright}}_{\alpha}N:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}$
(Q-${\mathop{\blacktriangleright}}$)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:{\mathop{\triangleright}}_{\alpha}\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleleft}}_{\alpha}M\equiv{\mathop{\blacktriangleleft}}_{\alpha}N:\tau@{A\alpha}\end{array}}$
(Q-${\mathop{\blacktriangleleft}}$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A\quad\quad\alpha\notin\text{FSV}(\Gamma)\cup\text{FSV}(A)\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\Lambda\alpha.M\equiv\Lambda\alpha.N:\forall\alpha.\tau@A\end{array}}$
(Q-Gen)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\forall\alpha.\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\
A\equiv N\ A:\tau[\alpha\mapsto A]@A\end{array}}$ (Q-Ins)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\%_{\alpha}M\equiv\%_{\alpha}N:\tau@{A\alpha}\end{array}}$
(Q-Csp)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
M:\tau@A\end{array}}$ (Q-Refl)
$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}N\equiv
M:\tau@A\end{array}}$ (Q-Sym)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A\quad\quad\Gamma\vdash_{\Sigma}N\equiv
L:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
L:\tau@A\end{array}}$ (Q-Trans)

$\frac{\begin{array}[]{@{}c@{}}\Gamma,x:\sigma@A\vdash_{\Sigma}M:\tau@A\quad\quad\Gamma\vdash_{\Sigma}N:\sigma@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\lambda
x:\sigma.M)\ N\equiv M[x\mapsto N]:\tau[x\mapsto N]@A\end{array}}$ (Q-$\beta$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleleft}}_{\alpha}({\mathop{\blacktriangleright}}_{\alpha}M)\equiv
N:\tau@A\end{array}}$
(Q-${\mathop{\blacktriangleleft}}{\mathop{\blacktriangleright}}$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\Lambda\alpha.M):\forall\alpha.\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}(\Lambda\alpha.M)\
B\equiv M[\alpha\mapsto B]:\tau[\alpha\mapsto B]@A\end{array}}$ (Q-$\Lambda$)

$\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}M:\tau@{A\alpha}\quad\quad\Gamma\vdash_{\Sigma}M:\tau@A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\Sigma}\%_{\alpha}M\equiv
M:\tau@{A\alpha}\end{array}}$ (Q-%)

##  Appendix 0.B Proofs

$\mathcal{J}$ is a metavariable for judgments as in Section 4. We say type
environment $\Gamma$ is a subsequence of type environment $\Delta$ if and only
if we can get $\Gamma$ from $\Delta$ by deleting some or no variables without
changing the order of the remaining elements.

######  Lemma 4 (Weakening)

If $\Gamma\vdash_{\Sigma}\mathcal{J}@A$ and $\Gamma$ is a subsequence of
$\Delta$, then $\Delta\vdash_{\Sigma}J@A$.

###### Proof

By straightforward induction on the derivation of typing, kinding, well-formed
kinding, term equivalence, type equivalence or kind equivalence. We show only
representative cases.

Case W-Abs:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=(\Pi
x:\tau.K)\text{\ kind}@A\\\
\Gamma\vdash_{\Sigma}\tau::*@A&\Gamma,x:\tau@A\vdash_{\Sigma}K\text{\
kind}@A\end{array}$
By the induction hypothesis, we have

$\displaystyle\Delta\vdash_{\Sigma}\tau::*@A$
$\displaystyle\Delta,x:\tau@A\vdash_{\Sigma}K\text{\ kind}@A$

from which $\Delta\vdash_{\Sigma}(\Pi x:\tau.K)\text{\ kind}@A$ follows by
W-Abs.

Case K-Abs:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=(\Pi
x:\tau.)::(\Pi x:\tau.J)@A\\\
\Gamma\vdash_{\Sigma}\tau::*@A&&\Gamma,x:\tau<EMAIL_ADDRESS>
By the induction hypothesis, we have

$\displaystyle\Delta\vdash_{\Sigma}\tau::*@A$
$\displaystyle\Delta,x:\tau@A\vdash_{\Sigma}\sigma::J@A$

from which $\Delta\vdash_{\Sigma}(\Pi x:\tau.)::(\Pi x:\tau.J)@A$ follows.

Case  QT-Abs:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=\rho\equiv\pi::*@A\\\
\Gamma\vdash_{\Sigma}\tau\equiv\sigma::*@A&\Gamma,x:\tau<EMAIL_ADDRESS>
By the induction hypothesis, we have

$\displaystyle\Delta\vdash_{\Sigma}\tau\equiv\sigma::*@A$
$\displaystyle\Delta,x:\tau@A\vdash_{\Sigma}\rho\equiv\pi::*@A$

from which $\Delta\vdash_{\Sigma}\rho\equiv\pi::*@A$ follows. ∎

######  Theorem 0.B.1 (Term Substitution)

If $\Gamma,z:\xi@B,\Delta\vdash_{\Sigma}\mathcal{J}$ and
$\Gamma\vdash_{\Sigma}P:\xi@B$, then $\Gamma,\Delta[z\mapsto
P]\vdash_{\Sigma}\mathcal{J}[z\mapsto P]$. Similarly, if
$\vdash_{\Sigma}\Gamma,z:\xi@B,\Delta$ and $\Gamma\vdash_{\Sigma}P:\xi@B$,
then $\vdash_{\Sigma}\Gamma,\Delta[z\mapsto P]$.

###### Proof

Proved simultaneously by induction on derivations with case analysis on the
last rule used. We show only representative cases.

Case T-Var:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=y:\tau@A\\\
y:\tau@A\in(\Gamma,z:\xi@B,\Delta).\end{array}$

  * •

If $y:\tau@A\in\Gamma$ or $y:\tau@A\in\Delta$, then it is obvious that
$y:\tau[z\mapsto P]@A\in\Gamma$. $\Gamma,\Delta[z\mapsto
P]\vdash_{\Sigma}y[z\mapsto P]:\tau[z\mapsto P]@A$ from T-Var.

  * •

If $y:\tau@A=z:\xi@B$, then $y=z$, $\tau=\xi$, and $A=B$. From the well-
formedness of $\Gamma,z:\xi@B,\Delta$, there is no $z$ in $\xi$. Therefore,
$\tau[z\mapsto P]=\xi[z\mapsto P]=\xi$. It is obvious that $y[z\mapsto
P]=z[z\mapsto P]=P$. Thus, $\Gamma\vdash_{\Sigma}y[z\mapsto P]:\tau[z\mapsto
P]@A$. By Weakening, $\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}y[z\mapsto
P]:\tau[z\mapsto P]@A$

Case W-Abs:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=(\Pi
x:\tau.K)\text{\ kind}@A\\\
\Gamma,z:\xi@B,\Delta\vdash_{\Sigma}\tau::*@A&\Gamma,z:\xi@B,\Delta,x:\tau\vdash_{\Sigma}K\text{\
<EMAIL_ADDRESS>
We can assume $x\neq z$ because we can select fresh $x$ when we construct
$\Pi$ type. By the induction hypothesis,

$\displaystyle\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}\tau[z\mapsto P]::*@A$
$\displaystyle\Gamma,\Delta[z\mapsto P],x:\tau[z\mapsto
P]\vdash_{\Sigma}K[z\mapsto P]\text{\<EMAIL_ADDRESS>
$\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}(\Pi x:\tau[z\mapsto P].K[z\mapsto
P])\text{\ kind}@A$ from W-Abs and it is equivalent to $\Gamma,\Delta[z\mapsto
P]\vdash_{\Sigma}(\Pi x:\tau.K)[z\mapsto P]\text{\ kind}@A$.

Case T-App:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=M\
N:\tau[x\mapsto N]@A\\\
\Gamma,z:\xi@B,\Delta\vdash_{\Sigma}M:\Pi(x:\sigma).\tau@A&\Gamma,z:\xi@B,\Delta\vdash_{\Sigma}N:\sigma@A\end{array}$
We can assume $x\neq z$ because we can select fresh $x$ when we construct
$\Pi$ type. By the induction hypothesis,

$\displaystyle\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}M[z\mapsto
P]:(\Pi(x:\sigma).\tau)[z\mapsto P]@A$ $\displaystyle\Gamma,\Delta[z\mapsto
P]\vdash_{\Sigma}N[z\mapsto P]:\sigma[z\mapsto<EMAIL_ADDRESS>
and $\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}M[z\mapsto
P]:(\Pi(x:\sigma).\tau)[z\mapsto P]@A$ is equivalent to
$\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}M[z\mapsto P]:(\Pi(x:\sigma[z\mapsto
P]).\tau[z\mapsto P])@A$. From T-App, $\Gamma,\Delta[z\mapsto P](M[z\mapsto
P]\ N[z\mapsto P]):\tau[z\mapsto P][x\mapsto N[z\mapsto P]]@A$ and this is
equivalent to $\Gamma,\Delta[z\mapsto P]\vdash_{\Sigma}(M\ N)[z\mapsto
P]:\tau[x\mapsto N][z\mapsto P]@A$. ∎

######  Lemma 5 (Stage Substitution)

If $\Gamma\vdash_{\Sigma}\mathcal{J}$, then $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}\mathcal{J}[\beta\mapsto B]$. Similarly, if
$\vdash_{\Sigma}\Gamma$, then $\vdash_{\Sigma}\Gamma[\beta\mapsto B]$.

###### Proof

Proved simultaneously by induction on derivations with case analysis on the
last rule used. We show only representative cases.

Case T-Gen:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=\Lambda\alpha.M:\forall\alpha.\tau@A\\\
\Gamma\vdash_{\Sigma}M:\tau@A&\alpha\notin\rm{FTV}(\Gamma)\cup\rm{FTV}(A).\end{array}$
We can assume $\alpha\notin B$ because $\alpha$ is a bound variable. By the
induction hypothesis, we have $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}M[\beta\mapsto B]:\tau[\beta\mapsto B]@A$. We can prove
easily $\alpha\notin\text{FSV}(\Gamma[\beta\mapsto B])\cup\text{FSV}(A)$.
Then, $\Gamma[\beta\mapsto B]\vdash_{\Sigma}(\Lambda\alpha.M)[\beta\mapsto
B]:(\forall\alpha.\tau)[\beta\mapsto B]@A[\beta\mapsto B]$ by T-Gen.

Case K-${\mathop{\triangleright}}$:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=\Gamma\vdash_{\Sigma}{\mathop{\triangleright}}_{\alpha}\tau::*@A\\\
<EMAIL_ADDRESS>

  * •

If $\alpha\neq\beta$,
$\Gamma[\beta\mapsto B]\vdash_{\Sigma}\tau[\beta\mapsto B]::*[\beta\mapsto
B]@A\alpha[\beta\mapsto B]$ from the induction hypothesis.
$\Gamma[\beta\mapsto
B]\vdash_{\Sigma}{\mathop{\triangleright}}_{\alpha}\tau[\beta\mapsto
B]::*[\beta\mapsto B]@A[\beta\mapsto B]$ from K-${\mathop{\triangleright}}$.

  * •

If $\alpha=\beta$,
$\Gamma[\beta\mapsto B]\vdash_{\Sigma}\tau[\beta\mapsto B]::*[\beta\mapsto
B]@A\alpha[\beta\mapsto B]$ from the induction hypothesis and it is identical
to $\Gamma[\beta\mapsto B]\vdash_{\Sigma}\tau[\beta\mapsto B]::*@AB$. We can
get $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}{\mathop{\triangleright}}_{B}\tau[\beta\mapsto B]::*@A$ after
repeatedly using K-${\mathop{\triangleright}}$.

Case Q-Gen:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathcal{J}=\Lambda\alpha.M\equiv\Lambda\alpha.N:\forall\alpha.\tau@A\\\
\Gamma\vdash_{\Sigma}M\equiv
N:\tau@A&\alpha\notin\text{FSV}(\Gamma)\cup\text{FSV}(A).\end{array}$
From the induction hypothesis, $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}M[\beta\mapsto B]\equiv N[\beta\mapsto B]:\tau[\beta\mapsto
B]@A[\beta\mapsto B]$. We can assume $\alpha\notin B$ because $\alpha$ is a
bound variable. Thus, $\alpha\notin\text{FSV}(\Gamma[\beta\mapsto
B])\cup\text{FSV}(A[\beta\mapsto B])$. $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}\Lambda\alpha.M[\beta\mapsto
B]\equiv\Lambda\alpha.N[\beta\mapsto B]:\tau[\beta\mapsto B]@A[\beta\mapsto
B]$ from Q-Gen and it is identical to $\Gamma[\beta\mapsto
B]\vdash_{\Sigma}(\Lambda\alpha.M)[\beta\mapsto
B]\equiv(\Lambda\alpha.N)[\beta\mapsto B]:\tau[\beta\mapsto B]@A[\beta\mapsto
B]$. ∎

######  Lemma 6 (Agreement)

  1. 1.

If $\Gamma\vdash_{\Sigma}\tau::K@A$, then $\Gamma\vdash_{\Sigma}K\text{\
kind}@A$.

  2. 2.

If $\Gamma\vdash_{\Sigma}M:\tau@A$, then $\Gamma\vdash_{\Sigma}\tau::*@A$.

  3. 3.

If $\Gamma\vdash_{\Sigma}K\equiv J@A$, then $\Gamma\vdash_{\Sigma}K\text{\
kind}@A$ and $\Gamma\vdash_{\Sigma}J\text{\ kind}@A$.

  4. 4.

If $\Gamma\vdash_{\Sigma}\tau\equiv\sigma::K@A$, then
$\Gamma\vdash_{\Sigma}\tau::K@A$ and $\Gamma\vdash_{\Sigma}\sigma::K@A$.

  5. 5.

If $\Gamma\vdash_{\Sigma}M\equiv N:\tau@A$, then
$\Gamma\vdash_{\Sigma}M:\tau@A$ and $\Gamma\vdash_{\Sigma}N:\tau@A$.

###### Proof

We can prove using induction on the derivation tree. We show some cases as
examples.

Case K-Csp:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}K::*@A\alpha\text{
is derived from<EMAIL_ADDRESS>
By W-Star, $\Gamma\vdash_{\Sigma}*\text{\ kind}@A\alpha$.

Case T-Csp:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}\%_{\alpha}M::\tau@A\alpha\text{
is derived from }\Gamma\vdash_{\Sigma}M::\tau@A\end{array}$
By the induction hypothesis, $\Gamma\vdash_{\Sigma}\tau::*@A$. By K-Csp,
$\Gamma\vdash_{\Sigma}\tau::*@A\alpha$.

Case Q-$\beta$:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}(\lambda
x:\sigma.M)\ N\equiv M[x\mapsto N]:\tau[x\mapsto N]@A\text{ is derived from
}\\\ \Gamma,x:\sigma@A\vdash_{\Sigma}M:\tau@A\text{ and
<EMAIL_ADDRESS>
From T-Abs and T-App, $\Gamma\vdash_{\Sigma}(\lambda x:\sigma.M)\
N:\tau[x\mapsto N]@A$. From Term Substitution,
$\Gamma\vdash_{\Sigma}M[x\mapsto N]:\tau[x\mapsto N]@A$. ∎

As we said in Section 4, we generalize Inversion Lemma to use induction.

######  Lemma 7 (Inversion Lemma for $\Pi$ Type)

  1. 1.

If $\Gamma\vdash_{\Sigma}(\lambda x:\sigma.M):\rho$, then there are
$\sigma^{\prime}$ and $\tau^{\prime}$ such that $\rho=\Pi
x:\sigma^{\prime}.\tau^{\prime}$,
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}@A$ and
$\Gamma,x:\sigma^{\prime}@A\vdash_{\Sigma}M:\tau^{\prime}@A$.

  2. 2.

If $\Gamma\vdash_{\Sigma}\rho\equiv(\Pi x:\sigma.\tau):K@A$, then there are
$\sigma^{\prime},\tau^{\prime},K$, and $J$ such that $\rho=\Pi
x:\sigma^{\prime}.\tau^{\prime}$,
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}:K@A$, and
$\Gamma,x:\sigma@A\vdash_{\Sigma}\tau\equiv\tau^{\prime}:J@A$.

  3. 3.

If $\Gamma\vdash_{\Sigma}(\Pi x:\sigma.\tau)\equiv\rho:K@A$, then there are
$\sigma^{\prime},\tau^{\prime},K$, and $J$ such that $\rho=\Pi
x:\sigma^{\prime}.\tau^{\prime}$,
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}:K@A$, and
$\Gamma,x:\sigma@A\vdash_{\Sigma}\tau\equiv\tau^{\prime}:J@A$.

###### Proof

We can prove using induction on the derivation tree. We show a few main cases.

Case T-Abs:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}\sigma::*@A\text{
and }\Gamma,x:\sigma<EMAIL_ADDRESS>
We can take $\sigma$ and $\tau$ as $\sigma^{\prime}$ and $\tau^{\prime}$ in
the statement.

Case T-Conv:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}(\lambda
x:\sigma.M):\rho@A\text{ and }\Gamma\vdash_{\Sigma}\rho\equiv(\Pi
<EMAIL_ADDRESS>
There are $\sigma^{\prime}$ and $\tau^{\prime}$ such that $\rho=\Pi
x:\sigma^{\prime}.\tau^{\prime}$,
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}@A$ and
$\Gamma,x:\sigma^{\prime}@A\vdash_{\Sigma}M:\tau^{\prime}@A$ by the induction
hypothesis.

Case QT-Refl:
There two cases for the conclusion.

  * •

If $\Gamma\vdash_{\Sigma}\rho\equiv(\Pi x:\sigma.\tau):K@A$, we can use the
third statement of the lemma as the induction hypothesis.

  * •

If $\Gamma\vdash_{\Sigma}(\Pi x:\sigma.\tau)\equiv\rho:K@A$, we can use the
second statement of the lemma as the induction hypothesis.

∎

######  Lemma 8 (Inversion Lemma for ${\mathop{\triangleright}}$ type)

If $\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M:\tau@A$,
then there is $\sigma$ such that
$\tau={\mathop{\triangleright}}_{\alpha}\sigma$ and
$\Gamma\vdash_{\Sigma}M:\sigma@A$.

If
$\Gamma\vdash_{\Sigma}\rho\equiv{\mathop{\triangleright}}_{\alpha}\tau:K@A$,
then there are $\tau^{\prime},K$, and $J$ such that
$\rho={\mathop{\triangleright}}_{\alpha}\tau^{\prime}$ and
$\Gamma\vdash_{\Sigma}\tau\equiv\tau^{\prime}:K@A$.

If
$\Gamma\vdash_{\Sigma}{\mathop{\triangleright}}_{\alpha}\tau\equiv\rho:K@A$,
then there are $\tau^{\prime},K$, and $J$ such that
$\rho={\mathop{\triangleright}}_{\alpha}\tau^{\prime}$ and
$\Gamma\vdash_{\Sigma}\tau\equiv\tau^{\prime}:K@A$.

###### Proof

We can prove using induction on the derivation tree. We show some cases as
examples.

Case T-${\mathop{\blacktriangleright}}$:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l<EMAIL_ADDRESS>
We can take $\sigma^{\prime}$ as $\sigma$.

Case T-Conv:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M:\tau^{\prime}@A\text{
and<EMAIL_ADDRESS>
There is $\sigma$ such that
$\tau^{\prime}={\mathop{\triangleright}}_{\alpha}\sigma$ and
$\Gamma\vdash_{\Sigma}M:\sigma@A$ by using the induction hypothesis to
$\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}_{\alpha}M:\tau^{\prime}@A$.
There are $\sigma^{\prime}$ and $K^{\prime}$ such that
$\tau={\mathop{\triangleright}}_{\alpha}\sigma^{\prime}$ and
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}:K@A$ by using the induction
hypothesis to
$\Gamma\vdash_{\Sigma}{\mathop{\triangleright}}_{\alpha}\sigma:\tau::K^{\prime}@A$.
Finally, $\Gamma\vdash_{\Sigma}M:\sigma^{\prime}@A$ by T-Conv. ∎

######  Lemma 9 (Inversion for $\Lambda$ Type)

If $\Gamma\vdash_{\Sigma}\Lambda\alpha.M:\tau$, then there is $\sigma$ such
that $\sigma=\forall\alpha.\sigma$ and $\Gamma\vdash_{\Sigma}M:\sigma@A$.

If $\Gamma\vdash_{\Sigma}\rho\equiv\forall\alpha.\tau:K@A$, then there are
$\tau^{\prime},K$ such that $\rho=\forall\alpha.\tau^{\prime}$ and
$\Gamma\vdash_{\Sigma}\tau\equiv\tau^{\prime}:K@A$.

If $\Gamma\vdash_{\Sigma}\forall\alpha.\tau\equiv\rho:K@A$, then there are
$\tau^{\prime},K$ such that $\rho=\forall\alpha.\tau^{\prime}$ and
$\Gamma\vdash_{\Sigma}\tau\equiv\tau^{\prime}:K@A$.

###### Proof

We can prove using induction on the derivation tree.

∎

######  Lemma 10 (Inversion Lemma for Application)

If $\Gamma\vdash_{\Sigma}(\lambda x:\sigma.M)\ N:\tau@A$ then there are $x$
and $\rho$ such that $\Gamma,x:\sigma\vdash_{\Sigma}M:\rho@A$ and
$\Gamma\vdash_{\Sigma}N:\sigma@A$.

###### Proof

We can prove using induction on the derivation tree. ∎

######  Theorem 0.B.2 (Preservation for $\beta$-Reduction)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow_{\beta}M^{\prime}$,
then $\Gamma\vdash_{\Sigma}M^{\prime}:\tau@A$.

###### Proof

We can prove using induction on the type derivation tree. We show some cases
as examples.

Case T-App:
The shape of the reduction is one of following three.

  * •

$(\lambda x:\sigma.N)\ L\longrightarrow_{\beta}N[x\mapsto L]$.
Because the last rule of the type derivation tree is T-App, we have
$\Gamma\vdash_{\Sigma}(\lambda x:\sigma.N):(\Pi
x:\sigma^{\prime}.\tau^{\prime})@A$ and
$\Gamma\vdash_{\Sigma}L:\sigma^{\prime}@A$. By using Inversion Lemma for $\Pi$
type to $\Gamma\vdash_{\Sigma}(\lambda x:\sigma.N):(\Pi
x:\sigma^{\prime}.\tau^{\prime})@A$, we get
$\Gamma,x:\sigma\vdash_{\Sigma}N:\tau$ and
$\Gamma\vdash_{\Sigma}\sigma\equiv\sigma^{\prime}$ and
$\Gamma,x:\sigma\vdash_{\Sigma}\tau\equiv\tau^{\prime}@A$. By T-Conv,
$\Gamma\vdash_{\Sigma}L:\sigma@A$. By Term Substitution Lemma, we get
$\Gamma\vdash_{\Sigma}N[x\mapsto L]:\tau[x\mapsto L]$.

  * •

$M\ N\longrightarrow_{\beta}M^{\prime}\ N$.
From the induction hypothesis and T-App, the type is preserved for the
reduction.

  * •

$M\ N\longrightarrow_{\beta}M\ N^{\prime}$.
From the induction hypothesis and T-App, the type is preserved for the
reduction.

∎

######  Theorem 0.B.3 (Preservation for Term on $\blacklozenge$-Reduction)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow_{\blacklozenge}N$,
then $\Gamma\vdash_{\Sigma}N:\tau@A$

###### Proof

We can prove using induction on the type derivation tree. We show the case of
T-${\mathop{\blacktriangleleft}}$ as examples. Other cases are easy.

Case T-${\mathop{\blacktriangleleft}}$:
There are two cases for $\longrightarrow_{\blacklozenge}$.

  * •

${\mathop{\blacktriangleleft}}{\mathop{\blacktriangleright}}M\longrightarrow_{\blacklozenge}M$.
Because the last rule is T-${\mathop{\blacktriangleleft}}$, we have
$\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}M:{\mathop{\triangleright}}_{\alpha}\tau@A$.
By using Inversion Lemma for ${\mathop{\triangleright}}$ type to
$\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleright}}M:{\mathop{\triangleright}}_{\alpha}\tau@A$,
we get $\Gamma\vdash_{\Sigma}M:\tau@A$

  * •

${\mathop{\blacktriangleleft}}M\longrightarrow_{\blacklozenge}{\mathop{\blacktriangleleft}}M^{\prime}$.
We can use the induction hypothesis and T-${\mathop{\blacktriangleleft}}$.

∎

######  Theorem 0.B.4 (Preservation for Term on $\Lambda$ Reduction)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow_{\Lambda}N$, then
$\Gamma\vdash_{\Sigma}N:\tau@A$.

###### Proof

We can prove using induction on the type derivation tree. We show the case of
T-Ins as examples. Other cases are easy.

Case T-Ins:
There are two cases $\longrightarrow_{\Lambda}$.

  * •

$(\Lambda\alpha.M)\ B\longrightarrow_{\Lambda}M[\alpha\mapsto B]$
Because the last rule is T-Ins, we have $\Gamma\vdash_{\Sigma}\Lambda\alpha.M\
:\forall\alpha.\tau@A$. By using Inversion Lemma for $\Lambda$ type to
$\Gamma\vdash_{\Sigma}\Lambda\alpha.M\ :\forall\alpha.\tau@A$, we obtain
$\Gamma\vdash_{\Sigma}M:\tau@A$. By using Stage Substitution Lemma to
$\Gamma\vdash_{\Sigma}M:\tau@A$, we obtain $\Gamma[\alpha\mapsto
B]\vdash_{\Sigma}M[\alpha\mapsto B]:\tau[\alpha\mapsto B]@A[\alpha\mapsto B]$.
$\alpha$ is a bound variable therefore we can assume
$\alpha\notin\text{FSV}(\Gamma)\cup\text{FSV}(A)$. So, we can rewrite
$\Gamma[\alpha\mapsto B]\vdash_{\Sigma}M[\alpha\mapsto B]:\tau[\alpha\mapsto
B]@A[\alpha\mapsto B]$ to $\Gamma\vdash_{\Sigma}M[\alpha\mapsto
B]:\tau[\alpha\mapsto B]@A$.

  * •

$M\ B\longrightarrow_{\Lambda}M^{\prime}\ B$
By the induction hypothesis and T-Ins.

∎

######  Definition 1 ($\natural$ translation)

The $\natural$ translation is a translation from $\lambda^{\text{MD}}$ to
$\lambda^{\to}$.

  * •

Term

$\displaystyle\natural(x)$ $\displaystyle=x$ $\displaystyle\natural(\lambda
x:\tau.M)$ $\displaystyle=\lambda x:\natural(\tau).\natural(M)$
$\displaystyle\natural(M\ N)$ $\displaystyle=\natural(M)\ \natural(N)$
$\displaystyle\natural({\mathop{\blacktriangleright}}_{\alpha}M)$
$\displaystyle=\natural(M)$
$\displaystyle\natural({\mathop{\blacktriangleleft}}_{\alpha}M)$
$\displaystyle=\natural(M)$ $\displaystyle\natural(\Lambda\alpha.M)$
$\displaystyle=\natural(M)$ $\displaystyle\natural(M\ B)$
$\displaystyle=\natural(M)$

  * •

Type

$\displaystyle\natural(X)$ $\displaystyle=X$ $\displaystyle\natural(\Pi
x:\tau.\sigma)$ $\displaystyle=\natural(\tau)\to\natural(\sigma)$
$\displaystyle\natural(\tau\ x)$ $\displaystyle=\natural(\tau)$
$\displaystyle\natural({\mathop{\triangleright}}_{\alpha}\tau)$
$\displaystyle=\natural(\tau)$ $\displaystyle\natural(\forall\alpha.\tau)$
$\displaystyle=\natural(\tau)$

  * •

Kind

$\displaystyle\natural(K)$ $\displaystyle=*$

  * •

Context

$\displaystyle\natural(\phi)$ $\displaystyle=\phi$
$\displaystyle\natural(\Gamma,x:T@A)$
$\displaystyle=\natural(\Gamma),\natural(x):\natural(\tau)$
$\displaystyle\natural(\Gamma,X:K@A)$ $\displaystyle=\natural(\Gamma)$

######  Lemma 11 (Preservation of Equality in $\natural$)

If $\Gamma\vdash_{\Sigma}\tau\equiv\sigma@A$ then
$\natural(\tau)=\natural(\sigma)$.

###### Proof

We can prove using induction on the type derivation tree. ∎

######  Lemma 12 (Preservation of Typing in $\natural$)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ in $\lambda^{\text{MD}}$ then
$\natural(\Gamma)\vdash_{\Sigma}\natural(M):\natural(\tau)$ in
$\lambda^{\to}$.

###### Proof

We can prove using induction on the type derivation tree. We show the case of
T-App and T-Conv as examples. Other cases are easy.

Case T-App:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}M:(\Pi(x:\sigma).\tau)@A\text{
and }\Gamma\vdash_{\Sigma}N:\sigma@A\end{array}$
From the induction hypothesis, we have
$\natural(\Gamma)\vdash_{\Sigma}\natural(M):\natural(\sigma)\to\natural(\tau)$
and $\natural(\Gamma)\vdash_{\Sigma}\natural(N):\natural(\sigma)$. Use the
Application rule in $\lambda^{\to}$, we get
$\natural(\Gamma)\vdash_{\Sigma}\natural(M)\ \natural(N):\natural(\tau)$.
Because $\natural(M)\ \natural(N)=\natural(M\ N)$ from the definition of
$\natural$, $\natural(\Gamma)\vdash_{\Sigma}\natural(M\ N):\natural(\tau)$ in
$\lambda^{\to}$.

Case T-Conv:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}M:\tau@A\text{
and }\Gamma\vdash_{\Sigma}\tau\equiv\sigma@A\end{array}$
By using Preservation of typing in $\natural$ to
$\Gamma\vdash_{\Sigma}\tau\equiv\sigma@A$, we get
$\natural(\tau)=\natural(\sigma)$.
$\natural(\Gamma)\vdash_{\Sigma}\natural(M):\natural(\tau)$ from the induction
hypothesis. Then,
$\natural(\Gamma)\vdash_{\Sigma}\natural(M):\natural(\sigma)$. ∎

######  Lemma 13 (Preservation of Substitution in $\natural$)

If $\Gamma,x:\sigma\vdash_{\Sigma}M:\tau@A$ and
$\Gamma\vdash_{\Sigma}N:\sigma@A$ in $\lambda^{\text{MD}}$ then
$\natural(M[x\mapsto N])$ = $\natural(M)[x\mapsto\natural(N)]$

###### Proof

We prove by induction on the type derivation tree of
$\Gamma,x:\sigma\vdash_{\Sigma}M:\tau@A$. ∎

######  Lemma 14 (Preservation of $\beta$-Reduction in $\natural$)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow_{\beta}N$ in
$\lambda^{\text{MD}}$ then
$\natural(M)\longrightarrow_{\beta}^{+}\natural(N)$.

###### Proof

We prove by induction on the derivation of $\beta$ reduction of
$\lambda^{\textrm{MD}}$. We show only the main case.

Case $(\lambda x:\tau.M)\ N\longrightarrow_{\beta}M[x\mapsto N]$:
From the definition of $\natural$, $\natural((\lambda x:\tau.M)\ N)$ =
$\lambda x:\natural(\tau).\natural(M)\ \natural(N)$. Because $\lambda
x:\natural(\tau).\natural(M)\ \natural(N)$ is a typed term in $\lambda^{\to}$,
we can do $\beta$ reduction from it. As a result of the reduction, we get
$\natural(M)[x\mapsto\natural(N)]$. From Preservation of substitution in
$\natural$, $\natural(M[x\mapsto N])$ = $\natural(M)[x\mapsto\natural(N)]$. ∎

######  Lemma 15 (Preservation of $\Lambda$-Reduction in $\natural$)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow_{\beta}N$ in
$\lambda^{\text{MD}}$ then $\natural(M)$ = $\natural(N)$.

###### Proof

We prove by induction on the derivation of $\Lambda$-reduction of
$\lambda^{\textrm{MD}}$. We show only the main case.

  * •

Case $(\Lambda\alpha.M)\ A\longrightarrow_{\Lambda}M[\alpha\mapsto A]$.
By the definition of $\natural$, $\natural((\Lambda\alpha.M)\ A)=\natural(M)$.
Because $\natural(M)$ does not contain $\alpha$, $\natural(M[\alpha\mapsto
A])=\natural(M)$.

∎

######  Lemma 16 (Preservation of $\blacklozenge$-Reduction in $\natural$)

If $\Gamma\vdash_{\Sigma}M:\tau@A$ and $M\longrightarrow_{\blacklozenge}N$ in
$\lambda^{\text{MD}}$ then $\natural(M)$ = $\natural(N)$.

###### Proof

We prove by induction on the derivation of $\blacklozenge$-reduction of
$\lambda^{\textrm{MD}}$. We show only the main case.

  * •

Case
${\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}M\longrightarrow_{\blacklozenge}M$.
By the definition of $\natural$,
$\natural({\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}M)=\natural(M)$.

∎

######  Theorem 0.B.5 (Strong Normalization)

If $\Gamma\vdash_{\Sigma}^{A}t:T$ then there is no infinite sequence of terms
$(t_{i})_{i\geq 1}$ and
$t_{i}\longrightarrow_{\beta,{\mathop{\blacktriangleleft}}{\mathop{\blacktriangleright}},\Lambda}t_{i+1}$
for $i\geq 1$

###### Proof

If there is an infinite reduction sequence in $\lambda^{\text{MD}}$ then there
are infinite beta reductions in the sequence. This is because reductions other
than $\beta$-reduction reduce the size of a term.

Then, we show Strong Normalization by proof by contradiction. We assume that
there is an infinite reduction in a typed $\lambda^{\textrm{MD}}$ from typed
term $M$. We can construct a typed term of simply typed lambda calculus
$\natural(M)$ from Preservation of Typing in $\natural$ and $\natural(M)$ has
infinite reductions from Preservation of Reduction in $\natural$. However,
$\lambda^{\to}$ has a property of Strong Normalization, so there is no
infinite reductions. ∎

######  Theorem 0.B.6 (Confluence(Church-Rosser Property))

Define $M\longrightarrow N$ as $M\longrightarrow_{\beta}N$ or
$M\longrightarrow_{\blacklozenge}N$ or $M\longrightarrow_{\Lambda}N$. For any
term $M$, if $M\longrightarrow^{*}N$ and $M\longrightarrow^{*}L$, there exists
$O$ that satisfies $N\longrightarrow^{*}O$ and $L\longrightarrow^{*}O$.

###### Proof

Because we show the Strong Normalization of $\lambda^{\text{MD}}$, we can use
Newman’s lemma to prove Church-Rosser Property of $\lambda^{\text{MD}}$. Then,
what we must show is Weak Church-Rosser Property.

When we consider two different redexes in a $\lambda^{\text{MD}}$ term, they
can only be disjoint, or one is a part of the other. In short, they never
overlap each other. So, we can reduce one of them after we reduce another. ∎

######  Lemma 17 (Unique Decomposition)

If $\Gamma$ does not have any variable declared at stage $\varepsilon$ and
$\Gamma\vdash_{\Sigma}M:\tau@A$, then either

  1. 1.

$M\in V^{A}$, or

  2. 2.

$M$ can be uniquely decomposed into an evaluation context and a redex, that
is, there uniquely exist $B,E^{A}_{B}$, and $R^{B}$ such that
$M=E^{A}_{B}[R^{B}]$.

###### Proof

We prove by induction on the type derivation tree of
$\Gamma\vdash_{\Sigma}M:\tau@A$.

Case T-Var:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}x:\tau@A\text{
is the root of the type derivation tree. }\end{array}$
We can assume $A\neq\varepsilon$ because $x:\tau@\varepsilon\notin\Gamma$.
Then, $x\in V^{A}$.

Case T-${\mathop{\blacktriangleleft}}$:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}{\mathop{\blacktriangleleft}}_{\alpha}M:\tau@A\alpha\text{
is derived from
<EMAIL_ADDRESS>
From the induction hypothesis, one of the following holds.

  1. 1.

$M\in V^{A}$.

  2. 2.

There is an unique triple of $(B,E^{A}_{B},R^{B})$ such that ($B=\varepsilon$
or $B=\beta$) and $M=E^{A}_{B}[R^{B}]$.

  * •

If $M\in V^{A}$ is true

    * –

and $A=\varepsilon$, then
$M={\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}$ from Inversion Lemma and
${\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}v^{\alpha}=E^{\alpha}_{\alpha}[R^{\alpha}]$.

    * –

and $A\neq\varepsilon$, then
${\mathop{\blacktriangleleft}}_{\alpha}v^{A}\in V^{A\alpha}$.

  * •

If there is an unique triple of $(B,E^{A}_{B},R^{B})$ such that
($B=\varepsilon$ or $B=\beta$) and $M=E^{A}_{B}[R^{B}]$

    * –

and $M={\mathop{\blacktriangleright}}_{\alpha}E^{\alpha}_{B}[R^{B}]$, then
${\mathop{\blacktriangleleft}}_{\alpha}{\mathop{\blacktriangleright}}_{\alpha}E^{\alpha}_{B}[R^{B}]\longrightarrow_{s}E^{\alpha}_{B}[R^{B}]$
doesn’t hold because $E^{\alpha}_{B}[R^{B}]\notin v^{\alpha}$. So, given
$B,E^{A}_{B},R^{B}$ are the unique tuples satisfies the condition.

    * –

Otherwise,
It is obvious from the induction hypothesis and the definition of $E^{A}_{B}$.

Case T-Ins:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\vdash_{\Sigma}M\
C:\tau[\alpha\mapsto C]@A\\\ \text{ is derived from
<EMAIL_ADDRESS>

  * •

If $A=\varepsilon$,
By the induction hypothesis, either

    1. 1.

$M\in V^{\varepsilon}$ or

    2. 2.

there is a unique triple of $(B,E^{\varepsilon}_{B},R^{B})$ such that
($B=\varepsilon$ or $B=\beta$) and $M=E^{\varepsilon}_{B}[R^{B}]$.

    * –

If $M\in V^{\varepsilon}$,
$M=\Lambda\alpha.v^{\varepsilon}$ from Inversion Lemma. Thus,
$\Lambda\alpha.v^{\varepsilon}\
C=E^{\varepsilon}_{\varepsilon}[R^{\varepsilon}]$

    * –

If there is an unique triple of $(B,E^{\varepsilon}_{B},R^{B})$ such that
($B=\varepsilon$ or $B=\beta$) and $M=E^{\varepsilon}_{B}[R^{B}]$, we can
decompose $E^{\varepsilon}_{B}[R^{B}]\ B$ uniquely because
$E^{\varepsilon}_{B}[R^{B}]\neq\Lambda\alpha.v^{\varepsilon}$,

  * •

If $A\neq\varepsilon$,
By the induction hypothesis, either

    1. 1.

$M\in V^{A}$ or

    2. 2.

there is a unique triple of $(B,E^{A}_{B},R^{B})$ such that ($B=\varepsilon$
or $B=\beta$) and $M=E^{A}_{B}[R^{B}]$.

    * –

If $M\in V^{A}$, it is clear that $v^{A}\ C\in V^{A}$.

    * –

If there are an unique triple of $(B,E^{A}_{B},R^{B})$ such that
($B=\varepsilon$ or $B=\beta$) and $M=E^{A}_{B}[R^{B}]$, we can decompose
$E^{A}_{B}[R^{B}]\ C$ uniquely because we cannot $\Lambda$ reduction at stage
$A$.

∎

######  Corollary 2 (Progress)

If $x:\tau@\varepsilon\notin\Gamma$ and $\Gamma\vdash_{\Sigma}M:\tau@A$ then
$M\in V^{A}$ or there is $M^{\prime}$ such that $M\longrightarrow M^{\prime}$.

###### Proof

Immediate from Unique Decomposition. ∎