# A Categorical Normalization Proof for the Modal Lambda-Calculus

Jason Z. S. Hu  Brigitte Pientka  School of Computer Science
McGill University
Montréal, QC, Canada

###### Abstract

We investigate a simply typed modal $\lambda$-calculus,
$\lambda^{\to\square}$, due to Pfenning, Wong and Davies, where we define a
well-typed term with respect to a context stack that captures the possible
world semantics in a syntactic way. It provides logical foundation for multi-
staged meta-programming. Our main contribution in this paper is a
normalization by evaluation (NbE) algorithm for $\lambda^{\to\square}$ which
we prove sound and complete. The NbE algorithm is a moderate extension to the
standard presheaf model of simply typed $\lambda$-calculus. However, central
to the model construction and the NbE algorithm is the observation of _Kripke-
style substitutions_ on context stacks which brings together two previously
separate concepts, structural modal transformations on context stacks and
substitutions for individual assumptions. Moreover, Kripke-style substitutions
allow us to give a formulation for contextual types, which can represent open
code in a meta-programming setting. Our work lays the foundation for extending
the logical foundation by Pfenning, Wong, and Davies towards building a
practical, dependently typed foundation for meta-programming.

###### keywords:

modal $\lambda$-calculus, normalization by evaluation, presheaf model,
contextual types

††volume: NN††journal: Electronic Notes in Theoretical Informatics and
Computer Science

and ††thanks: Email<EMAIL_ADDRESS>
††thanks: Email<EMAIL_ADDRESS>
##  1 Introduction

The Curry-Howard correspondence fundamentally connects formulas and proofs to
types and programs. This view not only provides logical explanations for
computational phenomena, but also serves as a guiding principle in designing
type theories and programming languages.

Extending the Curry-Howard correspondence to modal logic has been fraught with
challenges. One of the first such calculi for the modal logic S4 were proposed
by Bierman and de Paiva [7, 8] and subsequently by Pfenning and Davies [34]. A
key characteristic of this work is to separate the assumptions that are valid
in every world from the assumptions that presently hold in the current world.
This leads to a dual-context style formulation that satisfies substitution
properties (see for example [17]).

In recent years, modal type systems based on this dual-context style have
received renewed attention and provided insights into a wide range of
seemingly unconnected areas: from reasoning about universes in homotopy type
theory [30, 38] to mechanizing meta-theory [36, 37], to reasoning about
effects [40], and meta-programming [27]. This line of work builds on the dual-
context formulation of Pfenning and Davies. However, due to the permutation
conversions it is also challenging to extend to dependent type theories and
directly prove normalization via logical relations. An alternative to dual-
context-style modal calculi is pursued by Clouston, Birkedal and collaborators
(see [13, 23]). This line of work is inspired by the Fitch-style proof
representation given by Borghuis [12]. Following Borghuis they have been
calling their representation the Fitch style. Fitch-style systems model Kripke
semantics [29] and use locks to manage assumptions in a context. To date,
existing formulations of $S4$ in Fitch style [13, 23] mainly considers
idempotency where $\square T$ is isomorphic to $\square\square T$. However,
this distinction is important from a computational view. For example, in
multi-staged programming (see [34, 15]) $\square T$ describes code generated
in one stage, while $\square\square T$ denotes code generated in two stages.
It is also fruitful to keep the distinction from a theoretical point of view,
as it allows for a fine grained study of different, related modal logics.

In this paper, we take $\lambda^{\to\square}$, an intuitionistic version of
modal logic $S4$, from Pfenning, Wong and Davies [35, 15] as a starting point.
Historically, $\lambda^{\to\square}$ is also motivated by Kripke semantics
[29] (see [14, Section 3] and [15, Section 4]) and is hence referred to as the
Kripke style. Unlike Fitch-style systems where worlds are represented by
segments between two adjacent “lock” symbols, in $\lambda^{\to\square}$, each
world is represented by a context in a context stack. Nevertheless, the
conversion between Kripke and Fitch styles is largely
straightforward111However, we note that $\lambda^{\to\square}$ has never been
identified as or called a Fitch-style system.. Here, we will often use
“context” and “world” interchangeably. In $\lambda^{\to\square}$, a term $t$
is typed in a context stack $\overrightarrow{\Gamma}$ where initially, the
context stack consists of a single local context which is itself empty (i.e.
$\epsilon;\cdot$). ϵ; Γ_1; …; Γ_n ⊢t : T

or

$\overrightarrow{\Gamma}$⊢t : T The rightmost (or topmost) context represents
the current world. In the $\square$ introduction rule, we extend the context
stack with a new world (i.e. new context). In the elimination rule, if
$\square T$ is true in a context stack $\overrightarrow{\Gamma}$, then $T$ is
true in any worlds $\overrightarrow{\Gamma};\Delta_{1};\ldots;\Delta_{n}$
reachable from $\overrightarrow{\Gamma}$. The choice of the level $n$
corresponds to reflexivity and transitivity of the accessibility relation
between worlds in the Kripke semantics. * $\overrightarrow{\Gamma}$; ⋅ ⊢t : T
$\overrightarrow{\Gamma}$⊢box t : □T

* $\overrightarrow{\Gamma}$⊢t : □T $\overrightarrow{\Gamma}$; Δ_1; …; Δ_n ⊢unbox_n t : T There are two key advantages of this unbox formulation in $\lambda^{\to\square}$. First, it introduces a syntactic convenience to use natural numbers to describe levels and therefore allows us to elegantly capture various modal logics differing only in one parameter of the unbox rule. By introducing unbox levels, $\square$ is naturally non-idempotent. Having unbox allows us to study the relation of various sublogics of $S4$ and treat them uniformly and compactly.

Axiom \ System | $K$ | $T$ | $K4$ | $S4$
---|---|---|---|---
$K$: $\square(S\longrightarrow T)\to\square S\to\square T$ | $\checkmark$ | $\checkmark$ | $\checkmark$ | $\checkmark$
$T$: $\square T\to T$ |  | $\checkmark$ |  | $\checkmark$
$4$: $\square T\to\square\square T$ |  |  | $\checkmark$ | $\checkmark$
unbox level (UL) $n$ | { 1 } | { 0, 1 } | $\mathbb{N}^{+}$ | $\mathbb{N}$

Second, compared to dual-context formulation, it directly corresponds to
computational idioms quote (box) and unquote (unbox) in practice, thereby
giving a logical foundation to multi-staged meta-programming [15]. In
particular, allowing $n=0$ gives us the power to not only generate code, but
also to run and evaluate code.

A major stumbling block in reasoning about $\lambda^{\to\square}$ (see also
[19]) is the fact that it is not obvious how to define substitution properties
for context stacks. This prevents us from formulating an explicit substitution
calculus for $\lambda^{\to\square}$ which may serve as an efficient
implementation. More importantly, it also seems to be the bottleneck in
developing normalization proofs for $\lambda^{\to\square}$ that can be easily
adapted to the various subsystems of S4.

In this paper, we make the following contributions:

  1. (1)

We introduce the concept of of _Kripke-style substitutions_ on context stacks
(Sec. 3) which combines two previously separate concepts: modal
transformations on context stacks (such as modal weakening and fusion) and
substitution properties for individual assumptions within a given context.

  2. (2)

We extend the standard presheaf model [5] for simply typed $\lambda$-calculus
and obtain a normalization by evaluation (NbE) algorithm for
$\lambda^{\to\square}$ in Sec. 4. One critical feature of our development is
that the algorithm and the proof accommodate all four subsystems of S4
_without change_.

  3. (3)

As opposed to Nanevski et al. [32], we provide a contextual type formulation
in $\lambda^{\to\square}$ inspired by our notion of Kripke-style substitutions
in Sec. 5 which can serve as a construct for describing open code in a meta-
programming setting.

This work opens the door to a substitution calculus and normalization of a
dependently typed modal type theory. There are A partial formalization [24] of
this work in Agda [2, 33] and an accompanying technical report [25].

$\overrightarrow{\Gamma}\vdash t:T$ Term $t$ has type $T$ in context stack
$\overrightarrow{\Gamma}$ * x : T ∈Γ $\overrightarrow{\Gamma}$; Γ ⊢x : T

* $\overrightarrow{\Gamma}$; ⋅ ⊢t : T $\overrightarrow{\Gamma}$⊢box t : □T

* $\overrightarrow{\Gamma}$⊢t : □T
—$\overrightarrow{\Delta}$— = n $\overrightarrow{\Gamma}$;
$\overrightarrow{\Delta}$ ⊢unbox_n t : T

* $\overrightarrow{\Gamma}$;Γ, x : S ⊢t : T $\overrightarrow{\Gamma}$;Γ ⊢λx. t : S ⟶T

* $\overrightarrow{\Gamma}$⊢t : S ⟶T
$\overrightarrow{\Gamma}$⊢s : S $\overrightarrow{\Gamma}$⊢t s : T

$\overrightarrow{\Gamma}\vdash t\approx t^{\prime}:T$ Terms $t$ and
$t^{\prime}$ have type $T$ and are equivalent in context stack
$\overrightarrow{\Gamma}$

Figure 1: Typing judgments and some chosen equivalence judgments

##  2 Definition of $\lambda^{\to\square}$

In this section, we introduce the simply typed modal $\lambda$-calculus,
$\lambda^{\to\square}$, by Pfenning, Wong and Davies [35, 15] more formally.
We concentrate here on the fragment containing function types
$S\longrightarrow T$, the necessity modality $\square T$, and a base type $B$.

$\begin{array}[]{l@{~}l@{~}l}S,T\hfil~{}&:=\hfil~{}&\ B\;|\;\square
T\;|\;S\longrightarrow T\hfill\mbox{Types, {Typ}}\\\
l,m,n\hfil~{}&\lx@intercol\hfil\mbox{$\texttt{unbox}$ levels or offsets,
$\mathbb{N}$}\lx@intercol\\\ x,y\hfil~{}&\lx@intercol\hfil\mbox{Variables,
$\textsf{Var}$}\lx@intercol\\\ s,t,u\hfil~{}&:=\hfil~{}&x\;|\;\texttt{box}\
t\;|\;\texttt{unbox}_{n}\ t\;|\;\lambda x.t\;|\;s\ t\hfill\qquad\mbox{Terms,
$\textsf{Exp}$}\\\
\Gamma,\Delta,\Phi\hfil~{}&:=\hfil~{}&\cdot\;|\;\Gamma,x:T\hfill\mbox{Contexts,
{Ctx}}\\\ \overrightarrow{\Gamma},\overrightarrow{\Delta}\hfil~{}&:=\hfil~{}&\
\epsilon\;|\;\overrightarrow{\Gamma};\Gamma\hfill\mbox{Context stack,
$\overrightarrow{\textsf{Ctx}}$}\\\ w\hfil~{}&:=\hfil~{}&v\;|\;\texttt{box}\
w\;|\;\lambda x.w\hfill\mbox{Normal form, $\textsf{Nf}$}\\\
v\hfil~{}&:=\hfil~{}&x\;|\;v\ w\;|\;\texttt{unbox}_{n}\ v\hfill\mbox{Neutral
form, $\textsf{Ne}$}\end{array}$

Following standard practice, we consider variables, applications, and unbox
neutral. Functions, boxed terms and neutral terms are normal. Note that we
allow reductions under binders and inside boxed terms. As a consequence, a
function or a boxed term is normal, if their body is normal.

We define typing rules and type-directed equivalence between terms in Sec. 1.
We only show the rules for $\beta$ and $\eta$ equivalence of terms, but the
full set of rules can be found in Appendix A. We use Barendregt’s abstract
naming and $\alpha$ renaming to ensure that variables are unique with respect
to context stacks. The variable rule asserts that one can only refer to a
variable in the current world (the topmost context). In a typing judgment, we
require all context stacks to be non-empty, so the topmost context must exist.

