# The Vanilla Sequent Calculus is Call-by-Value

Beniamino Accattoli

► To cite this version:

Beniamino Accattoli. The Vanilla Sequent Calculus is Call-by-Value. ESOP 2025 - 34th European Symposium on Programming, May 2025, Hamilton, Canada. pp.1-22, 10.1007/978-3-031-91118-7_1.hal-05454658

HAL Id: hal-05454658

https://hal.science/hal-05454658v1

Submitted on 12 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# The Vanilla Sequent Calculus is Call-by-Value

Beniamino Accattoli(✉) ID

Inria & LIX, Ecole Polytechnique, UMR 7161, Palaiseau, France

beniamino.accattoli@inria.fr

**Abstract.** Existing Curry-Howard interpretations of call-by-value evaluation for the λ-calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact that call-by-value was introduced in an intuitionistic setting without linear features.

This paper shows that the most basic sequent calculus for minimal intuitionistic logic—dubbed here vanilla—can naturally be seen as a logical interpretation of call-by-value evaluation. This is obtained by establishing mutual simulations with a well-known formalism for call-by-value evaluation.

**Keywords:** λ-calculus, proof theory, Curry-Howard.

## 1 Introduction

The connection between functional languages and proof theory stems from Howard's insight that the system of simple types for the λ-calculus is exactly Gentzen's natural deduction for minimal intuitionistic logic [41]. Additionally, β-reduction exactly matches the logical process of *detour elimination*, also called *normalization*. This correspondence concerns the unrestricted, or *call-by-name*, notion of β-reduction.

In practice, the evaluation mechanism at work in functional languages never follows that of call-by-name of the ordinary λ-calculus. Plotkin's call-by-value λ-calculus [52] restricts β-reduction to fire when the argument is a *value*, that is, a variable or an abstraction, and it is often seen as a better fit for applications.

*Call-by-Value and Natural Deduction.* Natural deduction, unfortunately, does not provide a solid logical foundation for call-by-value (shortened to CbV). On the positive side, values are proofs ending in a logical introduction rule. The restriction to values in the proof normalization process, however, has to be *enforced*; it does not arise naturally from the structure of natural deduction. Moreover, when one considers open terms and/or strong evaluation (that is, under abstraction), the normal forms of Plotkin's CbV calculus have a complex inductive structure not corresponding to any natural concept in natural deduction. The study of strong evaluation is essential for proof assistants based on dependent types. Notably, Leroy and Grégoire use strong CbV for Coq [37]. Strong evaluation is also advocated by Scherer and Rémy [57] as relevant for a solid theory of functional languages. Lastly, in proof theory one speaks of *cut/detour elimination*, and they can be eliminated only if evaluation goes under abstractions.
$$ 
\begin{array}{ccc}
\frac{\Gamma \vdash A \quad \Gamma, A \vdash B}{\Gamma \vdash B} & \text{cut} & \frac{\Gamma, A \vdash A}{\Gamma \vdash A} \quad \text{ax} \\[1.5em]
\frac{\Gamma \vdash A \quad \Gamma, B \vdash C}{\Gamma, A \Rightarrow B \vdash C} & \Rightarrow_I & \frac{\Gamma, A \vdash B \quad \Gamma \vdash A \Rightarrow B}{\Gamma \vdash A \Rightarrow B} \quad \Rightarrow_r
\end{array}
$$

<caption>**Fig. 1.** Vanilla sequent calculus for minimal intuitionistic logic (MIL).</caption>

The issue with normal forms is delicate. It is well-known that the rewriting rules of Plotkin's calculus are not suited for open terms and strong evaluation, causing *premature normal forms*, as pointed out by Paolini and Ronchi della Rocca [51,50,55]. The literature contains many alternative CbV $\lambda$-calculi fixing this defect, as surveyed by Accattoli and Guerrieri [6], often extending the syntax of the $\lambda$-calculus with let-expressions or explicit substitutions, as for instance is the case in Moggi's calculus [46,47].

Logically, both let-expressions and explicit substitutions are decorations for the (intuitionistic) cut rule. Even when one considers these alternative CbV $\lambda$-calculi not suffering of premature normal forms, natural deduction with cut is not really a solid logical foundation, because CbV normal terms correspond to proofs with cuts. That is, not all cuts are eliminable.

*Call-by-Value and Proof Theory.* Beyond natural deduction for minimal intuitionistic logic (shortened to MIL), there are two main ways of looking at CbV via proof theory. One of them is as a certain intuitionistic fragment of linear logic, as first done by Girard [35], which can also be seen as a certain embedding into the modal logic S4, as pointed out recently by Espírito Santo et al. [30]. Another way is via the duality between CbV and call-by-name (CbN) in classical logic, usually traced back to Filinski [31]. This duality was then analyzed through linear logic lenses by Danos et al. [21], and crystalized as the computational interpretation of a sequent calculus by Curien and Herbelin [18].

What is not ideal, however, is that these are additional logical concepts. In Plotkin's CbV (and in many of the alternative CbV $\lambda$-calculi), indeed, there is no trace of linearity nor of classical principles. It is natural to wonder whether there is a neat logical way of modeling CbV using only MIL. There are works connecting CbV and MIL, such as Dyckhoff and Lengrand's study of Herbelin's LJQ [40,25,26] or Ohori [49], but they are based on modifications of the deductive system imposing the CbV reading. This paper presents a fresh perspective on this question.

*The Vanilla Sequent Calculus.* Our result is that the most basic presentation of Gentzen's sequent calculus [34] for MIL, here dubbed vanilla sequent calculus and shown in Fig. 1 (the proper additive presentation of MIL requires some further details about contractions, see Sect. 3), is a natural Curry-Howard reading of CbV evaluation. The system comes with a natural notion of values, which are proofs ending with right deduction rules. Crucially, we exploit a splitting property that is specific to sequent proofs of MIL: every proof of $\Gamma \vdash A$ can be uniquely split into a value sub-proof of $\Delta \vdash A$ followed by a sequence of left rules turning $\Delta$ into $\Gamma$ without touching $A$. Thanks to this feature, there is no need to modify the sequent calculus with a so-called stoup (i.e. a distinguished formula in a formula context) as in Curien and Herbelin [18], adding restrictions on the
shape of proofs as in Herbelin’s presentation of LJQ [40] or Ohori [49], or having a separate judgement for values as in Lengrand and Dyckhoff’s presentation of LJQ [25,26]. Essentially, values are recovered on-the-fly, with no need to mark them out explicitly.

Beyond the splitting property, our fresh perspective stems from the observation that the ineliminable cuts in the CbV reading of natural deduction correspond exactly to occurrences of the left rule ($\Rightarrow_I$) for $\Rightarrow$ in the vanilla sequent calculus. In other words, the cut rule in CbV natural deduction is *overloaded*. When one looks at it through the vanilla sequent calculus, it represents both the vanilla (cut) and ($\Rightarrow_I$) rules. Disentangling the two concepts, the vanilla sequent calculus provides a neater logical foundation where CbV normal terms have no cuts, as one would expect.

Concretely, we adopt proof terms for the vanilla sequent calculus defined without the application $ts$ construct (which is specific to natural deduction) and with *distinct* explicit substitutions constructs for rules (cut) and ($\Rightarrow_I$), what we dub here *vanilla $\lambda$-terms*.

*Cut Elimination at a Distance: the Vanilla $\lambda$-Calculus.* Once it is clarified that cut-free vanilla proofs are a good formalism for CbV normal forms, one needs to pair them with a natural notion of cut elimination. Quoting Zucker [61]: "we know at the outset what a cut-free derivation is, and the problem is to define the conversions".

For that, we give a very compact definition of cut elimination following the *at a distance* style of rewriting rules promoted by Accattoli and Kesner for natural deduction calculi [10,4,42], and recently shown to be a good fit for the intuitionistic linear logic sequent calculus (without stoup) by Accattoli [1]. To avoid misunderstandings, note that, while rewriting at a distance is also an additional concept, it is fundamentally different from linear or classical logic. Linear and classical logic are *logical* concepts; they change the logic. Rewriting at a distance is a *rewriting* concept, not a logical one; the logic stays the same, what changes is only how proofs/terms are rewritten.

The key point of rewriting at a distance is that it avoids the many rewriting rules propagating explicit substitutions through the term structure, which are found in many extended $\lambda$-calculi, via generalizations of the rewriting rules exploiting contexts (that is, terms with a hole). This is particularly useful in the study of sequent calculi, where commuting cut elimination cases are a notorious burden. Essentially, rewriting at a distance allows one to have only *principal* cut elimination cases, avoiding completely the commutative ones. This is similar to what happens with proof nets, except that it is simpler, because the graphical language is avoided altogether by means of—again—contexts.

Rules at a distance rest on *on-the-fly* decompositions of a term into a context and a sub-term. In our setting, this decomposition becomes the splitting property mentioned above. Distance thus allows for a smooth treatment of values at the rewriting level.

