Call-By-Push-Value

2025-08-01

Introduction

Syntax

Types and Terms

1 Introduction

Call-by-push-value (CBPV) is a generalisation to call-by-name (CBN) and call-by-value (CPV). This programming language paradigm is based on the slogan "a value is, a program does" and is equipped with a type theory, operational semantics, and denotational models. A calculus for CBPV was first presented in Paul Blain Levy's PhD thesis. This note summerises parts of the thesis.

2 Syntax

In CBPV we distinguish between computations and values. Hence there are two disjoint kinds of types: a computation has a computation type, and a value has a value type.

2.1 Types and Terms

The syntax of types and terms are given in Figure 1. We omit the ground types and values (e.g. booleans) and prospone the discussion in Remark B.

Types

Terms

Figure 1: Syntax for types and terms

Once we get to the semantics and equational theory, we will see that the let-bindings are essentially syntax sugars for lambda application (e.g. is equivalent to ). Nonetheless, the intuition behind the other terms are explained as follows. Notice the a value is, a computation does principle.

Remark 21A (A value is, a computation does).

is the thunk of a computation .

Suppose there is an operand-stack of values and tags.

produces the value .
behaves as where is the thunk of .
pops a value from the stack, then behaves as .
pushes to the stack, then behaves as .

Observe that only a value can be pushed or popped. However, we can "freeze" a computation into a value; this value is called the thunk of . Later, when desired, this thunk can be forced (i.e. executed).

Remark 21B (Ground values and types).

We can extend value types with ground types by adding the unit type and sum type for some countable index . For instance, we can define .

The only term of type is , and by an abuse of notation, terms of are simply denoted for . We call these terms ground values.

2.2 Judgments

Since we have two kinds of types, the judgments in the calculus are

and the type system is given in Figure 2.

Figure 2: Type system

3 Semantics

We present a big-step semantics that can reduce all closed computation to a terminal computation. Intuitively, a terminal computation cannot proceed if the operand-stack is empty.

Definition 3A (Terminal computation).

A closed computation is terminal if it is in the form

Let denote the set of closed computation of type , and denote the set of terminal computations. The big-step semantics presented in Figure 3 defines a (total) function from to .

Figure 3: Big-step semantics

4 Equational Theory

Based on the big-step semantics, we can derive an equational theory and recover laws such as the -reduction and -conversion. Formally, we define new judgments

to express judgmental equalities. However, we adopt the following conventions.

We assume all the conditions needed to well-type each side of an equation, and to make sure that the two sides havve the same context and type.
If a metasyntactic variable occurs in the scope of an variable binder, then we assume that is not in the context of .¹

The laws are grouped into - and -laws in Figure 4, and sequencing laws in Figure 5.

Figure 4: -laws (left) and -laws (right)

Figure 5: Sequencing laws

5 CBV to CPBV

todocbv and semantics for cbv

The most important difference between CBV and CPBV is that is a value in CBV whereas in CPBV its a computation. Thus is translated to in CBPV.

notice that