From Kripke semantics’ point of view, the introduction rule for $\square$ says
a term of $\square T$ is just a term of $T$ in the next world. The elimination
rule brings $\square T$ from some previous world to the current world. This
previous world is determined by the level $n$. As mentioned earlier, the
choice of $n$ determines which logic the system corresponds to.
$|\overrightarrow{\Delta}|$ counts the number of contexts in
$\overrightarrow{\Delta}$.

To illustrate, we recap how the axioms in Sec. 1 can be described in
$\lambda^{\to\square}$. $K$ is defined by choosing $n=1$. Axiom $T$ requires
that $n=0$ and Axiom $4$ is only possible when unbox levels (ULs) can be $>1$.

$\begin{array}[]{llp{1cm}llp{1cm}ll}K&:\square(S\longrightarrow T)\to\square
S\to\square T&&T&:\square T\to T&&A4&:\square T\to\square\square T\\\ K\ f\
x&:=\texttt{box}\ ((\texttt{unbox}_{1}\ f)(\texttt{unbox}_{1}\ x))&&T\
x&:=\texttt{unbox}_{0}\ x&&A4\ x&:=\texttt{box}\ (\texttt{box}\
(\texttt{unbox}_{2}\ x))\end{array}$

The term equivalence rules are largely standard. In the $\eta$ rule for
$\square$, we restrict unbox to level $1$. In the $\beta$ rule for $\square$,
we rely on the modal transformation operation [15], written as $\\{n/0\\}$,
which allows us to transform the term $t$ which is well-typed in the context
stack $\overrightarrow{\Gamma};\cdot$ to the context stack
$\overrightarrow{\Gamma};\overrightarrow{\Delta}$. We abuse slightly notation
and use ; for both extending a context stack with a context and appending two
context stacks. We will discuss modal transformations more later in this
section.

###  2.1 Term Substitutions

A term substitution simply replaces a variable $x$ with a term $s$ in a term
$t$. It simply pushes the substitution inside the subterms of $t$ and avoiding
capture using renaming. Below, we simply restate the ordinary term
substitution lemma:

######  Lemma 2.1 (Term Substitution).

If
$\overrightarrow{\Gamma};(\Gamma,x{:}S,\Gamma^{\prime});\overrightarrow{\Delta}\vdash
t:T$ and $\overrightarrow{\Gamma};(\Gamma,\Gamma^{\prime})\vdash s:S$, then
$\overrightarrow{\Gamma};(\Gamma,\Gamma^{\prime});\overrightarrow{\Delta}\vdash
t[s/x]:T$.

###  2.2 Modal Transformations (MoTs)

In addition to the usual structural properties (weakening and contraction) of
individual contexts, $\lambda^{\to\square}$ also relies on structural
properties of context stacks, e.g. in the $\beta$ rule for $\square$. In
particular, we need to be able to weaken a context stack
$\overrightarrow{\Gamma};\overrightarrow{\Gamma}^{\prime}$ to
$\overrightarrow{\Gamma};\overrightarrow{\Delta};\overrightarrow{\Gamma}^{\prime}$
by splicing in additional contexts $\overrightarrow{\Delta}$ (_modal
weakening_). _Modal fusion_ allows us to combine two adjacent contexts in a
context stack transforming a context stack
$\overrightarrow{\Gamma};\Gamma_{0};\Gamma_{1};\overrightarrow{\Delta}$ to a
context stack
$\overrightarrow{\Gamma};(\Gamma_{0},\Gamma_{1});\overrightarrow{\Delta}$.

These modal transformations (_MoTs_) require us to relabel the level $n$
associated with the unbox eliminator. This is accomplished by the operation
$t\\{n/l\\}$. Assume that $t$ is well-typed in a context stack
$\overrightarrow{\Gamma}$. If $n>0$, then at position $l$ in the stack (i.e.
$\overrightarrow{\Gamma}=\overrightarrow{\Gamma}^{\prime};\overrightarrow{\Delta}$
and $|\overrightarrow{\Delta}|=l$), we splice in $n-1$ additional contexts. If
$n=0$, then this can be interpreted as fusing the two adjacent contexts at
position $l$ in the stack $\overrightarrow{\Gamma}$.

$\begin{array}[]{ll}x\\{n/l\\}&:=x\\\ \texttt{box}\ t\\{n/l\\}&:=\texttt{box}\
(t\\{n/l+1\\})\\\\[1.99997pt] \texttt{unbox}_{m}\
t\\{n/l\\}&:=\begin{cases}\texttt{unbox}_{m}\ (t\\{n/l-m\\})&\text{if $m\leq
l$}\\\ \texttt{unbox}_{n+m-1}\ t&\text{if $m>l$}\end{cases}\\\\[1.99997pt]
\lambda x.t\\{n/l\\}&:=\lambda x.(t\\{n/l\\})\\\ s\ t\\{n/l\\}&:=(s\\{n/l\\})\
(t\\{n/l\\})\end{array}$

In the box case, $l$ increases by one, as we extend the context stack by a new
world. In the unbox case, we distinguish cases based on the unbox level $m$.
If $m\leq l$, then we simply rearrange the ULs recursively in $t$. If $m>l$,
we only need to adjust the UL and do not recurse on $t$. MoTs satisfy the
following lemma:

######  Lemma 2.2 (Structural Property of Context Stacks).

If $\overrightarrow{\Gamma};\Gamma_{0};\Delta_{0};\cdots;\Delta_{l}\vdash
t:T$, then
$\overrightarrow{\Gamma};\Gamma_{0};\cdots;(\Gamma_{n},\Delta_{0});\cdots;\Delta_{l}\vdash
t\\{n/l\\}:T$.

We call the case where $n=0$ _modal fusion_ or just _fusion_. Other cases are
_modal weakening_. These names can be made sense of from the following
examples:

  * •

When $n=l=0$, the lemma states that if
$\overrightarrow{\Gamma};\Gamma_{0};\Delta_{0}\vdash t:T$, then
$\overrightarrow{\Gamma};(\Gamma_{0},\Delta_{0})\vdash t\\{0/0\\}:T$. Notice
that $\Gamma_{0}$ and $\Delta_{0}$ in the premise are fused into one in the
conclusion, hence “modal fusion”.

  * •

When $n=2$ and $l=0$, the lemma states that if
$\overrightarrow{\Gamma};\Gamma_{0};\Delta_{0}\vdash t:T$, then
$\overrightarrow{\Gamma};\Gamma_{0};\Gamma_{1};(\Gamma_{2},\Delta_{0})\vdash
t\\{2/0\\}:T$. A new context $\Gamma_{1}$ is inserted into the stack and the
topmost context is (locally) weakened by $\Gamma_{2}$, hence “modal
weakening”.

  * •

In the $\beta$ rule for $\square$, a MoT $\\{n/0\\}$ is used to transform $t$
in context stack $\overrightarrow{\Gamma};\cdot$ to
$\overrightarrow{\Gamma};\overrightarrow{\Delta}$.

  * •

When $l>0$, the leading $l$ contexts are skipped. If $n=2$, $l=1$ and
$\overrightarrow{\Gamma};\Gamma_{0};\Delta_{0};\Delta_{1}\vdash t:T$, then
$\overrightarrow{\Gamma};\Gamma_{0};\Gamma_{1};(\Gamma_{2},\Delta_{0});\Delta_{1}\vdash
t\\{2/1\\}:T$. Here $\Delta_{1}$ is kept as is.

##  3 Kripke-style Substitutions

Traditionally, we have viewed term substitutions and modal transformations as
two separate operations [15]. This makes reasoning about
$\lambda^{\to\square}$ complex. For example, a composition of $n$ MoTs leads
to up to $2^{n}$ cases in the unbox case. This becomes quickly unwieldy. How
can we avoid such case analyses by _unifying_ MoTs and term substitutions as
one operation that transforms context stacks? – We will view context stacks as
a category and a special _unifying_ group of simultaneous substitutions as
morphisms (denoted by $\Rightarrow$). MoTs are then simply a special case of
these morphisms. Lemma 2.2 suggests to view a MoT as a morphism:

$\begin{array}[]{c}\\{n/l\\}:\overrightarrow{\Gamma};\Gamma_{0};\cdots;(\Gamma_{n},\Delta_{0});\cdots;\Delta_{l}\Rightarrow\overrightarrow{\Gamma};\Gamma_{0};\Delta_{0};\cdots;\Delta_{l}\end{array}$

because $\\{n/l\\}$ moves $t$ from the codomain context stack to the domain
context stack. If this group of substitutions are closed under composition,
then a category of context stacks can be organized.

###  3.1 Composing MoTs

If MoTs are just special substitutions, then the composition of substitutions
must also compose MoTs. The following diagram is a composition of multiple
MoTs, forming a morphism
$\overrightarrow{\Gamma}\Rightarrow\overrightarrow{\Delta}$:

${\overrightarrow{\Gamma}:=\epsilon;}$${\Gamma_{0};}$${\Delta_{0};}$${\Delta_{1};}$${(\Gamma_{1},\Gamma_{2},\Gamma_{3});}$${\Delta_{2};}$${\Gamma_{4}}$${\overrightarrow{\Delta}:=\epsilon;}$${\Gamma_{0};}$${\Gamma_{1};\Gamma_{2};\Gamma_{3};}$${\Gamma_{4}}$

This composition contains both fusion ($\Gamma_{1}$, $\Gamma_{2}$,
$\Gamma_{3}$) and modal weakening ($\Delta_{0}$, $\Delta_{1}$, $\Delta_{2}$).
The thin arrows correspond to contexts in both stacks. Some of these arrows
are local identities ($\Gamma_{0}$ and $\Gamma_{4}$). They happen between
contexts that are affected by modal weakenings. The rest are local weakenings
($\Gamma_{1}$, $\Gamma_{2}$ and $\Gamma_{3}$); in this case, they are affected
by modal fusions. The first observation is that the size of gaps between
adjacent thin arrows varies, because it is determined by different MoTs.
Another observation is that thin arrows do not have to be just local
weakenings; if they contain general terms, then we obtain a general
simultaneous substitution. Moreover, thanks to the thin arrows, we know
exactly which context stack each term should be well-typed in. Combining all
information, we arrive at the definition of _Kripke-style substitutions_ :

######  Definition 3.1.

A Kripke-style substitution $\overrightarrow{\sigma}$, or just K-substitution,
between context stacks is defined as

$\begin{array}[]{ll}\sigma,\delta&:=()\;|\;\sigma,t/x\hfill\mbox{(Local)
substitutions, $\textsf{Subst}$}\\\
\overrightarrow{\sigma},\overrightarrow{\delta}&:=\varepsilon;\sigma\;|\;\overrightarrow{\sigma};\Uparrow^{n}\\!\\!{\sigma}\qquad\hfill\mbox{K-substitutions,
$\textsf{Substs}$}\end{array}$

σ: $\overrightarrow{\Gamma}$⇒Γ ε; σ : $\overrightarrow{\Gamma}$⇒ϵ;Γ

—$\overrightarrow{\Gamma}$’— = n σ:
$\overrightarrow{\Gamma}$;$\overrightarrow{\Gamma}$’ ⇒Δ
$\overrightarrow{\sigma}$;⇑^nσ:
$\overrightarrow{\Gamma}$;$\overrightarrow{\Gamma}$’
⇒$\overrightarrow{\Delta}$;Δ

where a local substitution $\sigma:\overrightarrow{\Gamma}\Rightarrow\Gamma$
is defined as a list of well-typed terms in $\overrightarrow{\Gamma}$ for all
bindings in $\Gamma$.