Our proof terms plus cut elimination at a distance form what we dub as the *vanilla $\lambda$-calculus*.

*Results.* The central result of the paper is that two standard translations, from natural deduction to sequent calculus, and back, induce termination-preserving simulations between the vanilla $\lambda$-calculus and one of the formalisms extending Plotkin's CbV. To make things as smooth as possible, our choice of formalism for CbV is Accattoli and Paolini's *value substitution calculus* [13], a natural deduction $\lambda$-calculus with explicit substitutions at a distance, used in various recent studies about CbV [6,5,8,9,12].
For the sake of keeping this fresh perspective light and readable, we focus on explaining the inception of the calculus, rewriting rules at a distance, and the simulation results. As a check of good design for the vanilla $\lambda$-calculus, we also prove strong normalization for typed terms. This result is more challenging than the simulations, but it is expected and proved via an established technique, namely, the bi-orthogonal reducibility method. Therefore, we only give the statements and refer to the technical report [3] for the details of the proof, which is adapted from Accattoli [1].

*How Our Approach Fits in the Literature.* Certainly, ours is not the first computational interpretation of a sequent calculus for MIL, whether vanilla or not. Essentially, there are three kinds of interpretations in the literature. For the first two, we adopt Mint's local / global terminology [44]:

1. **The local approach.** It decorates sequent proofs using a language of terms *without application* and with *let-expressions* (or explicit substitutions) for both the cut rule and the left rule for $\Rightarrow$, as we do. In particular, this approach does *not* use ordinary $\lambda$-terms to decorate proofs. These alternative terms are then endowed with (usually many) rewriting rules mimicking the *propagation* of cuts (that is, they are not at a distance). This approach is followed e.g. by Gallier [33], Ohori [49], Dyckhoff and Lengrand [25,26], and Cerrito and Kesner [16]. Gallier and Cerrito and Kesner do not notice the connection with $CbV$, while Ohori and Dyckhoff and Lengrand do embrace it, but use non-standard sequent calculi and complex sets of rewriting rules. Gallier (1993) revisits standard proof theoretical concepts under the influence of linear logic. Cerrito and Kesner (2004) develop a Curry-Howard for pattern matching. Ohori's (1999) aim is to show a connection between proof theory and Sabry and Felleisen's *A-normal forms* [56,32]. This paper can be seen as a re-elaboration of Ohori's work, where the focus is a minimalistic logical foundation rather than A-normal forms. Our aim is also similar to Dyckhoff and Lengrand [26] (2007) but the outcome is considerably simpler: they have three notions of cut and 14 rewriting rules, while we have only one cut and one rewriting rule.

2. **The global approach.** It amounts to decorate sequent proofs with ordinary $\lambda$-terms and endowing them with call-by-name rewriting. It is rooted in Prawitz's *many-to-one* translation of sequent calculus to natural deduction [54], it possibly first appears with proof terms in Pottinger [53], and it is nicely presented by Barendregt and Ghilezan using the vanilla sequent calculus [15]. The idea is to decorate rules (cut) and ($\Rightarrow_I$) using meta-level substitution, as follows:

$$ \frac{\Gamma \vdash s : A \qquad \Gamma, x : A \vdash t : B}{\Gamma \vdash \{s \to x\} t : B} \text{ cut} $$

$$ \frac{\Gamma \vdash s : A \qquad \Gamma, x : B \vdash t : C}{\Gamma, y : A \Rightarrow B \vdash \{ys \to x\} t : C} \Rightarrow_I $$

The serious drawback of the global approach is the potential *size mismatch* between a sequent calculus proof $\pi$ and the $\lambda$-term $u_\pi$ decorating $\pi$, stemming from the fact that in the sequent calculus the formula $B$ in ($\Rightarrow_I$) can be treated non-linearly, that is, it can be weakened or contracted, leading to duplications/erasures of $ys$. The non-linear use of $B$ is referred to as *the root of all evil* by Danos et al. [21], in their study of representations of System F in linear sequent calculi.
3. The stoup approach. A third approach departs from the vanilla sequent calculus, adopting a form of enriched sequent or adding further judgements to the deductive system. Typically, at the logical level it uses two judgements $\Gamma; \vdash A$ and $\Gamma; B \vdash A$, where the space between the semicolon and $\vdash$ is called stoup—terminology due to Girard [36]—and it is either empty or contains a single, distinguished formula. The non-decorated version of rule ($\Rightarrow_I$) then becomes:

$$ \frac{\Gamma; \vdash A \qquad \Gamma; B \vdash C}{\Gamma; A \Rightarrow B \vdash C} \Rightarrow_I $$

The key point is that the rules of the system (which can be defined in various ways) treat the stoup linearly, that is, the stoup formula is never weakened nor contracted. This fact is what circumvents the size mismatch of the global approach, and thus allows for a good match between sequent proofs with stoup and ordinary $\lambda$-terms. It is usually associated with CbN evaluation.

The stoup approach is first studied by Danos et al. [21], building on Girard [36]. It then became the basis for Herbelin [39], who studies the intuitionistic CbN case, and then Curien and Herbelin [18], who study the classical case in both CbN and CbV, with three judgements and stoup on both sides of the sequent. From [18], it is easy to extract a CbV intuitionistic fragment (as done for instance by Accattoli and Guerrieri [6]), but one obtains a sequent calculus with stoup, not the vanilla one. A different presentation of essentially the same system is the mentioned approach to LJQ by Dyckhoff and Lengrand [25,26], who use two distinct judgements—with one dedicated to values and connected to focalization—rather than the stoup.

Nowadays, a number of works have built over Curien and Herbelin's work, for instance [28,60,29,22,14,48,17,24,23,45], to the point that it became the standard computational interpretation of sequent calculi.

Our work is orthogonal, and somewhat more basic, as it looks at the intuitionistic case without any form of stoup, focalization, or separate judgement.

*Non-Canonicity vs Sharing.* In the proof theoretical literature, the vanilla sequent calculus is often criticized as *non-canonical* because (CbN) normal $\lambda$-terms correspond to more than one cut-free proof, when one embraces the global approach—this is another face of Danos et al.'s *root of all evil* mentioned above.

A key point of our fresh perspective is that this is a *feature* rather than a drawback: it is simply the fact that CbV normal terms such as $let x = yz$ in ($wxxx$) can be seen as *shared* representations of CbN normal forms such as $w(yz)(yz)(yz)$, and that a term can be shared in various ways—another one is $let x = yz$ in ($wxx(yz)$). Therefore, the vanilla sequent calculus gives a first-class status to sub-term sharing for normal forms.

More precisely, *let*-expressions annotate cuts and give a first-class status to sub-term sharing independently of the proof system. The concept of *value* induces a dynamic *l* static refinement of sub-term sharing. Dynamically, only values are *unshared* (that is, duplicated or erased). Non-values are never unshared, thus end up being *statically shared* in normal forms, as in $let x = yz$ in ($wxxx$), making sub-term sharing visible *denotationally*. These two roles are entangled in natural deduction for MIL while they are handled separately in sequent calculus via its two *left rules*, namely cut captures
(NATURAL) λ-CALCULUS

TERMS $Λ_N ∋ t, s ::= x ∈ V_N | λx.t | ts$

ROOT β (λx.t)s ↦→$_β$ {s→x}t

CONTEXTS $C, C' ::= (\cdot) | λx.C | Cs | tC$

CTX CLOSURE
$$ \frac{t \mapsto_{\beta} t'}{C\langle t \rangle \to_{\beta} C\langle t' \rangle} $$

DECORATED (ADDITIVE) NATURAL DEDUCTION

FORMULAS $A, B, C ::= X | A \Rightarrow B$

$$ \frac{\begin{array}{c} \overline{\Gamma, x : A \vdash_N x : A} \\ x : A, \Gamma \vdash_N t : B \\ \Gamma \vdash_N \lambda x.t : A \Rightarrow B \end{array}}{\Gamma \vdash_N t : A \Rightarrow B \qquad \Gamma \vdash_N s : A} \Rightarrow_r \quad @ $$

DETOURS

$$ \frac{\begin{array}{c} x : A, \Gamma \vdash_N t : B \\ \Gamma \vdash_N \lambda x.t : A \Rightarrow B \end{array}}{\Gamma \vdash_N (\lambda x.t)s : B} \Rightarrow_r \quad \begin{array}{c} \Gamma \vdash_N s : A \\ \Gamma \vdash_N \lambda x.t : A \end{array} \quad @ $$

<caption>Fig. 2. λ-calculus and natural deduction $\vdash_N$.</caption>

dynamic sharing and subtraction captures static sharing. Therefore, the left rules of the sequent calculus for MIL encapsulate the sharing features of values.

For an extensive informal discussion about the deep relationship between sharing and CbV see Accattoli's dissemination paper [2].