Just as context stacks must be non-empty and consist of at least one context,
a K-substitution must have a topmost local substitution written as
$\varepsilon;\sigma$ in the base case. It provides a mapping for the context
stack $\epsilon;\Gamma$. We extend a K-substitution $\overrightarrow{\sigma}$
with $\Uparrow^{n}\\!\\!\\!\sigma$ where $n$ captures the offset due to a MoT
and $\sigma$ is the local substitution. To illustrate, the morphism in the
previous diagram can be represented as
$\varepsilon;\textsf{id};\Uparrow^{3}\\!\\!{\textsf{wk}}_{1};\Uparrow^{0}\\!\\!{\textsf{wk}}_{2};\Uparrow^{0}\\!\\!{\textsf{wk}}_{3};\Uparrow^{2}\\!\\!{\textsf{id}}$
where id is the local identity substitution and
$\textsf{wk}_{i}:\Gamma_{0};\Delta_{0};\Delta_{1};(\Gamma_{1},\Gamma_{2},\Gamma_{3})\Rightarrow{\Gamma_{i}}$
are appropriate local weakenings. We break down this representation:

  1. (1)

We start with
$\varepsilon;\textsf{id}:\epsilon;\Gamma_{0}\Rightarrow\epsilon;\Gamma_{0}$.

  2. (2)

We add an offset $3$ and a local weakening $\textsf{wk}_{1}$, forming
$\varepsilon;\textsf{id};\Uparrow^{3}\\!\\!{\textsf{wk}}_{1}:\epsilon;\Gamma_{0};\Delta_{0};\Delta_{1};(\Gamma_{1},\Gamma_{2},\Gamma_{3})\Rightarrow\epsilon;\Gamma_{0};\Gamma_{1}$.
The offset $3$ adds three contexts to the domain stack ($\Delta_{0}$,
$\Delta_{1}$ and $\Gamma_{1},\Gamma_{2},\Gamma_{3}$). Local weakening
$\textsf{wk}_{1}$ extracts $\Gamma_{1}$ from
$\Gamma_{1},\Gamma_{2},\Gamma_{3}$.

  3. (3)

We extend the K-substitution to
$\varepsilon;\textsf{id};\Uparrow^{3}\\!\\!{\textsf{wk}}_{1};\Uparrow^{0}\\!\\!{\textsf{wk}}_{2}:\epsilon;\Gamma_{0};\Delta_{0};\Delta_{1};(\Gamma_{1},\Gamma_{2},\Gamma_{3})\Rightarrow\epsilon;\Gamma_{0};\Gamma_{1};\Gamma_{2}$.
Since the offset associated with $\textsf{wk}_{2}$ is $0$, no context is added
to the domain stack. This effectively represents fusion. $\textsf{wk}_{2}$ is
similar to $\textsf{wk}_{1}$.

  4. (4)

The rest of the K-substitution proceeds similarly.

Subsequently, we may simply write $\overrightarrow{\sigma};\sigma$ instead of
$\overrightarrow{\sigma};\Uparrow^{1}\\!\\!{\sigma}$. In particular, we will
write $\overrightarrow{\sigma};\textsf{wk}$ instead of
$\overrightarrow{\sigma};\Uparrow^{1}\\!\\!{\textsf{wk}}$ and
$\overrightarrow{\sigma};\textsf{id}$ instead of
$\overrightarrow{\sigma};\Uparrow^{1}\\!\\!{\textsf{id}}$. We often omit
offsets that are $1$ for readability.

###  3.2 Representing MoTs

Now we show that MoTs are a special case of K-substitutions. Let
$l:=|\overrightarrow{\Delta}|$. We define modal weakenings as

$\begin{array}[]{ll}\\{n+1/l\\}&:\overrightarrow{\Gamma};\Gamma_{1};\cdots;(\Gamma_{n+1},\Delta_{0});\overrightarrow{\Delta}\Rightarrow\overrightarrow{\Gamma};\Delta_{0};\overrightarrow{\Delta}\\\
\\{n+1/l\\}&=\varepsilon;\underbrace{\textsf{id};\cdots;\textsf{id}}_{|\overrightarrow{\Gamma}|};\Uparrow^{n+1}\textsf{wk};\underbrace{\textsf{id};\cdots;\textsf{id}}_{|\overrightarrow{\Delta}|}\end{array}$

where the offset $n+1$ on the right adds
$\Gamma_{1};\cdots;(\Gamma_{n+1},\Delta_{0})$ to $\overrightarrow{\Gamma}$ in
the domain stack and
$\textsf{wk}:\overrightarrow{\Gamma};\Gamma_{1};\cdots;(\Gamma_{n+1},\Delta_{0})\Rightarrow{\Delta_{0}}$.

Fusion is also easily defined:

$\begin{array}[]{ll}\\{0/l\\}&:\overrightarrow{\Gamma};(\Gamma_{1},\Gamma_{2});\overrightarrow{\Delta}\Rightarrow\overrightarrow{\Gamma};\Gamma_{1};\Gamma_{2};\overrightarrow{\Delta}\\\
\\{0/l\\}&=\varepsilon;\underbrace{\textsf{id};\cdots;\textsf{id}}_{|\overrightarrow{\Gamma}|};\textsf{wk}_{1};\Uparrow^{0}\\!\textsf{wk}_{2};\underbrace{\textsf{id};\cdots;\textsf{id}}_{|\overrightarrow{\Delta}|}\end{array}$

where the offset $0$ associated with $\textsf{wk}_{2}$ allows us to fuse
$\Gamma_{1}$ and $\Gamma_{2}$, and
$\textsf{wk}_{i}:\overrightarrow{\Gamma};(\Gamma_{1},\Gamma_{2})\Rightarrow{\Gamma_{i}}$
for $i\in\\{1,2\\}$.

###  3.3 Operations on K-Substitutions

We now show that K-substitutions are morphisms in a category of context
stacks. In order to define composition, we describe two essential operations:
1) _truncation_ ($\overrightarrow{\sigma}\mid{n}$) drops $n$ topmost
substitutions from a K-substitution $\overrightarrow{\sigma}$ and 2)
_truncation offset_ ($\mathcal{O}({\overrightarrow{\sigma}},{n})$) computes
the _total_ number of contexts that need to be dropped from the domain context
stack, given that we truncate $\overrightarrow{\sigma}$ by $n$. It computes
the sum of $n$ leading offsets. Let
$\overrightarrow{\sigma}:=\overrightarrow{\sigma}^{\prime};\Uparrow^{m_{n}}\\!\\!{\sigma_{n}};\ldots;\Uparrow^{m_{1}}\\!\\!{\sigma_{1}}$,
then $\mathcal{O}({\overrightarrow{\sigma}},{n})=m_{n}+\ldots+m_{1}$ and
$\overrightarrow{\sigma}\mid{n}=\overrightarrow{\sigma}^{\prime}$. For the
operation to be meaningful, $n$ must be less than $|\Delta|$.

$\begin{array}[]{ll}\lx@intercol\text{Truncation
Offset}\quad\mathcal{O}({\\_},{\\_}):(\overrightarrow{\Gamma}\Rightarrow\overrightarrow{\Delta})\to\mathbb{N}\to\mathbb{N}\hfil\lx@intercol\\\
\mathcal{O}({\overrightarrow{\sigma}},{0})&:=0\\\
\mathcal{O}({\overrightarrow{\sigma};\Uparrow^{n}\\!\\!{\sigma}},{1+m})&:=n+\mathcal{O}({\overrightarrow{\sigma}},{m})\end{array}$

Truncation simply drops $n$ local substitutions regardless of the offset that
is associated with each local substitution.

$\begin{array}[]{ll}\lx@intercol\text{Truncation}\quad\\_\mid{\\_}:(\overrightarrow{\sigma}:\overrightarrow{\Gamma}\Rightarrow\overrightarrow{\Delta})\to(n:\mathbb{N})\to\overrightarrow{\Gamma}\mid{\mathcal{O}({\overrightarrow{\sigma}},{n})}\Rightarrow\overrightarrow{\Delta}\mid{n}\hfil\lx@intercol\\\
\overrightarrow{\sigma}\mid{0}&:=\overrightarrow{\sigma}\\\
(\overrightarrow{\sigma};\Uparrow^{m}\\!\\!{\sigma})\mid{1+n}&:=\overrightarrow{\sigma}\mid{n}\end{array}$

Similar to truncation of K-substitutions, we rely on truncation of contexts,
written as $\overrightarrow{\Gamma}\mid{n}$ which simply drops $n$ contexts
from the context stack $\overrightarrow{\Gamma}$, i.e. if
$\overrightarrow{\Gamma}=\overrightarrow{\Gamma}^{\prime};\Gamma_{1};\ldots;\Gamma_{n}$,
then $\overrightarrow{\Gamma}\mid{n}=\overrightarrow{\Gamma}^{\prime}$. Note
that $n$ must satisfy $n<|\overrightarrow{\Gamma}|$, otherwise the operation
would not be meaningful. We emphasize that no further restrictions are placed
on $n$ and hence our definitions apply to any of the combinations of Axioms
$K$, $T$ and $4$ described in the introduction.

###  3.4 K-Substitution Operation

We now can define the K-substitution operation as follows:

$\begin{array}[]{ll}x[\varepsilon;\sigma]&:=\sigma(x)\qquad\hfill\mbox{lookup
$x$ in $\sigma$}\\\
x[\overrightarrow{\sigma};\Uparrow^{k}\\!\\!{\sigma}]&:=\sigma(x)\\\
(\texttt{box}\ t)[\overrightarrow{\sigma}]&:=\texttt{box}\
t[\overrightarrow{\sigma};\Uparrow^{1}\\!\\!{()}]\\\ (\texttt{unbox}_{n}\
t)[\overrightarrow{\sigma}]&:=\texttt{unbox}_{\mathcal{O}({\overrightarrow{\sigma}},{n})}\
(t[\overrightarrow{\sigma}\mid{n}])\\\ (\lambda
x.t)[\varepsilon;\sigma]&:=\lambda x.t[\varepsilon;(\sigma,x/x)]\\\ (\lambda
x.t)[\overrightarrow{\sigma};\Uparrow^{k}\\!\\!{\sigma}]&:=\lambda
x.t[\overrightarrow{\sigma};\Uparrow^{k}\\!\\!{(\sigma,x/x)}]\\\ (s\
t)[\overrightarrow{\sigma}]&:=s[\overrightarrow{\sigma}]\
u[\overrightarrow{\sigma}]\end{array}$

In the box case, the recursive call adds to $\overrightarrow{\sigma}$ an empty
local substitution. Note that the offset must be $1$, since we extend in the
box-introduction rule our context stack with a new empty context.

The unbox case for K-substitutions incorporates MoTs. Instead of
distinguishing cases based on the unbox level $n$, we use the truncation
offset operation to re-compute the UL and the recursive call
$t[\overrightarrow{\sigma}\mid{n}]$ continues with $\overrightarrow{\sigma}$
truncated, because $t$ is typed in a shorter stack.

Due to the typing invariants, we know that
$\mathcal{O}({\overrightarrow{\sigma}},{n})$ is indeed defined for all valid
UL $n$ in all our target systems. This fact can be checked easily. In System
$K$, since $n=1$ and all MoT offsets in $\overrightarrow{\sigma}$ are $1$, we
have that $\mathcal{O}({\overrightarrow{\sigma}},{n})=1$. In System $T$ where
$n\in\\{0,1\\}$ and $\overrightarrow{\sigma}$ only contains MoT offsets $0$
and $1$, we have $\mathcal{O}({\overrightarrow{\sigma}},{n})\in\\{0,1\\}$. In
System $K4$ where $n\geq 1$, $\mathcal{O}({\overrightarrow{\sigma}},{n})$
cannot be $0$ and thus $\mathcal{O}({\overrightarrow{\sigma}},{n})\geq 1$. In
System $S4$, since $n\in\mathbb{N}$,
$\mathcal{O}({\overrightarrow{\sigma}},{n})\in\mathbb{N}$ naturally holds.

The following lemma shows that K-substitutions are indeed the proper notion we
seek:

######  Lemma 3.2.

If $\overrightarrow{\Gamma}\vdash t:T$ and
$\overrightarrow{\sigma}:\overrightarrow{\Delta}\Rightarrow\overrightarrow{\Gamma}$,
then $\overrightarrow{\Delta}\vdash t[\overrightarrow{\sigma}]:T$.

###  3.5 Categorical Structure

We are now ready to organize K-substitutions into a category. First we define
the identity K-substitution:

$\begin{array}[]{l@{\;}l}\overrightarrow{\textsf{id}}_{\overrightarrow{\Gamma}}&:\overrightarrow{\Gamma}\Rightarrow\overrightarrow{\Gamma}\\\
\overrightarrow{\textsf{id}}_{\overrightarrow{\Gamma}}&:=\varepsilon;\textsf{id};\textsf{id};\cdots;\textsf{id}\end{array}$

where id’s are appropriate local identities. We again omit the offsets when we
extend K-substitutions with id, since they are $1$. We also omit the subscript
$\overrightarrow{\Gamma}$ on $\overrightarrow{\textsf{id}}$ for readability.

Composition is defined in terms of the K-substitution operation:

$\begin{array}[]{r@{\;\;}l}\\_\;\circ\\_&:\overrightarrow{\Gamma}^{\prime}\Rightarrow\overrightarrow{\Gamma}^{\prime\prime}\to\overrightarrow{\Gamma}\Rightarrow\overrightarrow{\Gamma}^{\prime}\to\overrightarrow{\Gamma}\Rightarrow\overrightarrow{\Gamma}^{\prime\prime}\\\
(\varepsilon;\sigma)\circ\overrightarrow{\delta}&:=\varepsilon;(\sigma[\overrightarrow{\delta}])\\\
(\overrightarrow{\sigma};\Uparrow^{n}\\!\\!{\sigma})\circ\overrightarrow{\delta}&:=(\overrightarrow{\sigma}\circ{(\overrightarrow{\delta}\mid{n})});\Uparrow^{\mathcal{O}({\overrightarrow{\delta}},{n})}\\!\\!{(\sigma[\overrightarrow{\delta}])}\end{array}$

where $\sigma[\overrightarrow{\delta}]$ iteratively applies
$\overrightarrow{\delta}$ to all terms in $\sigma$. In the recursive case, we
continue with a truncated K-substitution $\overrightarrow{\delta}\mid{n}$ and
recompute the offset.

Verification of the categorical laws is then routine:

######  Theorem 3.3.

Context stacks and K-substitutions form a category with identities and
composition defined as above.

###  3.6 Properties of Truncation and Truncation Offset

Finally, we summarize some critical properties of truncation and truncation
offset. Let
$\overrightarrow{\sigma}:\overrightarrow{\Gamma}^{\prime}\Rightarrow\overrightarrow{\Gamma}$
and
$\overrightarrow{\delta}:\overrightarrow{\Gamma}^{\prime\prime}\Rightarrow\overrightarrow{\Gamma}^{\prime}$:

######  Lemma 3.4.

If $n<|\overrightarrow{\Gamma}|$, then
$\mathcal{O}({\overrightarrow{\sigma}},{n})<|\overrightarrow{\Gamma}^{\prime}|$.

######  Lemma 3.5 (Distributivity of Addition).

If $n+m<|\overrightarrow{\Gamma}|$, then
$\overrightarrow{\sigma}\mid{(n+m)}=(\overrightarrow{\sigma}\mid{n})\mid{m}$
and
$\mathcal{O}({\overrightarrow{\sigma}},{n+m})=\mathcal{O}({\overrightarrow{\sigma}},{n})+\mathcal{O}({\overrightarrow{\sigma}\mid{n}},{m})$.

######  Lemma 3.6 (Distributivity of Composition).

If $n<|\overrightarrow{\Gamma}|$, then
$\mathcal{O}({\overrightarrow{\sigma}\circ\overrightarrow{\delta}},{n})=\mathcal{O}({\overrightarrow{\delta}},{\mathcal{O}({\overrightarrow{\sigma}},{n})})$
and
$(\overrightarrow{\sigma}\circ\overrightarrow{\delta})\mid{n}=(\overrightarrow{\sigma}\mid{n})\circ(\overrightarrow{\delta}\mid{\mathcal{O}({\overrightarrow{\sigma}},{n})})$.

These properties will be used in Sec. 4. Later we will define other instances
of truncation and truncation offsets but all these instances satisfy
properties listed here. Therefore, these properties sufficiently characterize
an algebra of truncation and truncation offset.

##  4 Normalization: A Presheaf Model

In this section, we present our NbE algorithm based on a presheaf model. Once
we determine the base category, the rest of the construction is largely
standard following Altenkirch et al. [5] with minor differences, which we will
highlight.

To construct the presheaf model, we first determine the base category. Then we
interpret types, contexts and context stacks to presheaves and terms to
natural transformations. After that, we define two operations, reification and
reflection, and use them to define the NbE algorithm. Last, we briefly discuss
the completeness and soundness proof. The algorithm is implemented in Agda
[24].

###  4.1 Kripke-style Weakenings

In the simply typed $\lambda$-calculus (STLC), the base category is the
category of weakenings. In $\lambda^{\to\square}$, we must consider the
effects of MoTs and we will use the more general notion of _Kripke-style
weakenings_ or K-weakenings which characterizes how a well-typed term in
$\lambda^{\to\square}$ moves from one context stack to another.

######  Definition 4.1.

A K-weakening
$\overrightarrow{\gamma}:\overrightarrow{\Gamma}\Rightarrow_{w}\overrightarrow{\Delta}$
is:

$\overrightarrow{\gamma}:=\varepsilon\;|\;q(\overrightarrow{\gamma})\;|\;p(\overrightarrow{\gamma})\;|\;\overrightarrow{\gamma};\Uparrow^{n}\\!\\!{}\qquad\hfill\mbox{(K-weakenings)}$

ε: ϵ; ⋅⇒_w ϵ; ⋅

$\overrightarrow{\gamma}$: $\overrightarrow{\Gamma}$; Γ⇒_w
$\overrightarrow{\Delta}$; Δ q($\overrightarrow{\gamma}$) :
$\overrightarrow{\Gamma}$; (Γ, x : T) ⇒_w $\overrightarrow{\Delta}$; (Δ, x :
T)

$\overrightarrow{\gamma}$: $\overrightarrow{\Gamma}$; Γ⇒_w
$\overrightarrow{\Delta}$; Δ p($\overrightarrow{\gamma}$) :
$\overrightarrow{\Gamma}$; (Γ, x : T) ⇒_w $\overrightarrow{\Delta}$; Δ

—$\overrightarrow{\Gamma}$’— = n $\overrightarrow{\gamma}$;⇑^n :
$\overrightarrow{\Gamma}$; $\overrightarrow{\Gamma}$’ ⇒_w
$\overrightarrow{\Delta}$; ⋅ (the offset $n$ depends on UL)  The $q$
constructor is the identity extension of the K-weakening
$\overrightarrow{\gamma}$, while $p$ accommodates weakening of an individual
context. These constructors are typical in the category of weakenings [5,
Definition 2]. To accommodate MoTs, we add to the category of weakenings the
last rule which transforms a context stack. In the last rule, the offset $n$
is again parametric, subject to the _same_ UL as the syntactic system, and its
choice determines which modal logic the system corresponds to. Note that we
also write $\overrightarrow{\textsf{id}}$ for the identity K-weakening.
Following our truncation and truncation offset operations for K-substitutions
in Sec. 3, we can easily define these operations together with composition
also for K-weakenings. We omit these definitions for brevity and we simply
note that a truncated K-weakening remains a K-weakening. Now we obtain the
base category:

######  Lemma 4.2.

K-weakenings form a category $\mathpzc{W}$.

###  4.2 Presheaves

The NbE proof is built on the presheaf category $\widehat{}\mathpzc{W}$ over
$\mathpzc{W}$. $\widehat{}\mathpzc{W}$ has presheaves
$\mathpzc{W}^{op}\Rightarrow\mathpzc{Set}$ as objects and natural
transformations as morphisms. We know from the Yoneda lemma that two
presheaves $F$ and $G$ can form a presheaf exponential
$F{\hat{\longrightarrow}}G$:

$\begin{array}[]{ll}F{\hat{\longrightarrow}}G&:\mathpzc{W}^{op}\Rightarrow\mathpzc{Set}\\\
(F{\hat{\longrightarrow}}G)_{\;\overrightarrow{\Gamma}}&:=\forall\overrightarrow{\Delta}\Rightarrow_{w}\overrightarrow{\Gamma}.F_{\;\overrightarrow{\Delta}}\to
G_{\;\overrightarrow{\Delta}}\end{array}$

It is natural in $\overrightarrow{\Delta}$. As a convention, we use subscripts
for both functorial applications and natural transformation components. As in
[5], presheaf exponentials model functions. To model $\square$, we define

$\begin{array}[]{rl}{\hat{\square}}F&:\mathpzc{W}^{op}\Rightarrow\mathpzc{Set}\\\
({\hat{\square}}F)_{\;\overrightarrow{\Gamma}}&:=F_{\;\overrightarrow{\Gamma};\cdot}\end{array}$

where $F$ is a presheaf. In Kripke semantics, ${\hat{\square}}$ takes $F$ to
the next world. Unlike presheaf exponentials which always exist regardless of
the base category, ${\hat{\square}}$ requires the base category to have the
notion of “the next world”. This dependency in turn allows us to embed the
Kripke structure of context stacks into the base category, so that our
presheaf model can stay a moderate extension of the standard construction [5].

With this setup, we give the interpretations of types, contexts, and context
stacks in Fig. 2. The interpretation of the base type $B$ is the presheaf from
context stacks to neutral terms of type $B$. We write $\textsf{Ne}\ T\
\overrightarrow{\Gamma}$ for the set of neutral terms of type $T$ in stack
$\overrightarrow{\Gamma}$. $\textsf{Ne}\ T$ then is the presheaf
$\overrightarrow{\Gamma}\mapsto\textsf{Ne}\ T\ \overrightarrow{\Gamma}$.
$\textsf{Nf}\ T\ \overrightarrow{\Gamma}$ and $\textsf{Nf}\ T$ are defined
similarly. The case $\llbracket\square T\rrbracket:={\hat{\square}}\llbracket
T\rrbracket$ states that semantically, a value of $\llbracket\square
T\rrbracket$ is just a value of $\llbracket T\rrbracket$ in the next world,
which implicitly relies on unified weakening’s capability of expressing MoTs.
$\hat{\top}$ are $\hat{\times}$ are a chosen terminal object and products in
$\widehat{}\mathpzc{W}$ and $*$ is _the only element_ in the chosen singleton
set.

The interpretation of context stacks is more interesting. In the step case,
$\overrightarrow{\Gamma};\Gamma$ is interpreted as a product. To extract both
part of
$\overrightarrow{\rho}\in\llbracket\overrightarrow{\Gamma}\rrbracket_{\overrightarrow{\Delta}}$,
we write $(\pi,\rho):=\overrightarrow{\rho}$ where
$(n,\overrightarrow{\rho}^{\prime}):=\pi$. The first component, namely $\pi$,
again consists of two parts: 1) the level $n$ satisfying
$n<|\overrightarrow{\Delta}|$ which corresponds to the MoTs that we support.
We note that our definitions again apply to any of the combinations of Axioms
$K$, $T$ and $4$ depending on the choice of $n$. 2) the recursive
interpretation of $\overrightarrow{\Gamma}$ in the truncated stack
$\overrightarrow{\Delta}\mid{n}$ described by
$\overrightarrow{\rho}^{\prime}$. This stack truncation is necessary to
interpret unbox.

The second component, namely $\rho$, describes the interpretation of the top-
most context $\Gamma$. The fact that our interpretation of context stacks
stores the level $n$ ultimately justifies the offsets stored in
K-substitutions.

$\displaystyle\llbracket\\_\rrbracket$
$\displaystyle:\textsf{Typ}\to\mathpzc{W}^{op}\Rightarrow\mathpzc{Set}$
$\displaystyle\llbracket B\rrbracket$ $\displaystyle:=\textsf{Ne}\ B$
$\displaystyle\llbracket\square T\rrbracket$
$\displaystyle:={\hat{\square}}\llbracket T\rrbracket$
$\displaystyle\llbracket S\longrightarrow T\rrbracket$
$\displaystyle:=\llbracket S\rrbracket{\hat{\longrightarrow}}\llbracket
T\rrbracket$