*Proofs* Omitted proofs are in the associated technical report on arXiv [3].

## 2 Natural Deduction, Call-by-Name, and Rewriting at a Distance

In this section, we give our presentation of Howard's standard correspondence between natural deduction for minimal intuitionistic logic and the simply typed (call-by-name) λ-calculus [41], here also referred to as the *natural λ-calculus*, to distinguish it from the one that shall be associated to the sequent calculus. The correspondence is in Fig. 2. Curiously, in [41] Howard mentions that his work stems from Tait's "discovery of the close correspondence between cut elimination and reduction of λ-terms" [59].

*Routine Definitions: Terms and Contexts.* We assume given a countable set of variables $V_N$, where $N$ stresses that they are for the natural $\lambda$-calculus. The meta-level capture-avoiding substitution of $s$ for $x$ in $t$ is denoted with $\{s \to x\}t$.

Contexts are terms with exactly one occurrence of the *hole* $\langle \cdot \rangle$, an additional constant, standing for a removed sub-term. We shall use various notions of contexts. For the λ-calculus, the most general ones are (*general*) contexts C, which simply allow the hole to be anywhere. The main operation about contexts is *plugging* $C\langle t \rangle$ where the hole $\langle \cdot \rangle$ in context C is replaced by t. Plugging, as usual with contexts, can capture variables—for instance $(\lambda x.\langle \cdot \rangle)t\langle x \rangle = \lambda x.xt$.

*Routine Definitions: Types and Derivations.* Types are built out of an unspecified atomic type X and the implication $\cdot \Rightarrow \cdot$ connective. Type contexts Γ are implicitly considered
<table><tr><td>TERMS</td><td>Λ<sub>N</sub><sup>ES</sup> ∋ t, s ::= x | λx.t | ts | [s→x]t</td></tr><tr><td>CONTEXTS</td><td>C, C' ::= &lt;·&gt; | λx.C | Cs | tC | [C→x]t | [s→x]C</td></tr><tr><td>SUBSTITUTIONS CTXS</td><td>L, L' ::= &lt;·&gt; | [s→x]L</td></tr></table><table><tr><td>ROOT RULES</td><td>CONTEXTUAL CLOSURE</td></tr><tr><td>β AT A DISTANCE</td><td>L&lt;λx.t&gt;s ↦<sub>dB</sub> L&lt;[s→x]t&gt;</td></tr><tr><td>SUBSTITUTION</td><td>[s→x]t ↦<sub>s</sub> {s→x}t</td></tr></table><table><tr><td>Γ ⊢<sub>N</sub> s : A</td><td>Γ, x : A ⊢<sub>N</sub> t : B</td><td>cut</td></tr><tr><td>Γ ⊢<sub>N</sub> [s→x]t : B</td><td></td><td></td></tr></table>

CUT RULE DECORATED WITH AN EXPLICIT SUBSTITUTION

$$ \frac{\Gamma \vdash_N s : A \qquad \Gamma, x : A \vdash_N t : B}{\Gamma \vdash_N [s \to x] t : B} \quad \text{cut} $$

<caption>Fig. 3. Substitution Calculus (SC).</caption>

modulo exchange, that is, $\Gamma$ is a partial function from variables to formulas such that $dom(\Gamma) := \{x | \Gamma(x)$ is defined$\}$ is finite, usually written as $x_1 : A_1, \dots, x_n : A_n$ (with $n \in \mathbb{N}$) if $dom(\Gamma) = \{x_1, \dots, x_n\}$ and $\Gamma(x_i) = A_i$ for $1 \le i \le n$. As it is standard, writing $\Gamma, x : A$ implicitly assumes that $x \notin dom(\Gamma)$.

We write $\pi \triangleright \Gamma \vdash_N t : A$ if $\pi$ is a (type) derivation, that is, a tree constructed using the rules for $\vdash_N$, having axioms as leaves, and of final judgment $\Gamma \vdash_N t : A$.

*Left and Right Rules.* The typing rule ($\Rightarrow_r$) for abstraction carries a right $r$ subscript, to later distinguish it from the left rule for implication of the sequent calculus. We shall constantly refer to left and right rules, and yet we shall dodge abstract definitions of these notions. Rules $ax, \Rightarrow_r$, and $@$ are right rules.

*Detours.* The logical analogues of $\beta$-redexes are *detours*, which are simply given by a $\Rightarrow_r$ rule followed by a $@$ rule, that is exactly what is required to type a $\beta$-redex—see Fig. 2. $\lambda$-terms in normal form are exactly those typed by proofs of $\vdash_N$ without detours.

*Explicit Substitutions.* In Fig. 3, the $\lambda$-calculus is extended with an explicit substitution (shortened to ES) constructor $[s \to x]t$, which binds $x$ in $t$. It can be thought as a more compact notation for let $x = s$ in $t$, with the slight difference that the evaluation order is not fixed in $[s \to x]t$. At the logical level, ESs are decorations for cuts, as shown in Fig. 3. Note that in the literature about $\lambda$-calculi at a distance, ESs are usually rather written using the mirrored construct $t[x \leftarrow s]$. We here prefer to use $[s \to x]t$ because it more faithfully reflects the structure of type derivations.

A point of view underlying our study is that ESs are a form of *sub-term sharing*, meaning that $[t \to x](xx)$ is a version of $tt$ where $t$ is shared.

In this paper, cut shall be considered as a left rule (for its right premise), according to the view outlined at the end of the introduction that left rules account for sharing.
<figure><img src="image_2.png" /><figcaption>Fig. 4. Plotkin's (natural) CbV λ-calculus.</figcaption></figure>

**Rewriting Rules.** We endow natural λ-terms with ESs with small-step rewriting rules, that is, rules based on meta-level substitution, obtaining Accattoli and Kesner's substitution calculus (SC) [11], of rewriting relation $\rightarrow_{\text{SC}}$. It is composed of two rewriting rules, namely the standard substitution rule $\rightarrow_{\text{s}}$, and the perhaps less standard $\beta$ at a distance rule $\rightarrow_{\text{dB}}$. Rule $\rightarrow_{\text{dB}}$ generalizes $\beta$-redexes as to fire even when there are some ESs (i.e. left rules) in between the abstraction and the argument, fact that is formalized in the definition of the rule via the (possibly empty) substitution context $L$ (mnemonic: $L$ stands for *List* of substitutions). For instance,

$$ ([u \to z][s \to y](\lambda x.t))rp \rightarrow_{\text{dB}} ([u \to z][s \to y][r \to x]t)p. \quad (1) $$

This kind of rule circumvents the need of having commuting rewriting rules such as $[s \to y](\lambda x.t) \to \lambda x.[s \to y]t$ or $([s \to y]t)u \to [s \to y](tu)$ in order to expose the $\beta$-redex in (1). The rewriting theory of ESs at a distance has simpler proofs and stronger properties (e.g. residuals) than for commuting-based ESs, see Accattoli and Kesner [10,11,4].

Note that ESs can always be reduced, thus there are no ESs in $\rightarrow_{\text{SC}}$-normal forms. In other words, normal forms are sharing-free.

Clearly, the substitution calculus simulates $\beta$, since $(\lambda x.t)s \rightarrow_{\text{dB}} [s \to x]t \rightarrow_{\text{s}} \{s \to x\}t$.

## 3 The Natural λ-Calculus By Value

In this section, we discuss the presentation of CbV in a natural deduction calculus, first in Plotkin's style and then with cuts / ESs. In particular, we shall see the advantages and the limits of ESs for CbV.

**Plotkin's Call-by-Value and Open Terms.** The definition of CbV à la Plotkin following the modern presentation by Dal Lago and Martini [20] is in Fig. 4. Values $v$ are defined as variables and abstraction, and the $\beta_v$-rule is obtained by restricting $\beta$-redexes to fire only when the argument is a value. Strong evaluation allows one to reduce $\beta_v$-redexes everywhere in a term, and weak evaluation instead forbids $\beta_v$-redexes under abstraction.

It is well-known that Plotkin's approach works smoothly only in the important and yet limited case of weak evaluation of closed terms. Open terms are an issue, and even more so is strong evaluation, because they cause *stuck* $\beta$-redexes such as $(\lambda x.t)(yz)$
TERMS $\Lambda_{\mathbb{N}}^{\text{ES}}$ (as for the SC)