$\displaystyle\llbracket\\_\rrbracket$
$\displaystyle:\textsf{Ctx}\to\mathpzc{W}^{op}\Rightarrow\mathpzc{Set}$
$\displaystyle\llbracket\cdot\rrbracket$ $\displaystyle:=\hat{\top}$
$\displaystyle\llbracket\Gamma,x:T\rrbracket$
$\displaystyle:=\llbracket\Gamma\rrbracket\hat{\times}\llbracket T\rrbracket$

$\displaystyle\llbracket\\_\rrbracket$
$\displaystyle:\overrightarrow{\textsf{Ctx}}\to\mathpzc{W}^{op}\Rightarrow\mathpzc{Set}$
$\displaystyle\llbracket\epsilon;\Gamma\rrbracket$
$\displaystyle:=\hat{\top}\hat{\times}\llbracket\Gamma\rrbracket$
$\displaystyle\llbracket\overrightarrow{\Gamma};\Gamma\rrbracket_{\;\overrightarrow{\Delta}}$
$\displaystyle:=(\Sigma
n<|\overrightarrow{\Delta}|.\llbracket\overrightarrow{\Gamma}\rrbracket_{\;\overrightarrow{\Delta}\mid{n}})\;\times\;\llbracket\Gamma\rrbracket_{\;\overrightarrow{\Delta}}$
(where the offset $n$ depends on UL)

Figure 2: Interpretations of types, contexts and context stacks to presheaves

######  Lemma 4.3 (Functoriality).

$\llbracket T\rrbracket$, $\llbracket\Gamma\rrbracket$ and
$\llbracket\overrightarrow{\Gamma}\rrbracket$ are presheaves.

Functoriality means the interpretations also act on morphisms in
$\mathpzc{W}$. Given
$\overrightarrow{\gamma}:\overrightarrow{\Gamma}\Rightarrow_{w}\overrightarrow{\Delta}$
and $a\in\llbracket T\rrbracket_{\;\overrightarrow{\Delta}}$, we write
$a[\overrightarrow{\gamma}]\in\llbracket
T\rrbracket_{\;\overrightarrow{\Gamma}}$. We intentionally overload the
notation for applying K-substitutions to draw a connection. This notation also
applies for morphism actions of $\llbracket\Gamma\rrbracket$ and
$\llbracket\overrightarrow{\Gamma}\rrbracket$.

$\begin{array}[]{l@{\;}l}\lx@intercol\mbox{Evaluation}\qquad\llbracket\\_\rrbracket\\!\quad:\overrightarrow{\Gamma}\vdash
t:T\to\llbracket\overrightarrow{\Gamma}\rrbracket\Rightarrow\llbracket
T\rrbracket\hfil\lx@intercol\\\ \lx@intercol\mbox{Expanded form}~{}\llbracket
t\rrbracket_{\;\overrightarrow{\Delta}}:\llbracket\overrightarrow{\Gamma}\rrbracket_{\;\overrightarrow{\Delta}}{\;{\to}\;}\llbracket
T\rrbracket_{\;\overrightarrow{\Delta}}\hfil\lx@intercol\\\ \llbracket
x\rrbracket_{\;\overrightarrow{\Delta}}((\\_,\rho))&:=\rho(x)\hfill\mbox{lookup
$x$ in $\rho$}\\\ \llbracket\texttt{box}\
t\rrbracket_{\;\overrightarrow{\Delta}}(\overrightarrow{\rho})&:=\llbracket
t\rrbracket_{\;\overrightarrow{\Delta};\cdot}(((1,\overrightarrow{\rho}),*))\\\
\llbracket\texttt{unbox}_{n}\
t\rrbracket_{\overrightarrow{\Delta}}(\overrightarrow{\rho})&:=\llbracket
t\rrbracket_{\;\overrightarrow{\Delta}\mid{m}}(\overrightarrow{\rho}\mid{n})[\overrightarrow{\textsf{id}};\Uparrow^{m}]\qquad\mbox{where
$m:=\mathcal{O}({\overrightarrow{\rho}},{n})$ and
$\overrightarrow{\textsf{id}};\Uparrow^{m}:\overrightarrow{\Delta}\Rightarrow_{w}\overrightarrow{\Delta}\mid{m};\cdot$}\\\
\llbracket\lambda
x.t\rrbracket_{\;\overrightarrow{\Delta}}(\overrightarrow{\rho})&:=(\overrightarrow{\gamma}:\overrightarrow{\Delta}^{\prime}\Rightarrow_{w}\overrightarrow{\Delta})(a)\mapsto\llbracket
t\rrbracket_{\overrightarrow{\Delta}^{\prime}}((\pi,(\rho,a)))\hfill\text{where
$(\pi,\rho):=\overrightarrow{\rho}[\overrightarrow{\gamma}]$}\\\\[1.99997pt]
\llbracket t\
s\rrbracket_{\;\overrightarrow{\Delta}}(\overrightarrow{\rho})&:=\llbracket
t\rrbracket_{\;\overrightarrow{\Delta}}(\overrightarrow{\rho},\overrightarrow{\textsf{id}}_{\;\overrightarrow{\Delta}}~{},~{}\llbracket
s\rrbracket_{\;\overrightarrow{\Delta}}(\overrightarrow{\rho}))\\\\[5.0pt]
\lx@intercol\mbox{Reification}\quad\downarrow^{T}:\llbracket
T\rrbracket\Rightarrow\textsf{Nf}\ T\hfil\lx@intercol\\\
\downarrow^{B}_{\overrightarrow{\Gamma}}(a)&:=a\\\\[7.5pt] \downarrow^{\square
T}_{\overrightarrow{\Gamma}}(a)&:=\texttt{box}\
\downarrow^{T}_{\overrightarrow{\Gamma};\cdot}(a)\hfill\mbox{notice
$a\in({\hat{\square}}\llbracket
T\rrbracket)_{\overrightarrow{\Gamma}}=\llbracket
T\rrbracket_{\overrightarrow{\Gamma};\cdot}$}\\\\[7.5pt]
\downarrow^{S\longrightarrow T}_{\overrightarrow{\Gamma};\Gamma}(a)&:=\lambda
x.\downarrow^{T}_{\overrightarrow{\Gamma};(\Gamma,x:S)}(a~{}(p(\overrightarrow{\textsf{id}})~{},~{}{\uparrow^{S}_{\overrightarrow{\Gamma};(\Gamma,x:S)}\\!(x)}))\hfill\mbox{where
$p(\overrightarrow{\textsf{id}}):\overrightarrow{\Gamma};\Gamma,x{:}S\Rightarrow_{w}\overrightarrow{\Gamma};\Gamma$}\\\\[5.0pt]
\lx@intercol\mbox{Reflection}\quad\uparrow^{T}:\textsf{Ne}\
T\Rightarrow\llbracket T\rrbracket\hfil\lx@intercol\\\
\uparrow^{B}_{\overrightarrow{\Gamma}}(v)&:=v\\\\[7.5pt] \uparrow^{\square
T}_{\overrightarrow{\Gamma}}(v)&:=\uparrow^{T}_{\overrightarrow{\Gamma};\cdot}({\texttt{unbox}_{1}\
v})\\\\[7.5pt] \uparrow^{S\longrightarrow
T}_{\overrightarrow{\Gamma};\Gamma}(v)&:=(\overrightarrow{\gamma}:\overrightarrow{\Delta}\Rightarrow_{w}\overrightarrow{\Gamma};\Gamma)(a)\mapsto\uparrow^{T}_{\overrightarrow{\Delta}}(v[\overrightarrow{\gamma}]\
\downarrow^{S}_{\overrightarrow{\Delta}}(a))\end{array}$ Figure 3: Evaluation,
reification and reflection functions

###  4.3 Evaluation

The interpretation of well-typed terms to natural transformations, or
_evaluation_ (see Fig. 3), relies on truncation and the truncation offset.
These operations are defined below and follow the same principles that lie
behind the corresponding operations for syntactic K-substitutions.

$\begin{array}[]{llp{.5cm}ll}\lx@intercol\mbox{Truncation
Offset}\;\mathcal{O}({\\_},{\\_}):\llbracket\overrightarrow{\Gamma}\rrbracket_{\;\overrightarrow{\Delta}}\to\mathbb{N}\to\mathbb{N}\hfil\lx@intercol&&\lx@intercol\mbox{Truncation}\;\\_\mid{\\_}:(\overrightarrow{\rho}:\llbracket\overrightarrow{\Gamma}\rrbracket_{\;\overrightarrow{\Delta}})\;(n:\mathbb{N})\to\llbracket\overrightarrow{\Gamma}\mid{n}\rrbracket_{\overrightarrow{\Delta}\mid{\mathcal{O}({\overrightarrow{\rho}},{n})}}\hfil\lx@intercol\\\
\mathcal{O}({\overrightarrow{\rho}},{0})&:=0&&\overrightarrow{\rho}\mid{0}&:=\overrightarrow{\rho}\\\
\mathcal{O}({((n,\overrightarrow{\rho}),\rho)},{1+m})&:=n+\mathcal{O}({\overrightarrow{\rho}},{m})&&((n,\overrightarrow{\rho}),\rho)\mid{1+m}&:=\overrightarrow{\rho}\mid{m}\end{array}$

Most cases in evaluation are straightforward. In the box case the recursion
continues with an extended environment and $t$ in the next world. In the unbox
case, we first recursively interpret $t$ with a truncated environment and then
the result is K-weakened. This is because from the well-typedness of $t$, we
know $\overrightarrow{\Gamma}\mid{n}\vdash t:\square T$, so $\llbracket
t\rrbracket_{\;\overrightarrow{\Delta}\mid{m}}(\overrightarrow{\rho}\mid{n})$
gives an element in set $\llbracket\square
T\rrbracket_{\;\overrightarrow{\Delta}\mid{m}}=\llbracket
T\rrbracket_{\;\overrightarrow{\Delta}\mid{m};\cdot}$. To obtain our goal
$\llbracket T\rrbracket_{\;\overrightarrow{\Delta}}$, we can apply
monotonicity of $\llbracket T\rrbracket$ using a morphism
$\overrightarrow{\Delta}\Rightarrow_{w}\overrightarrow{\Delta}\mid{m};\cdot$,
which is given by $\overrightarrow{\textsf{id}};\Uparrow^{m}$. The cases
related to functions are identical to [5]. In the $\lambda$ case, since we
need to return a set function due to presheaf exponentials, we use $\mapsto$
to construct this function. We first K-weaken the environment
$\overrightarrow{\rho}$ and then extend it with the input value $a$. In the
application case, since $\llbracket t\rrbracket$ gives us a presheaf
exponential, we just need to apply it to $\llbracket s\rrbracket$. We simply
supply $\overrightarrow{\textsf{id}}_{\overrightarrow{\Delta}}$ for the
K-weakening argument because no extra weakening is needed.

The following lemma proves that $\llbracket t\rrbracket$ is a natural
transformation in $\overrightarrow{\Delta}$:

######  Lemma 4.4 (Naturality).

If $\overrightarrow{\Gamma}\vdash t:T$ and
$\overrightarrow{\rho}\in\llbracket\overrightarrow{\Gamma}\rrbracket_{\;\overrightarrow{\Delta}}$,
then for all K-weakenings
$\overrightarrow{\gamma}:\overrightarrow{\Delta}^{\prime}\Rightarrow_{w}\overrightarrow{\Delta}$,
we have $\llbracket
t\rrbracket_{\;\overrightarrow{\Delta}^{\prime}}(\overrightarrow{\rho}[\overrightarrow{\gamma}])=\llbracket
t\rrbracket_{\;\overrightarrow{\Delta}}(\overrightarrow{\rho})[\overrightarrow{\gamma}]$.