<table><caption>Fig. 5. Value Substitution Calculus (VSC).</caption><thead><tr><th colspan="2">ROOT RULES</th><th>CONTEXTUAL CLOSURE</th></tr></thead><tbody><tr><td>β AT A DISTANCE</td><td>$L(\lambda x.t)s \mapsto_{dB} L([s \to x]t)$</td><td>$a \in \{\text{dB, vs}\}$</td></tr><tr><td>VALUE SUBSTITUTION</td><td>$[L(v) \to x]t \mapsto_{vs} L(\{v \to x\}t)$</td><td>$t \mapsto_a t'$</td></tr><tr><td>NOTATION</td><td>$\to_{VSC} ::= \to_{dB} \cup \to_{vs}$</td><td>$\frac{C(t) \to_a C(t')}{C(t) \to_a C(t')}$</td></tr></tbody></table>

where the argument is $\to \beta_v$-normal and not a value, thus the $\beta_v$-rule cannot fire. These stuck configurations are problematic, as first noticed by Paolini and Ronchi della Rocca [51,50,55]. The easiest way of stating the problem is that the paradigmatic looping term $\Omega := \delta\delta$, where $\delta := \lambda x.xx$, and its variant $\Omega_{\text{stuck}} := (\lambda x.\delta)(yz)\delta$ are contextual equivalent and yet $\Omega$ loops while $\Omega_{\text{stuck}}$ is normal in Plotkin's approach. Terms such as $\Omega_{\text{stuck}}$ are sometimes called *premature normal forms*, and break expected properties of Plotkin's calculus with respect to denotational models, see Accattoli and Guerrieri [7].

Logically, the issue is that not all detours can be eliminated using Plotkin's $\beta_v$-rule.

**Substitutions by Value.** The issue with open terms has been studied at length by Accattoli and Guerrieri and co-authors [6,38,7,8,12], who in [6] study and compare various ways of circumventing it. One of the most flexible and studied solutions amounts to add *ESs at a distance*. The framework is Accattoli and Paolini's *value substitution calculus* (VSC) [13], defined in Fig. 5, which is the variant of the substitution calculus (of the previous section) modelled over the CbV translation of $\lambda$-calculus in linear logic proof nets. The VSC has the same $\beta$ at a distance rule $\to_{\text{dB}}$ of the SC, which does not require the argument to be a value. It has instead a different substitution rule, which is where the value restriction takes place. Its value substitution rule $\to_{\text{vs}}$ uses distance (i.e. the substitution context $L$ around the value $v$). For instance, $[[u \to y]v \to x](zxx) \to_{\text{vs}} [u \to y](zvv)$. Distance allows one to avoid commuting rules such as $[[u \to y]s \to x]t \to [u \to y](s \to x]t$ which are often found in CbV calculi with let-expressions, for instance in Moggi's calculus [46,47], where that rule is called *assoc*.

**Advantages of ESs by Value.** The VSC handles open terms correctly thanks to distance and having moved the value restrictions from $\beta$-redexes to substitution redexes. As evidence of correct behavior, let's have a look at the variant $\Omega_{\text{stuck}}$ of $\Omega$ that is a premature normal form in Plotkin's calculus. It now (correctly) diverges in the VSC:

$$ \begin{align*} \Omega_{\text{stuck}} &:= (\lambda x.\delta)(yz)\delta & \to_{\text{dB}} ([yz \to x]\delta)\delta \\ & \to_{\text{dB}} [yz \to x][\delta \to w](ww) & \to_{\text{vs}} [yz \to x](\delta\delta) & \to_{\text{dB}} \dots \end{align*} $$

The VSC has a number of operational and denotational good properties, as shown by Accattoli and co-authors in various recent works [5,8,12], essentially providing a CbV calculus that mimics in CbV most of the good properties of the CbN $\lambda$-calculus, considerably improving over Plotkin's presentation. At the same time, the VSC and Plotkin's calculus induce the same contextual equivalence on closed terms (see [8]), thus the VSC is a *conservative* refinement of Plotkin's calculus.
$$ \text{VANILLA TERMS} \qquad \Lambda_s \ni t, s, u ::= x \in \mathcal{V}_s | \lambda x.t \mid [[s \to x]]t \mid (y \triangleright s|x)t $$

DECORATED (ADDITIVE) VANILLA SEQUENT CALCULUS

$$ \frac{\begin{array}{c} \Gamma \vdash_S s : A \\ \Gamma \vdash_S [[s \to x]]t : B \end{array}}{\Gamma \cup y : A \Rightarrow B \vdash_S (y \triangleright s|x)t : C} \xrightarrow{\text{cut}} \frac{\begin{array}{c} \Gamma, x : A \vdash_S x : A \\ x : A, \Gamma \vdash_S t : B \\ \Gamma \vdash_S \lambda x.t : A \Rightarrow B \end{array}}{\text{ax}} \xrightarrow{\iota} $$

<caption>Fig. 6. Vanilla $\lambda$-terms and how they decorate the vanilla sequent calculus $\vdash_S$ for MIL.</caption>

*Limits of ESs by Value in Natural Deduction.* The VSC, however, is not free from glitches. In contrast to the CbN case, in the VSC *not all ESs are eliminable*, because of the value constraint. Namely, an ES such as $[yz \to x]t$ cannot be eliminated, since $yz$ is normal and not a value. It might seem that this is the same issue that we pointed out for Plotkin's approach, for which some detours are not eliminable. The situation however is different: in Plotkin's case, ineliminable detours break operational and denotational properties, while ineliminable ESs do not cause similar problems in the VSC.

It is important to stress that—in itself—the presence of ineliminable ESs is not a drawback. They actually are a *feature* of CbV and of the VSC. The fact that some ESs are ineliminable, indeed, means that sub-term sharing ends up in normal forms, and thus becomes *denotationally visible*, which is a good thing, since it opens the way to a mathematical understanding of sharing and efficiency. In Ehrhard's CbV relational denotational model [27], for instance, $[yz \to x](wxx)$ and $w(yz)(yz)$ have *different interpretations*; they instead have the *same interpretation* in the CbN relational model. An extensive high-level discussion of the relationship between sharing and CbV can be found in Accattoli's dissemination paper [2].

The glitch of the VSC is the fact that its ESs are still typed with cuts, as in the SC. Therefore, if some ESs are ineliminable then some cuts are ineliminable, in the CbV interpretation of natural deduction with cuts. This clearly goes against the expected property of the cut rule, which is *admissibility*, that is, that all cuts are eliminable. What happens in the VSC is that only cuts containing values are eliminable.

Ideally, one would like to have two *separate constructors*, one for eliminable cuts and one for ineliminable cuts. This does not seem to be naturally achievable in natural deduction, where the two are entangled. The aim of this paper is to show that, instead, it is exactly what naturally happens in the sequent calculus.

# 4 Proof Terms for the Vanilla Sequent Calculus

Here, we present the sequent calculus for minimal intuitionistic logic (MIL). We adopt an additive presentation of the MIL fragment of Gentzen's original one [34] (which was multiplicative), mimicking the nowadays standard use of additive natural deduction for Howard's correspondence with the $\lambda$-calculus (see e.g. Sørensen and Urzyczyn [58]), despite the fact that Howard's original presentation was multiplicative [41]. The rules are in Fig. 6, which we refer to as *vanilla*, to stress that we do not considered distinguished formulas (also called *stoup*) on the left of sequent symbol $\vdash_S$, nor any other tweak.
The main difference with natural deduction is that the application rule (@) is re-
placed by the left rule (⇒ᵢ) for ⇒ (see Fig. 6, the notation Γ ∪ y : A ⇒ B is explained
below), beyond having the cut rule from the start (while in natural deduction we added
it only at a later moment). For the sequent calculus, we shall re-use most basic concepts
introduced for natural deduction without re-defining them.

Vanilla λ-Terms and the Left Rule for ⇒. We adopt what Mint calls the local approach [44], followed also, for instance, by Gallier [33, Section 10], Dyckhoff and Lengrand [25,26], Ohori [49], and Cerrito and Kesner [16], introducing a language Λ<sub>S</sub> of vanilla λ-terms faithfully coding the structure of sequent proofs. We write the terms of Λ<sub>S</sub> using a different font t, s, u (with respect to the one used for natural λ-terms), also for the variables x, y, z, w, whose set is noted V<sub>S</sub>. The main point of Λ<sub>S</sub> is that there are no applications (which decorate (@) rules). They are replaced by a new constructor (y▷s|x)t, dubbed here subtraction (following Accattoli [1]), and which binds x in t and adds a free occurrence of y. Intuitively, subtraction can be thought of as let x = ys in t (which is the notation used by Gallier [33]) but we prefer to avoid such a notation, for various reasons. Firstly, writing ys we would still be resting on application, while we want to stress that application is not part of the new language, since there is no (@) rule at the logical level. Secondly, in let x = ys in t the two active premises x and s of the (⇒ᵢ) logical rule are given asymmetric roles, while in (y▷s|x)t their roles are symmetric. Thirdly, let-expressions are verbose, thus we adopt a bracket notation.

Note that the typing rule for subtractions uses a new notation Γ ∪ x : A, defined as:

$$
\Gamma \cup x : A := \Gamma, x : A \quad \text{if } x \notin \text{dom}(\Gamma)
$$

$$
\Gamma \cup x : A := \Gamma \quad \text{if } x \in \Gamma \text{ and } \Gamma(x) = A
$$

and it is undefined if $x \in \Gamma$ and $\Gamma(x) \neq A$. The notation is needed because the additive presentation might have to do on-the-fly contractions on the newly introduced formula $A \Rightarrow B$, as for instance in the following case, where the free variable occurrence introduced by rule ($\Rightarrow_I$) is immediately identified with the already existing variable $y$:

$$
\frac{\Gamma \vdash_S s : A \quad \overline{\Gamma, x : B, y : A \Rightarrow B \vdash_S y : A \Rightarrow B}^{ax} \quad \Rightarrow_I}{\Gamma, y : A \Rightarrow B \vdash_S (y \triangleright s | x) y : B}
$$

This phenomenon is not present in natural deduction because therein formulas and vari-
ables are introduced on the left of ⊢_N only by axioms.

Given that weakenings are freely available (in axioms), rule (⇒ᵢ) can alternatively
be formulated without using ∪, as follows:

$$
\frac{\Gamma, y : A \Rightarrow B \vdash_S s : A \quad \overline{\Gamma, x : B, y : A \Rightarrow B \vdash_S t : C}^{\alpha x} \quad \Rightarrow_I}{\Gamma, y : A \Rightarrow B \vdash_S (y \triangleright s | x) t : C}
$$

This approach is adopted for instance by Herbelin [40] and Dyckhoff and Lengrand [26]. We preferred to avoid rule (⇒'ᵢ), however, as we find it counter-intuitive. Yet another equivalent approach is adopting a mixed multiplicative-additive presentation: having the simpler rule (⇒ᵢ) of Fig. 1 that does not use ∪ and adding a stand-alone contraction rule (which is multiplicative) for the left-hand side of ⊢<sub>S</sub>.
<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /><figcaption>**Fig. 7.** Translations between the natural $\lambda$-terms (with ESs) and the vanilla $\lambda$-terms.</figcaption></figure>

*Different Decoration for Cuts.* Another difference between $\Lambda_N$ and $\Lambda_S$ is that, since in $\Lambda_S$ cuts shall play a slightly different role than in the VSC / natural deduction by value, for the sake of clarity we decorate them differently, with $[[s \to x]]_t$ rather than with $[s \to x]_t$.

*Translations.* Translations from the natural $\lambda$-calculus to the vanilla one and vice-versa are given in Fig. 7. They induce translations of the related logical systems, whose key ingredients are highlighted in Fig. 7, namely the simulation of the (@) rule by $\vdash_S$ and the simulation of the ($\Rightarrow_I$) rule by $\vdash_N$. Both translations are obtained by introducing axioms and cuts, and are standard. For instance, Girard's CbN and CbV translations of natural deduction to linear logic [35] are modal decorations of $\sim_S$, and the cuts used in the translation of applications are called *correction cuts* by Danos et al. [21]. Note that the translations preserve (and reflect) values.

*Translation of Cut-Free Vanilla Terms.* We have not yet introduced rewriting rules for vanilla $\lambda$-terms (that is, cut elimination), but there are no doubts about the expected notion of normal vanilla terms: they must be the cut-free ones. The next proposition states the starting observation of this work, that is, the fact that cut-free vanilla terms are mapped to natural terms that are CbV normal, but not necessarily CbN normal.

**Proposition 4.1.** Let $t \in \Lambda_S$ be cut-free. Then $\underline{t}_N$ is $\to_{VSC}$-normal but not necessarily $\to_{SC}$-normal.
*Proof.* By induction on $t$. For $\rightarrow_{VSC}$, simply note that, for cut-free vanilla terms, ESs and applications (which form $\rightarrow_{VSC}$ redexes) are only introduced by the translation of subtractions, and they receive as left sub-terms the application of a free variable to a term: thus the introduced application is not a $\rightarrow_{dB}$-redex, nor it is a value (nor can reduce to one) thus the introduced ES is not a $\rightarrow_{VS}$-redex. For $\rightarrow_{SC}$, the translation of subtraction instead introduces $\rightarrow_S$ redexes. $\square$

In the other direction, $\rightarrow_{VSC}$-normal natural terms are not mapped by $\neg S$ to cut-free vanilla terms, because the translation of applications adds cuts. It is possible to optimize the translation as to avoid this mismatch, but the optimized translations would considerably complicate the translation of contexts (introduced and used in the next sections), which is why we refrain from it. At the same time, we shall show that the translation of normal natural terms are almost cut-free, in a suitable harmless way.

# 5 Defining Cut Elimination for the Vanilla $\lambda$-Calculus

In this section, we define cut elimination on vanilla $\lambda$-terms, obtaining the vanilla $\lambda$-calculus. Our cut elimination shall be based on meta-level substitution. The notion of value shall emerge naturally, and rules at a distance shall play a role.

*Left Variable Occurrences.* At first sight, defining small-step cut elimination for vanilla terms is conceptually easy, since one would simply define it as follows:

$$[\llbracket s \rightarrow x \rrbracket t \rightarrow_{\text{cut}} \llbracket s \rightarrow x \rrbracket t$$

for a notion of meta-level substitution $[\llbracket s \rightarrow x \rrbracket t]$ for vanilla $\lambda$-terms. The problem however is that the definition of $[\llbracket s \rightarrow x \rrbracket t]$ cannot be the same as for natural terms.

In natural deduction, the free occurrences of a variable are introduced by axioms, and axioms can always be replaced by proofs having the same ending sequent. Since we consider axiom as a right rule, let us say that variables have only right occurrences, and that on right occurrences one can always define meta-level substitution $\{u \rightarrow x\}t$ simply as the replacement of $x$ by $u$ in $t$.

On vanilla terms, subtractions $(y \triangleright s | x)t$ introduce left occurrences of $y$. In contrast to right occurrences, the left ones cannot be simply replaced by a vanilla term $u$, because $(u \triangleright s | x)t$ does not belong to the grammar of vanilla terms. Therefore, the definition of meta-level substitution $[\llbracket u \rightarrow x \rrbracket t]$ on vanilla terms is a bit tricky on subtractions.

*Easy Cases and Values.* To define $[\llbracket u \rightarrow x \rrbracket t]$, we have to inspect the shape of $u$. The simplest case is when $u$ is a variable $y$, since in that case it is possible to simply replace $x$ by $y$. A second clear case is when $u$ is an abstraction $\lambda y.s$. Then, we can set:

$$[\llbracket \lambda y.s \rightarrow x \rrbracket (x \triangleright r | z) t := [[[\llbracket \lambda y.s \rightarrow x \rrbracket r \rightarrow y]s \rightarrow z] \llbracket \lambda y.s \rightarrow x \rrbracket t]$$

This complex definition amounts to do the expected elimination of the principal cut between the abstraction and the subtraction (roughly, corresponding to the $\rightarrow_{dB}$ step $(\lambda y.s)r \rightarrow_{dB} [r \rightarrow y]s$ of the (V)SC plus putting the resulting term in a second created cut on $z$ and propagating the substitution $[\llbracket \lambda y.s \rightarrow x \rrbracket]$ to the sub-terms $r$ and $t$ of the
<table><tr><td>TERMS</td><td>Λ<sub>S</sub> ⊃ t, s, u ::= x ∈ V<sub>S</sub> | λx.t | [[s→x]]t | (y▷s|x)t</td></tr><tr><td>VALUES</td><td>v ::= x | λx.t</td></tr><tr><td>CONTEXTS</td><td>C ::= &lang;·&rang; | λx.C | [[t→x]]C | [[C→x]]t | (y▷t|x)C | (y▷C|x)t</td></tr><tr><td>LEFT CTXS</td><td>L ::= &lang;·&rang; | [[t→x]]L | (y▷t|x)L</td></tr></table>

<table><caption>**Fig. 8.** The vanilla λ-calculus.</caption><thead><tr><th colspan="4">META-LEVEL SUBSTITUTION OF VALUES FOR VANILLA TERMS</th></tr></thead><tbody><tr><td>[[v→x]]x := v</td><td>[[v→x]][[s→y]]t := [[[v→x]]s→y][[v→x]]t</td></tr><tr><td>[[v→x]]y := y</td><td>[[v→x]](y▷s|z)t := (y▷[[v→x]]s|z)[[v→x]]t</td></tr><tr><td>[[v→x]]λy.t := λy.[[v→x]]t</td><td>[[y→x]](x▷s|z)t := (y▷[[y→x]]s|z)[[y→x]]t</td></tr><tr><td>[[λy.u→x]](x▷s|z)t := [[[[λy.u→x]]s→y]u→z][[λy.u→x]]t</td><td></td></tr><tr><td colspan="4">ROOT CUT ELIMINATION</td></tr><tr><td>[[L⟨v⟩→x]]t →<sub>cut</sub> L⟨[[v→x]]t⟩</td><td>CTX CLOSURE</td><td>t →<sub>cut</sub> t'<br> C⟨t⟩ ⇄<sub>cut</sub> C⟨t'⟩</td></tr></tbody></table>

subtraction. Note that the two clear cases $u = y$ and $u = λy.s$ are exactly those for values, which correspond to the right rules of $\vdash_S$. The full definition of meta-level substitution $[[v\to x]]t$ for values is in Fig. 8. The following property is proved by induction on $t$.

**Lemma 5.1.** Let $x \notin fv(t)$. Then $[[v\to x]]t = t$.

**The Vanilla λ-Calculus.** For defining small-step cut elimination for all terms, we rely on the crucial observation that every vanilla term $t$ splits uniquely as $t = L⟨v⟩$, where L is a left context—defined in Fig. 8—and $v$ is a value. Note that a similar splitting is also used in the value substitution rule $\to_{vs}$ of the VSC, but there is a key difference: in the VSC applications *cannot* be split as $L⟨v⟩$ (because application is not a left rule), which is why some ESs cannot be eliminated, while all vanilla terms can be split (because application is replaced by subtraction, which is a left rule).

We know how to substitute $v$, and we are left to define what to do with $L$. There are two options, namely mimicking the substitution rules by name (namely $\to_S$) and by value ($\to_{vs}$) for natural terms: either we carry $L$ along with $v$ in the propagation of the substitution, possibly duplicating or erasing it, as in the $CbN$ rule $\to_S$ of the SC, or we commute it out, as in the $CbV$ rule $\to_{vs}$ of the VSC. While in principle both are valid choices, the latter seems more natural because—even if we adopt the $CbN$ approach—cut-free vanilla terms map to $CbV$ normal natural terms, as shown by Proposition 4.1, and *not* to the $CbN$ ones. Essentially, to catch a $CbN$ semantics we should also modify something about cut-free proofs, but that goes against the starting point of our work, namely that vanilla cut-free proofs are a good representation of $CbV$ normal forms.

The cut elimination rule $\rightsquigarrow_{cut}$ is then defined in Fig. 8 by commuting out the left context $L$, completing the definition of the vanilla λ-calculus. Equivalently, one can also set $[[L⟨v⟩→x]]t := L⟨[[v→x]]t⟩$ and $[[s→x]]t \to_{cut} [[s→x]]t$.

**Subject Reduction.** The standard check for the definition of $\rightsquigarrow_{cut}$ is subject reduction.

**Proposition 5.1 (Subject reduction).** Let $t \in \Lambda_S$ and $\pi \vdash \Gamma \vdash_S t: A$ be a derivation. If $t \rightsquigarrow_{cut} s$ then there exists a derivation $\rho \vdash \Gamma \vdash_S s: A$.
*Proof.* Let $t = C(\llbracket L\langle v \rangle \to x \rrbracket u) \rightsquigarrow_{\text{cut}} C(L\langle \llbracket v \to x \rrbracket u \rangle) = s$. The proof is by induction on $u$, $L$, and $C$. Details are in the Appendix of the technical report [3]. □

# 6 Simulating the Vanilla $\lambda$-calculus in the VSC

To simulate the vanilla $\lambda$-calculus in the VSC, we need to look at how the $\to^S$ translation relates the respective notions of meta-level substitution. On vanilla terms, substitution on left variable occurrences does also the work that is done by rule $\to_{dB}$ on the VSC. Unsurprisingly, then, the translation commutes with substitution only up to $\to_{dB}$.

**Lemma 6.1 (Substitution and $\underline{\cdot}_N$ commute up to $\to_{dB}$).** $\{\underline{v}_N \to x\} \underline{t}_N \to^*_{dB} \underline{\langle \underline{v} \to x \rangle} \underline{t}_N$

To establish the simulation, we need a lemma about the commutation of contexts and of the translation. *Technicality*: the translations are extended to contexts by setting $\langle \cdot \rangle_N := \langle \cdot \rangle$ and $\overline{\langle \cdot \rangle}^S_N := \langle \cdot \rangle$, and defining them as for terms on the other cases.

**Lemma 6.2 (Contexts and $\underline{\cdot}_N$ translation).**

1. $\underline{L}_N$ is a $L$ context and $\underline{L\langle t \rangle}_N = \underline{L}_N\langle \underline{t}_N \rangle$.

2. $\underline{C}_N$ is a $C$ context and $\underline{C\langle t \rangle}_N = \underline{C}_N\langle \underline{t}_N \rangle$.

**Proposition 6.1 (VSC simulates vanilla).** If $t \rightsquigarrow^*_{\text{cut}} s$ then $\underline{t}_N \to_{\text{vs}}^* \underline{s}_N$.

*Proof.* For a root step $t = \llbracket L\langle v \rangle \to x \rrbracket u \to_{\text{cut}} L\langle \llbracket v \to x \rrbracket u \rangle = s$, we have:

$$ \begin{align*} \underline{\underline{\underline{L\langle v \rangle \to x \rangle}}} \underline{u}_N &= \underline{\underline{[L\langle v \rangle \to x]}} \underline{u}_N =_{L.6.2.1} \underline{\underline{[\underline{L}_N\langle \underline{v}_N \rangle \to x]}} \underline{u}_N \mapsto_{\text{vs}} \underline{\underline{\underline{L}_N\langle \underline{\{v_N \to x\}} \underline{u}_N \rangle}} \\ (L.6.1) \qquad \to_{\text{dB}}^* \underline{\underline{\underline{L}_N\langle \underline{\{v \to x\}} \underline{u}_N \rangle}} &=_{L.6.2.1} \underline{\underline{\underline{L\langle \underline{\{v \to x\}} \underline{u} \rangle}}} \underline{u}_N. \end{align*} $$

For steps in contexts, the simulation follows from the root case and Lemma 6.2.2. □

Putting together the simulation of cut elimination with the translation of cut-free terms, we obtain the following property.

**Lemma 6.3 (Preservation of VSC termination).** Let $t \rightsquigarrow^*_{\text{cut}} s$ with $s$ cut-free. Then $\underline{t}_N \to^*_{v_{\text{SC}}} \underline{s}_N$ with $\underline{s}_N$ is $\to_{v_{\text{SC}}}$-normal.

*Proof.* By Proposition 6.1, we obtain $\underline{t}_N \to^*_{v_{\text{SC}}} \underline{s}_N$. By Proposition 4.1, $\underline{s}_N$ is a $\to_{v_{\text{SC}}}$-normal form. □

# 7 Simulating the VSC in the Vanilla $\lambda$-Calculus

In the other direction, the translation and meta-level substitution commute neatly.

**Lemma 7.1 (Substitution and $\to^S$ commute).** $\llbracket \overline{v} \to^S x \rrbracket \to^S = \underline{\{v \to x\}} \underline{t}$.

As before, for the simulation we need a lemma about contexts.

**Lemma 7.2 (Contexts and $\to^S$ translation).**
1. $\overline{L}^S$ is an L context and $\overline{L\langle t \rangle}^S = \overline{L}^S \langle \overline{t}^S \rangle$.

2. $\overline{C}^S$ is a C context and $\overline{C\langle t \rangle}^S = \overline{C}^S \langle \overline{t}^S \rangle$.

**Proposition 7.1 (Vanilla simulates VSC).**

1. If $t \xrightarrow{\text{dB}} s$ then $\overline{t}^S \rightsquigarrow_{\text{cut}} \overline{s}^S$.

2. If $t \xrightarrow{\text{vs}} s$ then $\overline{t}^S \rightsquigarrow_{\text{cut}} \overline{s}^S$.

*Proof.* For root steps:

1. $\beta$ at a distance, i.e. $t = L\langle \lambda x.u \rangle r \mapsto_{\text{dB}} L\langle [r \to x]u \rangle = s$. With y and z fresh:

$$
\begin{align*}
\overline{L\langle \lambda x.u \rangle r}^S &= \overline{[L\langle \lambda x.u \rangle \to y] \mathbf{y} \triangleright \overline{r}^S | z \mathbf{z}} \\
&=_{L.6.2.1} \overline{[L^S \langle \lambda x.\overline{u}^S \rangle \to y] \mathbf{y} \triangleright \overline{r}^S | z \mathbf{z}} \\
&\rightsquigarrow_{\text{cut}} \overline{L^S \langle [[\| \lambda x.\overline{u}^S \to y \|] \overline{r}^S \to x] \overline{u}^S \to z \| z \rangle} \\
&=_{L.5.1} \overline{L^S \langle [[\overline{r}^S \to x] \overline{u}^S \to z] \| z \rangle} \\
(\star) \quad &\rightsquigarrow_{\text{cut}} \overline{L^S \langle [\overline{r}^S \to x] \overline{u}^S \rangle} \\
&= \overline{L^S \langle [\overline{r} \to x] u^S \rangle} \qquad =_{L.6.2.1} \overline{L\langle [r \to x] u \rangle}^S
\end{align*}
$$

Where step $(\star)$ is given by the general fact that $[t \to x]x \rightsquigarrow_{\text{cut}} t$, since $t = L\langle v \rangle$ for some L and v, thus $[t \to x]x = [L\langle v \rangle \to x]x \rightsquigarrow_{\text{cut}} L\langle v \rangle = t$.

2. Value substitution, i.e. $t = [L\langle v \rangle \to x]u \mapsto_{\text{dB}} L\langle \{v \to x\}u \rangle = s$. Then:

$$
\begin{align*}
\overline{[L\langle v \rangle \to x]u}^S &= \overline{[L\langle v \rangle^S \to x]u}^S \\
&=_{L.6.2.1} \overline{[L^S \langle \overline{v}^S \rangle \to x]u}^S \\
&\rightsquigarrow_{\text{cut}} \overline{L^S \langle [\| \overline{v}^S \to x \|] \overline{u}^S \rangle} \\
&=_{L.7.1} \overline{L^S \langle \{v \to x\}u \rangle}^S =_{L.6.2.1} \overline{L\langle \{v \to x\}u \rangle}^S
\end{align*}
$$

For steps in contexts, the simulation follows from the root case and Lemma 7.2.2. $\square$

<figure><img src="image_6.png" /></figure>

*Translation of Normal Natural Terms.* As anticipated in Sect. 5, the translation of normal VSC terms does not give cut-free vanilla terms, because the translation of applications introduces cuts. Here we show that nonetheless the obtained terms are almost cut-free, since they are cut-free up to some trivial cut elimination steps, dubbed renaming steps. In particular, they strictly reduce the size of a vanilla term.

**Definition 1 (Renaming Cut Elimination Steps).** A step $t = C\langle [L\langle v \rangle \to x]u \rangle \rightsquigarrow_{\text{cut}} C\langle L\langle [v \to x]u \rangle \rangle = s$ is a renaming step, noted $t \rightsquigarrow_{\text{ren-cut}} s$, if v is a variable.

**Proposition 7.2 (The $\overline{t}^S$ translation of VSC normal forms is almost cut-free).** Let $t \in \Lambda_N^{\text{ES}}$ be $\to_{\text{VSC}}$-normal. Then there exists a cut-free such that $\overline{t}^S \rightsquigarrow_{\text{ren-cut}}^k t$ with $k \le |t|$, where $|t|$ is the size (i.e. number of constructors) in t.

<figure><img src="image_7.png" /></figure>
As for the other direction, we can put together the simulation and the translation of normal forms, obtaining the preservation of termination by $\bar{s}$.

**Lemma 7.3 (Preservation of termination).** Let $t \to_{vSC}^* s$ with $s \to_{vSC} \text{-normal}$. Then there exists a cut-free term $s$ such that $\bar{t} \stackrel{*}{\rightleftharpoons}_{cut} \bar{s}$.

*Proof.* By Proposition 7.1, we obtain $\bar{t} \stackrel{S}{\rightleftharpoons}^*_{cut} \bar{s}$. By Proposition 7.2, there exists $s$ cut-free such that $\bar{s} \stackrel{*}{\rightleftharpoons}_{cut} s$. $\square$

# 8 Strong Normalization

The typical theorem for Curry-Howard correspondences is that the logical system ensures strong normalization of the typed terms. We provide such a result for our new correspondence between the vanilla $\lambda$-calculus and the vanilla sequent calculus.

In this section, we give only the statement, since the proof is too technical for a fresh perspective paper. The proof is developed in sections D and E of the Appendix of the technical report [3], and is based on the bi-orthogonal reducibility method, adapting and slightly simplifying its presentation in Accattoli [1].

**Definition 2 (Strong normalization).** A vanilla term $t$ is strongly normalizing, also noted $t \in \mathit{SN}_{cut}$, if $t \stackrel{*}{\rightleftharpoons}_{cut} s$ implies $s \in \mathit{SN}_{cut}$.

**Theorem 1 (Typable terms are SN).** Let $t \in \Lambda_S$ and $\Gamma \vdash_S t : A$. Then $t \in \mathit{SN}_{cut}$.

# 9 Conclusions

We introduced the *vanilla* $\lambda$-calculus, a computational interpretation of the simplest sequent calculus, and showed that it simulates and it is simulated by call-by-value evaluation. Technically, the simulations are clean and compact, thanks to the use of rewriting rules at a distance for both the new cut elimination rule for the vanilla $\lambda$-calculus and the presentation of call-by-value evaluation that we adopt from the literature.

Our study nicely complements the two famous cornerstones by Curry and Howard about minimal intuitionistic logic resting only on basic logical concepts:

1. *Curry 1958* [19]: Hilbert's system matches combinatorial logic;

2. *Howard 1969* (but published only in 1980) [41]: Gentzen's natural deduction mirrors the (call-by-name) $\lambda$-calculus;

3. *Here*: Gentzen's sequent calculus matches call-by-value evaluation.

We believe that our work provides a fresh perspective over the sequent calculus. Its modern computational interpretation is usually defined starting from sequent calculi with stoups for classical logic, following Curien and Herbelin [18]. The basic, *vanilla* presentation of the intuitionistic case seems to have fallen into a blind spot of the literature. This work shows that it is far from being unworthy of attention.

*Future Work.* Maraist et al. [43] propose a Curry-Howard correspondence for *call-by-need* using an affine logic with a duplication modality, tweaking the linear logic one for call-by-value. In ongoing work, we are using the results of this paper as the starting point for a Curry-Howard for call-by-need that is *not* based on linear/affine concepts.
References

1. Accattoli, B.: Exponentials as substitutions and the cost of cut elimination in linear logic. Log. Methods Comput. Sci. 19(4) (2023). https://doi.org/10.46298/LMCS-19(4:23)2023

2. Accattoli, B.: Sharing a perspective on the λ-calculus. In: van der Storm, T., Hirschfeld, R. (eds.) Proceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2023, Cascais, Portugal, October 25-27, 2023. pp. 179–190. ACM (2023). https://doi.org/10.1145/3622758.3622884

3. Accattoli, B.: The vanilla sequent calculus is call-by-value (2024), https://arxiv.org/abs/2409.19722

4. Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014. pp. 659–670. ACM (2014). https://doi.org/10.1145/2535838.2535886

5. Accattoli, B., Condoluci, A., Sacerdoti Coen, C.: Strong call-by-value is reasonable, implosively. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1–14. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470630

6. Accattoli, B., Guerrieri, G.: Open call-by-value. In: Igarashi, A. (ed.) Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings. Lecture Notes in Computer Science, vol. 10017, pp. 206–226 (2016). https://doi.org/10.1007/978-3-319-47958-3_12

7. Accattoli, B., Guerrieri, G.: Types of fireballs. In: Ryu, S. (ed.) Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11275, pp. 45–66. Springer (2018). https://doi.org/10.1007/978-3-030-02768-1_3

8. Accattoli, B., Guerrieri, G.: The theory of call-by-value solvability. Proc. ACM Program. Lang. 6(ICFP), 855–885 (2022). https://doi.org/10.1145/3547652

9. Accattoli, B., Guerrieri, G., Leberle, M.: Strong call-by-value and multi types. In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T. (eds.) Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru, December 4-8, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14446, pp. 196–215. Springer (2023). https://doi.org/10.1007/978-3-031-47963-2_13

10. Accattoli, B., Kesner, D.: The structural λ-calculus. In: Dawar, A., Veith, H. (eds.) Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6247, pp. 381–395. Springer (2010). https://doi.org/10.1007/978-3-642-15205-4_30

11. Accattoli, B., Kesner, D.: The permutative λ-calculus. In: Bjørner, N.S., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7180, pp. 23–36. Springer (2012). https://doi.org/10.1007/978-3-642-28717-6_5

12. Accattoli, B., Lancelot, A.: Light genericity. In: Kobayashi, N., Worrell, J. (eds.) Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II. Lecture Notes in Computer Science, vol. 14575, pp. 24–46. Springer (2024). https://doi.org/10.1007/978-3-031-57231-9_2
13. Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7294, pp. 4-16. Springer (2012). https://doi.org/10.1007/978-3-642-29822-6\_4

14. Ariola, Z.M., Herbelin, H., Saurin, A.: Classical call-by-need and duality. In: Ong, C.L. (ed.) Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6690, pp. 27-44. Springer (2011). https://doi.org/10.1007/978-3-642-21691-6\_6

15. Barendregt, H., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program. **10**(1), 121-134 (2000). https://doi.org/10.1017/S0956796899003524

16. Cerrito, S., Kesner, D.: Pattern matching as cut elimination. Theor. Comput. Sci. **323**(1-3), 71-127 (2004). https://doi.org/10.1016/J.TCS.2004.03.032

17. Curien, P., Fiore, M.P., Munch-Maccagnoni, G.: A theory of effects and resources: adjunction models and polarised calculi. In: Bodík, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016. pp. 44-56. ACM (2016). https://doi.org/10.1145/2837614.2837652

18. Curien, P., Herbelin, H.: The duality of computation. In: Odersky, M., Wadler, P. (eds.) Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000. pp. 233-243. ACM (2000). https://doi.org/10.1145/351240.351262

19. Curry, H., Feys, R.: Combinatory Logic. No. 1 in Studies in logic and the foundations of mathematics, North-Holland Publishing Company (1958)

20. Dal Lago, U., Martini, S.: The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. **398**(1-3), 32-50 (2008). https://doi.org/10.1016/J.TCS.2008.01.044

21. Danos, V., Joinet, J.B., Schellinx, H.: LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 211-224. No. 222 in London Mathematical Society Lecture Note Series, Cambridge University Press (1995). https://doi.org/10.1017/CBO9780511629150

22. Dougherty, D.J., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the curien-herbelin symmetric lambda calculus: Extending the coppo-dezani heritage. Theor. Comput. Sci. **398**(1-3), 114-128 (2008). https://doi.org/10.1016/J.TCS.2008.01.022

23. Downen, P., Ariola, Z.M.: A tutorial on computational classical logic and the sequent calculus. J. Funct. Program. **28**, e3 (2018). https://doi.org/10.1017/S0956796818000023

24. Downen, P., Maurer, L., Ariola, Z.M., Peyton Jones, S.: Sequent calculus as a compiler intermediate language. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. pp. 74-88. ACM (2016). https://doi.org/10.1145/2951913.2951931

25. Dyckhoff, R., Lengrand, S.: LJQ: A strongly focused calculus for intuitionistic logic. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings. Lecture Notes in Computer Science, vol. 3988, pp. 173-185. Springer (2006). https://doi.org/10.1007/11780342\_19

26. Dyckhoff, R., Lengrand, S.: Call-by-value lambda-calculus and LJQ. J. Log. Comput. **17**(6), 1109-1134 (2007). https://doi.org/10.1093/LOGCOM/EXM037
27. Ehrhard, T.: Collapsing non-idempotent intersection types. In: Cégielski, P., Durand, A. (eds.) Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France. LIPIcs, vol. 16, pp. 259–273. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012). https://doi.org/10.4230/LIPICS.CSL.2012.259

28. Espírito Santo, J.: Revisiting the correspondence between cut elimination and normalisation. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1853, pp. 600–611. Springer (2000). https://doi.org/10.1007/3-540-45022-X_51

29. Espírito Santo, J.: Completing Herbelin’s programme. In: Rocca, S.R.D. (ed.) Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4583, pp. 118–132. Springer (2007). https://doi.org/10.1007/978-3-540-73228-0_10

30. Espírito Santo, J., Pinto, L., Uustalu, T.: Plotkin’s call-by-value λ-calculus as a modal calculus. J. Log. Algebraic Methods Program. **127**, 100775 (2022). https://doi.org/10.1016/J.JLAMP.2022.100775

31. Filinski, A.: Declarative continuations: an investigation of duality in programming language semantics. In: Pitt, D.H., Rydeheard, D.E., Dybjer, P., Pitts, A.M., Poigné, A. (eds.) Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings. Lecture Notes in Computer Science, vol. 389, pp. 224–249. Springer (1989). https://doi.org/10.1007/BFB0018355

32. Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Cartwright, R. (ed.) Proceedings of the ACM SIGPLAN’93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993. pp. 237–247. ACM (1993). https://doi.org/10.1145/155090.155113

33. Gallier, J.H.: Constructive logics part I: A tutorial on proof systems and typed lambda-calculi. Theor. Comput. Sci. **110**(2), 249–339 (1993). https://doi.org/10.1016/0304-3975(93)90011-H

34. Gentzen, G.: Investigations into logical deduction. American Philosophical Quarterly **1**(4), 288–306 (1964), http://www.jstor.org/stable/20009142

35. Girard, J.: Linear logic. Theor. Comput. Sci. **50**, 1–102 (1987). https://doi.org/10.1016/0304-3975(87)90045-4

36. Girard, J.: A new constructive logic: Classical logic. Math. Struct. Comput. Sci. **1**(3), 255–296 (1991). https://doi.org/10.1017/S0960129500001328

37. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: (ICFP ’02). pp. 235–246 (2002). https://doi.org/10.1145/581478.581501

38. Guerrieri, G., Paolini, L., Ronchi Della Rocca, S.: Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods in Computer Science **13**(4) (2017). https://doi.org/10.23638/LMCS-13(4:29)2017

39. Herbelin, H.: A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers. Lecture Notes in Computer Science, vol. 933, pp. 61–75. Springer (1994). https://doi.org/10.1007/BFb0022247

40. Herbelin, H.: Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes. Ph.D. thesis, University Paris 7 (Jan 1995)
41. Howard, W.A.: The formulae-as-types notion of construction. In: Curry, H., B., H., Roger, S.J., Jonathan, P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press (1980), Notes written in 1969 and published only in 1980.

42. Kesner, D.: A fine-grained computational interpretation of girard's intuitionistic proof-nets. Proc. ACM Program. Lang. 6(POPL), 1-28 (2022). https://doi.org/10.1145/3498669

43. Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci. 228(1-2), 175-210 (1999). https://doi.org/10.1016/S0304-3975(98)00358-2

44. Mints, G.: Three faces of natural deduction. In: Galmiche, D. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '97, Pont-à-Mousson, France, May 13-16, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1227, pp. 16-30. Springer (1997). https://doi.org/10.1007/BFB0027402

45. Miquey, É.: A classical sequent calculus with dependent types. ACM Trans. Program. Lang. Syst. 41(2), 8:1-8:47 (2019). https://doi.org/10.1145/3230625

46. Moggi, E.: Computational λ-Calculus and Monads. LFCS report ECS-LFCS-88-66, University of Edinburgh (1988), http://www.lfcs.inf.ed.ac.uk/reports/88/ECS-LFCS-88-66/ECS-LFCS-88-66.pdf

47. Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989. pp. 14-23. IEEE Computer Society (1989). https://doi.org/10.1109/LICS.1989.39155

48. Munch-Maccagnoni, G., Scherer, G.: Polarised intermediate representation of lambda calculus with sums. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. pp. 127-140. IEEE Computer Society (2015). https://doi.org/10.1109/LICS.2015.22

49. Ohori, A.: A curry-howard isomorphism for compilation and program execution. In: Girard, J. (ed.) Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1581, pp. 280-294. Springer (1999). https://doi.org/10.1007/3-540-48959-2_20

50. Paolini, L.: Call-by-value separability and computability. In: Restivo, A., Ronchi Della Rocca, S., Roversi, L. (eds.) Theoretical Computer Science, 7th Italian Conference, ICTCS 2001, Torino, Italy, October 4-6, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2202, pp. 74-89. Springer (2001). https://doi.org/10.1007/3-540-45446-2_5

51. Paolini, L., Ronchi Della Rocca, S.: Call-by-value solvability. RAIRO Theor. Informatics Appl. 33(6), 507-534 (1999). https://doi.org/10.1051/ITA:1999130

52. Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125-159 (1975). https://doi.org/10.1016/0304-3975(75)90017-1

53. Pottinger, G.: Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic 12(3), 323-357 (1977). https://doi.org/10.1016/S0003-4843(77)80004-1

54. Prawitz, D.: Natural deduction. A proof-theoretical study. Almqvist & Wiksell (1965). https://doi.org/10.2307/2271676

55. Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https://doi.org/10.1007/978-3-662-10394-4

56. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: White, J.L. (ed.) Proceedings of the Conference on Lisp and Functional Programming, LFP 1992, San Francisco, California, USA, 22-24 June 1992. pp. 288-298. ACM (1992). https://doi.org/10.1145/141471.141563
57. Scherer, G., Rémy, D.: Full reduction in the face of absurdity. In: Vitek, J. (ed.) Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9032, pp. 685-709. Springer (2015). https://doi.org/10.1007/978-3-662-46669-8_28

58. Sørensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard isomorphism. Elsevier (2006). https://doi.org/10.5555/1197021

59. Tait, W.: Infinitely long terms of transfinite type. In: Crossley, J., Dummett, M. (eds.) Formal Systems and Recursive Functions, Studies in Logic and the Foundations of Mathematics, vol. 40, pp. 176-185. Elsevier (1965). https://doi.org/10.1016/S0049-237X(08)71689-6

60. Wadler, P.: Call-by-value is dual to call-by-name. In: Runciman, C., Shivers, O. (eds.) Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003. pp. 189-201. ACM (2003). https://doi.org/10.1145/944705.944723

61. Zucker, J.: The correspondence between cut-elimination and normalization. Annals of Mathematical Logic 7(1), 1-112 (1974). https://doi.org/10.1016/0003-4843(74)90010-2

**Open Access.** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution, and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.