The lemma states that the result of evaluation in a K-weakened environment is
the same as K-weakening the result evaluated in the original environment. In
STLC, despite being a fact, naturality is not used anywhere in the proof. In
$\lambda^{\to\square}$, since K-weakenings encode MoTs, naturality is
necessary in the completeness proof.

After evaluation, we obtain a semantic value of the semantic type $\llbracket
T\rrbracket$. In the last step, we use a _reification_ function to convert the
semantic value back to a normal form. Reification is defined mutually with
_reflection_ in Fig. 3. As suggested by their signatures, they are both
natural transformations, but our proof does not rely on this fact. Both
reification and reflection are type-directed, so after reification we obtain
$\beta\eta$ normal forms. We reify a semantic value $a$ of box type $\square
T$ in a context stack $\overrightarrow{\Gamma}$ recursively extending the
context stack to $\overrightarrow{\Gamma};\cdot$. Note that $a$ has the
semantic type $({\hat{\square}}\llbracket
T\rrbracket)_{\overrightarrow{\Gamma}}$ which is defined as $\llbracket
T\rrbracket_{\overrightarrow{\Gamma};\cdot}$. In the case of function type
$S\longrightarrow T$, since $a$ is a presheaf exponential, we supply a
K-weakening and a value, the result of which is then recursively reified.

Reflection turns neutral terms into semantic values. We reflect neutral terms
of type $\square T$ recursively and incrementally extending the context stack
with one context at a time. In the function case, to construct a presheaf
exponential, we first take two arguments $\overrightarrow{\gamma}$ and $a$.
Since $v$ is a neutral term, $v[\overrightarrow{\gamma}]$ is also neutral but
now well-typed in $\overrightarrow{\Delta}$. Both recursive calls to
reification and reflection then go down to $\overrightarrow{\Delta}$ instead.

Normalization by evaluation (NbE) takes a well-typed term $t$ in a context
stack $\overrightarrow{\Gamma}$ as input, interprets $t$ to its semantic
counterpart in the initial environment, and reifies it back. Before defining
NbE more formally, we define the identity environment
$\llbracket\overrightarrow{\Gamma}\rrbracket_{\overrightarrow{\Gamma}}$ that
is used as the initial environment:

$\begin{array}[]{l@{}l}\uparrow&:(\overrightarrow{\Gamma}:\overrightarrow{\textsf{Ctx}})\to\llbracket\overrightarrow{\Gamma}\rrbracket_{\overrightarrow{\Gamma}}\\\
\uparrow^{\epsilon;\cdot}&:=(*,*)\\\
\uparrow^{\overrightarrow{\Gamma};\cdot}&:=((1,\uparrow^{\overrightarrow{\Gamma}}),*)\\\
\uparrow^{\overrightarrow{\Gamma};\Gamma,x:T}&:=(\pi,(\rho,\uparrow^{T}_{\overrightarrow{\Gamma};\Gamma,x:T}\\!\\!(x)))\hfill\;\;\mbox{where
$(\pi,\rho):=\uparrow^{\overrightarrow{\Gamma};\Gamma}[p(\overrightarrow{\textsf{id}})]$}\end{array}$

Finally we define the NbE algorithm:

######  Definition 4.5.

(Normalization by Evaluation) If $\overrightarrow{\Gamma}\vdash t:T$, then

$\textsf{nbe}^{T}_{\overrightarrow{\Gamma}}(t):=\downarrow^{T}_{\overrightarrow{\Gamma}}(\llbracket
t\rrbracket_{\overrightarrow{\Gamma}}(\uparrow^{\overrightarrow{\Gamma}}))$

###  4.4 Completeness and Soundness

The algorithm given above is sound and complete:

######  Theorem 4.6 (Completeness).

If $\overrightarrow{\Gamma}\vdash t\approx t^{\prime}:T$, then
$\textsf{nbe}^{T}_{\overrightarrow{\Gamma}}(t)=\textsf{nbe}^{T}_{\overrightarrow{\Gamma}}(t^{\prime})$.

######  Theorem 4.7 (Soundness).

If $\overrightarrow{\Gamma}\vdash t:T$, then $\overrightarrow{\Gamma}\vdash
t\approx\textsf{nbe}^{T}_{\overrightarrow{\Gamma}}(t):T$.

Due to space limitation, we are not able to present the whole proof.
Fortunately, the proof is very standard [5]. To prove completeness, we simply
need to prove that equivalent terms always evaluate to the same natural
transformation:

######  Lemma 4.8.

If $\overrightarrow{\Gamma}\vdash t\approx t^{\prime}:T$, then for any
$\overrightarrow{\rho}\in\llbracket\overrightarrow{\Gamma}\rrbracket_{\overrightarrow{\Delta}}$,
$\llbracket
t\rrbracket_{\overrightarrow{\Delta}}(\overrightarrow{\rho})=\llbracket
t^{\prime}\rrbracket_{\overrightarrow{\Delta}}(\overrightarrow{\rho})$.

######  Proof 4.9.

Induct on $\overrightarrow{\Gamma}\vdash t\approx t^{\prime}:T$ and apply
naturality in most cases about $\square$.

The soundness proof is established by a _Kripke gluing model_. The gluing
model $t\sim a\in\llparenthesis T\rrparenthesis_{\;\overrightarrow{\Gamma}}$
relates a syntactic term $t$ and a natural transformation $a$, so that after
reifying $a$, the resulting normal form is equivalent to $t$:

$\displaystyle\llparenthesis T\rrparenthesis_{\;\overrightarrow{\Gamma}}$
$\displaystyle\subseteq\textsf{Exp}\times\llbracket
T\rrbracket_{\;\overrightarrow{\Gamma}}$ $\displaystyle t\sim
a\in\llparenthesis B\rrparenthesis_{\;\overrightarrow{\Gamma}}$
$\displaystyle:=\overrightarrow{\Gamma}\vdash t\approx a:B$ $\displaystyle
t\sim a\in\llparenthesis\square T\rrparenthesis_{\;\overrightarrow{\Gamma}}$
$\displaystyle:=\overrightarrow{\Gamma}\vdash t:\square T\text{ and
}\forall\overrightarrow{\Delta}.\texttt{unbox}_{|\overrightarrow{\Delta}|}\
t\sim
a[\overrightarrow{\textsf{id}};\Uparrow^{|\overrightarrow{\Delta}|}]\in\llparenthesis
T\rrparenthesis_{\overrightarrow{\Gamma};\overrightarrow{\Delta}}$
$\displaystyle t\sim a\in\llparenthesis S\longrightarrow
T\rrparenthesis_{\;\overrightarrow{\Gamma}}$
$\displaystyle:=\overrightarrow{\Gamma}\vdash t:S\longrightarrow T\text{ and
}\forall\overrightarrow{\gamma}:\overrightarrow{\Delta}\Rightarrow_{w}\overrightarrow{\Gamma},s\sim
b\in\llparenthesis
S\rrparenthesis_{\;\overrightarrow{\Delta}}.t[\overrightarrow{\gamma}]\ s\sim
a(\overrightarrow{\gamma},b)\in\llparenthesis
T\rrparenthesis_{\;\overrightarrow{\Delta}}$

The gluing model should be monotonic in $\overrightarrow{\Gamma}$, hence
Kripke. Again the gluing model is very standard [5]. It is worth mentioning
that in the $\square T$ case, the Kripke predicate effectively requires that
$t$ and $a$ are related only when their results of _any_ unboxing remains
related. We then can move on to prove some properties of the gluing model and
define its generalization to substitutions, which eventually allow us to
conclude the soundness theorem. Please find more details in our technical
report [26].

###  4.5 Adaptiveness

We emphasize that our construction is stable no matter our choice of UL.
Hence, our construction applies to all four modal systems, $K$, $T$, $K4$ and
$S4$ that we introduced in Sec. 1 _without change_. The key insight that
allows us to keep our construction and model generic is the fact that
K-substitutions, K-weakenings, and
$\llbracket\overrightarrow{\Gamma}\rrbracket$ are instances of the algebra
formed by truncation and truncation offsets and satisfy all the properties, in
particular identity and distributivity, listed at the end of Sec. 3. More
importantly, all the truncation and truncation offset functions are defined
for all choices of UL thereby accommodating all four modal systems with their
varying level of unboxing.

##  5 Contextual Types

In $S4$ and a meta-programming setting, $\square$ is interpreted as stages,
where a term of type $\square T$ is considered as a term of type $T$ but
available only in the next stage. However, as pointed out in [15, 32],
$\square$ only characterizes closed code. Nanevski et al. [32] propose
contextual types which relativize the surrounding context of a term so
representing open code becomes possible. However, this notion of contextual
types is in the dual-context style and how contextual types can be formulated
with unbox and context stacks remains open. In this section, we answer this
question by utilizing our notion of K-substitutions.

###  5.1 Typing Judgments and Semi-K-substitutions

With contextual types, we augment the syntax as follows:

$\displaystyle S,T$
$\displaystyle:=\cdots\;|\;\lceil\overrightarrow{\Delta}\vdash T\rceil$
$\displaystyle s,t,u$
$\displaystyle:=\cdots\;|\;\lceil\overrightarrow{\Delta}\vdash
t\rceil\;|\;\lfloor
t\rfloor_{\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}}$

$\lceil\overrightarrow{\Delta}\vdash T\rceil$ is a contextual type. It
captures a list of contexts $\overrightarrow{\Delta}$ which a term of type $T$
can be open in. Note that $\overrightarrow{\Delta}$ here can be empty. This
notion of contextual types is very general and captures a term open in
multiple stages. $\lceil\overrightarrow{\Delta}\vdash t\rceil$ is the
constructor of a contextual type, where the contexts that it captures are
specified. $\lfloor
t\rfloor_{\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}}$
is the eliminator. Instead of an unbox level, we now require a different
argument
$\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}$,
which is a _semi-K-substitution_ storing unbox offsets and terms. We will
discuss more very shortly.

The introduction rule for contextual types is straightforward:
$\overrightarrow{\Gamma}$;$\overrightarrow{\Delta}$ ⊢t : T
$\overrightarrow{\Gamma}$⊢⌈$\overrightarrow{\Delta}$ ⊢t ⌉ :
⌈$\overrightarrow{\Delta}$ ⊢T ⌉ If we let
$\overrightarrow{\Delta}=\epsilon;\cdot$, then we recover $\square$. If we let
$\overrightarrow{\Delta}=\epsilon;\Delta$ for some $\Delta$, then we have an
open term $t$ which uses only assumptions in the same stage. If
$\overrightarrow{\Delta}$ has more contexts, then $t$ is an open term which
uses assumptions from previous stages. We can also let
$\overrightarrow{\Delta}=\epsilon$. In this case, $\lceil\epsilon\vdash
T\rceil$ is isomorphic to $T$ and is not too meaningful but allowing so makes
our formulation mathematically cleaner.

The elimination rule, on the other hand, becomes significantly more complex:
$\overrightarrow{\Gamma}$ ∣O(σ) ⊢t : ⌈$\overrightarrow{\Delta}$ ⊢T ⌉ σ:
$\overrightarrow{\Gamma}$⇒_s $\overrightarrow{\Delta}$
$\overrightarrow{\Gamma}$⊢⌊t ⌋_σ : T It is no longer enough to eliminate with
just an unbox level because the eliminator must specify how to replace all
variables in $\overrightarrow{\Delta}$ and how contexts in
$\overrightarrow{\Gamma}$ and $\overrightarrow{\Delta}$ relate. This
information is collectively stored in a _semi-K-substitution_
$\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}$
(notice the semi-arrow), which intuitively is not yet a valid K-substitution,
but close:

######  Definition 5.1.

A semi-K-substitution
$\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}$
is defined as follows:

$\displaystyle\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}},\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\delta}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\delta}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\delta}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\delta}}:=\varepsilon\;|\;\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}};\Uparrow^{n}\\!\\!{\sigma}$
Semi-K-substitutions, SSubsts

ε: $\overrightarrow{\Gamma}$⇒_s ϵ

—$\overrightarrow{\Gamma}$’— = n σ:
$\overrightarrow{\Gamma}$;$\overrightarrow{\Gamma}$’ ⇒Δ σ;⇑^nσ:
$\overrightarrow{\Gamma}$;$\overrightarrow{\Gamma}$’ ⇒_s
$\overrightarrow{\Delta}$;Δ  Compared to K-substitutions, semi-K-substitutions
differ in the base case, where empty $\varepsilon$ is permitted, so they are
not valid K-substitutions. However, if a semi-K-substitution is prepended by
an identity K-substitution, then the result is a valid K-substitution. Also,
$\mathcal{O}({\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}})$
computes the sum of all offsets in
$\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}$:

$\begin{array}[]{llp{2cm}ll}\overrightarrow{\textsf{id}};&:\textsf{SSubsts}\to\textsf{Substs}&&\mathcal{O}({\\_})&:\textsf{SSubsts}\to\mathbb{N}\\\
\overrightarrow{\textsf{id}};\varepsilon&:=\overrightarrow{\textsf{id}}&&\mathcal{O}({\varepsilon})&:=0\\\
\overrightarrow{\textsf{id}};(\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}};\Uparrow^{n}\\!\\!{\sigma})&:=(\overrightarrow{\textsf{id}};\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}});\Uparrow^{n}\\!\\!{\sigma}&&\mathcal{O}({\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}};\Uparrow^{n}\\!\\!{\sigma}})&:=\mathcal{O}({\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}})+n\end{array}$

We can prove the following lemma:

######  Lemma 5.2.

If
$\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}:\overrightarrow{\Gamma}\Rightarrow_{s}\overrightarrow{\Delta}$,
then
$\overrightarrow{\textsf{id}};\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}:\overrightarrow{\Gamma}\Rightarrow_{s}\overrightarrow{\Gamma}\mid{\mathcal{O}({\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}})};\overrightarrow{\Delta}$.

This lemma is needed to justify the $\beta$ equivalence rule which we are
about to discuss.

###  5.2 Equivalence of Contextual Types

Having defined the introduction and elimination rules, we are ready to
describe how they interact. Note that the congruence rules are standard so we
omit them here and only describe the $\beta$ and $\eta$ rules:
$\overrightarrow{\Gamma}$ ∣O(σ);$\overrightarrow{\Delta}$ ⊢t : T σ:
$\overrightarrow{\Gamma}$⇒_s $\overrightarrow{\Delta}$
$\overrightarrow{\Gamma}$⊢⌊⌈$\overrightarrow{\Delta}$ ⊢t ⌉ ⌋_σ
≈t[$\overrightarrow{\textsf{id}}$; σ] : T

$\overrightarrow{\Gamma}$⊢t : ⌈$\overrightarrow{\Delta}$ ⊢T ⌉
$\overrightarrow{\Gamma}$⊢t ≈⌈$\overrightarrow{\Delta}$ ⊢⌊t ⌋_id ⌉ :
⌈$\overrightarrow{\Delta}$ ⊢T ⌉ In the $\eta$ rule,
$\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\textsf{id}}}$
denotes the identity semi-K-substitution, which is defined as

$\displaystyle\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\textsf{id}}}_{\overrightarrow{\Delta}}$
$\displaystyle:\overrightarrow{\Gamma};\overrightarrow{\Delta}\Rightarrow_{s}\overrightarrow{\Delta}$
$\displaystyle\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\textsf{id}}}_{\overrightarrow{\Delta}}$
$\displaystyle:=\varepsilon;\underbrace{\textsf{id};\cdots;\textsf{id}}_{|\overrightarrow{\Delta}|}$

We omit the subscript whenever possible. Both rules are easily justified. In
the $\beta$ rule, since $t$ is typed in the context stack
$\overrightarrow{\Gamma}\mid{\mathcal{O}({\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}})};\overrightarrow{\Delta}$,
we obtain a term in $\overrightarrow{\Gamma}$ by applying
$\overrightarrow{\textsf{id}};\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\sigma}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\sigma}}$
due to Lemma 5.2. In the $\eta$ rule, by definition, we know
$(\overrightarrow{\Gamma};\overrightarrow{\Delta})\mid{\mathcal{O}({\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\textsf{id}}}})}=\overrightarrow{\Gamma}$
and therefore $\overrightarrow{\Gamma};\overrightarrow{\Delta}\vdash\lfloor
t\rfloor_{\mathchoice{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\displaystyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\textstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptstyle{\textsf{id}}}{\overarrow@\arrowfill@\mn@relbar\mn@relbar\rightharpoonup\scriptscriptstyle{\textsf{id}}}}:T$.

In an extensional setting, where the constructor and the eliminator of
modalities are congruent as done in this paper, we can show that the
contextual type $\lceil\epsilon;\Delta_{1};\cdots;\Delta_{n}\vdash T\rceil$ is
isomorphic to $\square(\Delta_{1}\to\cdots\square(\Delta_{n}\to T))$ if we
view contexts $\Delta_{i}$ as iterative products. This implies introducing
contextual types does not increase the logical strength of the system and the
system remains normalizing. Nevertheless, contextual types given here seem to
have a natural adaptation to dependent types and set a stepping stone towards
representing open code with dependent types and therefore a homogeneous,
dependently typed meta-programming system.

##  6 Related Work and Conclusion

###  6.1 Modal Type Theories

There are many early attempts to give a constructive formulation of modal
logic, especially the modal logic S4 starting back in the 1990’s [10, 9, 6, 3,
12, 31]. Pfenning and Davies [14, 34] give the first formulation of $S4$ in
the dual-context style where we separate the assumptions that are valid in
every world from assumptions that are true in the current world. This leads to
a dual-context style formulation that satisfies substitution properties and
has found many applications from staged computation to homotopy type theory
(HoTT). For example, Shulman [38] extends idempotent $S4$ with dependent
types, called spatial type theory and Licata et al. [30] define crisp type
theory, which removes the idempotency from spatial type theory. However, both
papers do not give a rigorous justification of their type theories. Most
recently Kavvos [28] investigates modal systems based on this dual-context
formulation for Systems $K$, $T$, $K4$ and $S4$ as well as the Löb induction
principle. Kavvos also gives categorical semantics for these systems.

However, it has been difficult to develop direct normalization proofs for
these dual-context formulations, since we must handle extensional properties
like commuting conversions (c.f. [28, 18]). Further, our four target systems
have very different formulations in the dual-context style as shown by Kavvos
[28]. As a consequence, it is challenging to have one single normalization
algorithm for all our four target systems.

An alternative to the dual-context style is the Fitch-style approach pursued
by Clouston, Birkedal and collaborators (see [13, 23, 11]). At the high-level,
Fitch-style systems also model the Kripke semantics, but instead of using one
context for each world, the Fitch style uses a special symbol (usually ) to
segment one context into multiple sections, each of them representing one
world. Variables to the left of the rightmost  are not accessible. Our
normalization proof and the generalization of $\lambda^{\to\square}$ to
contextual types also can likely be adapted to those systems.

Clouston [13] gives Systems $K$ and idempotent $S4$ in the Fitch style and
discusses their categorical semantics. Gratzer et al. [23] describe idempotent
$S4$ with dependent types. Birkedal et al. [11] give $K$ with dependent types
and formulate dependent right adjoints, an important categorical concept of
modalities. Gratzer et al. [21, 22, 20] proposes MTT, a multimode type theory,
which describes interactions between multiple modalities. Though MTT uses  to
segment contexts, we believe that MTT is better understood as a generalization
of the dual-context style and is apparent in the let-based formulation of the
box elimination rule. This different treatment of the box elimination also
makes it less obvious how to understand $\lambda^{\to\square}$ as a subsystem
of MTT.

Currently, existing Fitch-style systems mostly consider idempotent $S4$ where
$\square T$ is isomorphic to $\square\square T$. However, we consider this
distinction to be important from a computational view. For example, in multi-
staged programming (see [34, 15]) $\square T$ and $\square\square T$ describe
code generated in one stage and two stages, respectively. Moreover,
$\texttt{unbox}_{0}\ t$ is interpreted as evaluating and running the code
generated by $t$. It is nevertheless possible to develop a non-idempotent $S4$
system using unbox levels $n$ in the Fitch style by defining a function which
truncates a context until its $n$’th . This is however more elegantly handled
in $\lambda^{\to\square}$, because worlds are separated syntactically. For
this reason, we consider $\lambda^{\to\square}$ as a more versatile and more
suitable foundation for developing a dependently typed meta-programming
system. In particular, our extension to contextual types shows how we can
elegantly accomodate reasoning about open code which is important in practice.

Though context stacks in $\lambda^{\to\square}$ are taken from Pfenning, Wong
and Davies’ development [34, 15], Borghuis [12] also uses context stacks in
his development of modal pure type systems. The elimination rules use explicit
weakening and several “transfer” rules while $\lambda^{\to\square}$
incorporates both using unbox levels, which we consider more convenient and
more practical from a programmer’s point of view. Martini and Masini [31] also
use context stacks. Their system annotates all terms with a level which we
consider too verbose to be practical.

###  6.2 Normalization

For the dual-context style, Nanevski et al. [32] give contextual types and
prove normalization by reduction to another logical system with permutation
conversions [16]. This means that the proof is indirect and does not directly
yield an algorithm for normalizing terms. Kavvos [28] gives a rewriting-based
normalization proof for dual-context style systems with Löb induction. Most
recently, Gratzer [20] proves the normalization for MTT. It is not clear to us
whether techniques in [20] scale to dependently typed Kripke-style systems, as
the system have different treatment of the box elimination.

There are two recent papers closely related to our work: Valliappan et al.
[39] and Gratzer et al. [23]. [39] gives different simply typed formulations
in the Fitch style for all four subsystems of $S4$ and as a result, a
different normalization proof must be given to each subsystem individually.
Gratzer et al. [23] follow Abel [1] and give an NbE proof for dependently
typed idempotent $S4$. Since the proof in [23] is parameterized by an extra
layer of poset to model the Kripke world structure introduced by $\square$, as
pointed out in [21], this proof cannot even be easily adapted to dependently
typed $K$ (see Birkedal et al. [11]). Compared to these two papers, our model
is a moderate extension to the standard presheaf model, requiring no such
extra layer and adapting to multiple logics automatically, and we are
confident that it will generalize more easily to the dependently typed
setting. The ultimate reason why we only need one proof to handle all four
subsystems of $S4$ is that we _internalize_ the Kripke structure of context
stacks in the presheaf model. The internalization happens in the base
category, where MoTs are encoded as part of K-weakenings. The internalization
captures peculiar behaviours of different systems and conflates the extra
Kripke structure from context stacks and the standard model construction, so
that the proofs become much simpler and closer to the typical construction.

###  6.3 Conclusion and Future Work

In this paper, we present a normalization-by-evaluation (NbE) algorithm for
the simply-typed modal $\lambda$-calculus ($\lambda^{\to\square}$) which
covers all four subsystems of S4. The key to achieving this result is our
notion of K-substitutions which provides a unifying account for modal
transformations and term substitutions and allows us to formulate a
substitution calculus for modal logic S4 and its various subsystems. Such
calculus is not only important from a practical point of view, but play also a
central role in our theoretical analysis. Using insights gained from
K-substitutions we organize a presheaf model, from which we extract a
normalization algorithm. The algorithm can be implemented in conventional
programming languages and directly account for the normalization of
$\lambda^{\to\square}$. Deriving from K-substitutions, we are also able to
give a formulation for contextual types with unbox and context stacks, which
had been challenging prior to our observation of K-substitutions and is
important for representing open code in a meta-programming setting.

This work serves as a basis for further investigations into coproducts [4] and
categorical structure of context stacks. We also see this work as a step
towards a Martin-Löf-style modal type theory in which open code has an
internal shallow representation. With a dependently typed extension and
contextual types, it would allow us to develop a _homogeneous_ meta-
programming system with dependent types which has been challenging to achieve.

This work was funded by the Natural Sciences and Engineering Research Council
of Canada (grant number 206263), Fonds de recherche du Québec - Nature et
Technologies (grant number 253521), and Postgraduate Scholarship - Doctoral by
the Natural Sciences and Engineering Research Council of Canada awarded to the
first author.

## References

  * [1] Abel, A., “Normalization by evaluation: dependent types and impredicativity,” Habilitation thesis, Ludwig-Maximilians-Universität München (2013).
  * [2] Agda Team, _Agda 2.6.2_ (2021).
  * [3] Alechina, N., M. Mendler, V. de Paiva and E. Ritter, _Categorical and Kripke Semantics for Constructive S4 Modal Logic_ , in: L. Fribourg, editor, _Computer Science Logic_ , Lecture Notes in Computer Science (2001), pp. 292–307.
  * [4] Altenkirch, T., P. Dybjer, M. Hofmann and P. Scott, _Normalization by evaluation for typed lambda calculus with coproducts_ , in: _Proceedings 16th Annual IEEE Symposium on Logic in Computer Science_ , 2001, pp. 303–310, iSSN: 1043-6871.
  * [5] Altenkirch, T., M. Hofmann and T. Streicher, _Categorical reconstruction of a reduction free normalization proof_ , in: D. Pitt, D. E. Rydeheard and P. Johnstone, editors, _Category Theory and Computer Science_ (1995), pp. 182–199.
  * [6] Bellin, G., V. C. V. de Paiva and E. Ritter, _Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic_ , in: _In Proceedings of Methods for Modalities_ , 2001.
  * [7] Bierman, G. and V. de Paiva, _Intuitionistic necessity revisited_ , Technical Report CSR–96–10, University of Birmingham (1996).
  * [8] Bierman, G. M. and V. de Paiva, _On an intuitionistic modal logic_ , Studia Logica 65 (2000), pp. 383–416.
URL https://doi.org/10.1023/A:1005291931660

  * [9] Bierman, G. M. and V. de Paiva, _On an Intuitionistic Modal Logic_ , Studia Logica 65 (2000), pp. 383–416.
URL https://doi.org/10.1023/A:1005291931660

  * [10] Bierman, G. M. and V. C. V. de Paiva, _Intuitionistic Necessity Revisited_ , Technical report, University of Birmingham (1996).
  * [11] Birkedal, L., R. Clouston, B. Mannaa, R. E. Møgelberg, A. M. Pitts and B. Spitters, _Modal dependent type theory and dependent right adjoints_ , Mathematical Structures in Computer Science 30 (2020), pp. 118–138, publisher: Cambridge University Press.
URL https://www.cambridge.org/core/journals/mathematical-structures-in-
computer-science/article/abs/modal-dependent-type-theory-and-dependent-right-
adjoints/215682F46705DE70A67946FE73C95A3E

  * [12] Borghuis, V. A. J., “Coming to terms with modal logic : on the interpretation of modalities in typed lambda-calculus,” PhD Thesis, Mathematics and Computer Science (1994).
  * [13] Clouston, R., _Fitch-Style Modal Lambda Calculi_ , in: C. Baier and U. Dal Lago, editors, _Foundations of Software Science and Computation Structures_ , Lecture Notes in Computer Science (2018), pp. 258–275.
  * [14] Davies, R. and F. Pfenning, _A modal analysis of staged computation_ , in: H. Boehm and G. L. S. Jr., editors, _Conference Record of POPL’96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996_ (1996), pp. 258–270.
URL https://doi.org/10.1145/237721.237788

  * [15] Davies, R. and F. Pfenning, _A modal analysis of staged computation_ , Journal of the ACM 48 (2001), pp. 555–604.
URL https://dl.acm.org/doi/10.1145/382780.382785

  * [16] de Groote, P., _On the Strong Normalization of Natural Deduction with Permutation-Conversions_ , in: P. Narendran and M. Rusinowitch, editors, _Rewriting Techniques and Applications_ , Lecture Notes in Computer Science (1999), pp. 45–59.
  * [17] Ghani, N., V. de Paiva and E. Ritter, _Explicit substitutions for constructive necessity_ , in: K. G. Larsen, S. Skyum and G. Winskel, editors, _25th International Colloquium on Automata, Languages and Programming (ICALP’98)_ , Lecture Notes in Computer Science 1443 (1998), pp. 743–754.
URL https://doi.org/10.1007/BFb0055098

  * [18] Girard, J.-Y., “Proofs and types,” Number 7 in Cambridge tracts in theoretical computer science, Cambridge University Press, Cambridge [England] ; New York, 1989.
  * [19] Goubault-Larrecq, J., _On computational interpretations of the modal logic s4: Ii. the $\lambda$ev$q$-calculus_, Technical report, Univeristy of Karlsruhe (1996).
  * [20] Gratzer, D., _Normalization for multimodal type theory_ , in: _Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science_ , LICS ’22 (2022).
  * [21] Gratzer, D., G. A. Kavvos, A. Nuyts and L. Birkedal, _Multimodal Dependent Type Theory_ , in: _Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science_ , LICS ’20 (2020), pp. 492–506.
URL https://doi.org/10.1145/3373718.3394736

  * [22] Gratzer, D., G. A. Kavvos, A. Nuyts and L. Birkedal, _Multimodal Dependent Type Theory_ , Log. Methods Comput. Sci. 17 (2021).
  * [23] Gratzer, D., J. Sterling and L. Birkedal, _Implementing a modal dependent type theory_ , Proceedings of the ACM on Programming Languages 3 (2019), pp. 107:1–107:29.
URL https://doi.org/10.1145/3341711

  * [24] Hu, J. Z. S. and B. Pientka, _Agda mechanization_.
URL https://hustmphrrr.github.io/Kripke-style/Unbox.README.html

  * [25] Hu, J. Z. S. and B. Pientka, _An Investigation of Kripke-style Modal Type Theories_ (2022), number: arXiv:2206.07823 arXiv:2206.07823 [cs].
URL http://arxiv.org/abs/2206.07823

  * [26] Hu, J. Z. S. and B. Pientka, _An investigation of kripke-style modal type theories_ , CoRR abs/2206.07823 (2022).
URL https://doi.org/10.48550/arXiv.2206.07823

  * [27] Jang, J., S. Gélineau, S. Monnier and B. Pientka, _Moebius: Metaprogramming using contextual types – the stage where system f can pattern match on itself_ , Proc. ACM Program. Lang. (PACMPL) (2022).
  * [28] Kavvos, G. A., _Dual-context calculi for modal logic_ , in: _2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_ , 2017, pp. 1–12.
  * [29] Kripke, S. A., _Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi_ , Mathematical Logic Quarterly 9 (1963), pp. 67–96, _eprint: https://onlinelibrary.wiley.com/doi/pdf/10.1002/malq.19630090502.
URL https://onlinelibrary.wiley.com/doi/abs/10.1002/malq.19630090502

  * [30] Licata, D. R., I. Orton, A. M. Pitts and B. Spitters, _Internal Universes in Models of Homotopy Type Theory_ , in: H. Kirchner, editor, _3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)_ , Leibniz International Proceedings in Informatics (LIPIcs) 108 (2018), pp. 22:1–22:17, iSSN: 1868-8969.
URL http://drops.dagstuhl.de/opus/volltexte/2018/9192

  * [31] Martini, S. and A. Masini, _A Computational Interpretation of Modal Proofs_ , in: H. Wansing, editor, _Proof Theory of Modal Logic_ , Applied Logic Series, Springer Netherlands, Dordrecht, 1996 pp. 213–241.
URL https://doi.org/10.1007/978-94-017-2798-3_12

  * [32] Nanevski, A., F. Pfenning and B. Pientka, _Contextual modal type theory_ , ACM Transactions on Computational Logic 9 (2008), pp. 23:1–23:49.
URL https://doi.org/10.1145/1352582.1352591

  * [33] Norell, U., “Towards a practical programming language based on dependent type theory,” PhD Thesis, Chalmers University of Technology (2007).
  * [34] Pfenning, F. and R. Davies, _A judgmental reconstruction of modal logic_ , Mathematical Structures in Computer Science 11 (2001).
URL http://www.journals.cambridge.org/abstract_S0960129501003322

  * [35] Pfenning, F. and H.-C. Wong, _On a modal $\lambda$-calculus for S4_, in: S. Brookes and M. Main, editors, _Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Semantics_ , New Orleans, Louisiana, 1995, Electronic Notes in Theoretical Computer Science, Volume 1, Elsevier.
  * [36] Pientka, B., _A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions_ , in: _35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08)_ , 2008, pp. 371–382.
  * [37] Pientka, B., A. Abel, F. Ferreira, D. Thibodeau and R. Zucchini, _A type theory for defining logics and proofs_ , in: _34th IEEE/ ACM Symposium on Logic in Computer Science (LICS’19)_ (2019), pp. 1–13.
  * [38] Shulman, M., _Brouwer’s fixed-point theorem in real-cohesive homotopy type theory_ , Mathematical Structures in Computer Science 28 (2018), pp. 856–941, publisher: Cambridge University Press.
  * [39] Valliappan, N., F. Ruch and C. Tomé Cortiñas, _Normalization for fitch-style modal calculi_ , Proc. ACM Program. Lang. 6 (2022), pp. 772–798.
URL https://doi.org/10.1145/3547649

  * [40] Zyuzin, N. and A. Nanevski, _Contextual modal types for algebraic effects and handlers_ , Proc. ACM Program. Lang. 5 (2021), pp. 1–29.
URL https://doi.org/10.1145/3473580

##  Appendix A Equivalence Rules

* $\overrightarrow{\Gamma}$⊢s ≈t : T $\overrightarrow{\Gamma}$⊢t ≈s : T

* $\overrightarrow{\Gamma}$⊢s ≈t : T $\overrightarrow{\Gamma}$⊢t ≈u : T $\overrightarrow{\Gamma}$⊢s ≈u : T

* x : T ∈Γ $\overrightarrow{\Gamma}$; Γ ⊢x ≈x : T

* $\overrightarrow{\Gamma}$; ⋅ ⊢t ≈t’ : T $\overrightarrow{\Gamma}$⊢box t ≈box t’ : □T

* $\overrightarrow{\Gamma}$⊢t ≈t’ : □T —$\overrightarrow{\Delta}$— = n $\overrightarrow{\Gamma}$; $\overrightarrow{\Delta}$ ⊢unbox_n t ≈unbox_n t’ : T’

* $\overrightarrow{\Gamma}$;(Γ, x : S) ⊢t ≈t’ : T $\overrightarrow{\Gamma}$; Γ ⊢λx. t ≈λx. t’ : S ⟶T

* $\overrightarrow{\Gamma}$⊢t ≈t’ : S ⟶T $\overrightarrow{\Gamma}$⊢s ≈s’ : S $\overrightarrow{\Gamma}$⊢t s ≈t’ s’ : T

* $\overrightarrow{\Gamma}$; ⋅ ⊢t : T —$\overrightarrow{\Delta}$— = n $\overrightarrow{\Gamma}$; $\overrightarrow{\Delta}$ ⊢unbox_n (box t) ≈t{n / 0 } : T

* $\overrightarrow{\Gamma}$;(Γ, x : S) ⊢t : T $\overrightarrow{\Gamma}$; Γ ⊢s : S $\overrightarrow{\Gamma}$; Γ ⊢(λx. t) s ≈t[s/x] : T

* $\overrightarrow{\Gamma}$⊢t : □T $\overrightarrow{\Gamma}$⊢t ≈box unbox_1 t : □T

* $\overrightarrow{\Gamma}$⊢t : S ⟶T $\overrightarrow{\Gamma}$⊢t ≈λx. (t x) : S ⟶T