The hidden exception handler of Parigot’s λμ-calculus and its completeness properties

Observationally (Böhm) complete

↑

Saurin’s extension of λμ-calculus = call-by-name Danvy-Filinski shift-reset “calculus”
↓

call-by-value version complete for representing syntactic monads (exceptions, references, ...)

Contents

A tour of computational classical logic

- callcc vs try-with

- Operational semantics: the need for tp

- Felleisen λ_{C}-calculus and Parigot λμ-calculus

- Curry-Howard and classical logic

- Danvy-Filinski shift/reset calculus vs extending λμ with (pure) try

Böhm completeness

- David-Py incompleteness of λμ-calculus vs Saurin’s observational completeness

- Saurin’s calculus = call-by-name λμ + pure try = call-by-name shift/reset calculus

Part I Computing with classical logic

(a tour of callcc, A, C, try-with/raise, shift/reset, μ, μ̂, ...)

Computing with callcc and ptry

exception Result of int let product l = try let rec aux = function | []     -> 1 | 0 :: l -> raise (Result 0) | n :: l -> n * aux l in aux l with Result n -> n ptry sets a marker and an associated handler in the evaluation stack and raise jumps to the nearest enclosed marker. ≃ let product l = callcc (fun k => let rec aux = function | []     -> 1 | 0 :: l -> throw k 0 | n :: l -> n * aux l in aux l) callcc memorises the evaluation stack and throw restores the memorised evaluation stack

ptry binds raise dynamically

exception Result of int let product l = try let rec aux = function | []     -> 1 | 0 :: l -> raise (Result 0) | n :: l -> n * aux l in aux l with Result n -> n = exception Result of int let product l = let rec aux = function | []     -> 1 | 0 :: l -> raise (Result 0) | n :: l -> n * aux l in try aux l with Result n -> n

callcc binds its corresponding throw statically

let product l = callcc (fun k => let rec aux = function | []     -> 1 | 0 :: l -> throw k 0 | n :: l -> n * aux l in aux l)  ≠  let product l = let rec aux = function | []     -> 1 | 0 :: l -> throw k 0 | n :: l -> n * aux l in callcc (fun k => aux l) which is syntactically ill-formed!

A primitive form of try-with: ptry

Syntax

t ::= V | t t | raise t | ptry t  (terms)
V ::= x | λx.t  (values)
F ::= □ | F [V □] | F [□ t] | F [raise □]  (local evaluation contexts)
E ::= □ | E[ptry F]  (global evaluation contexts)

Operational Semantics (aka weak-head reduction)

E[(λx.t) u]  → E[t[u/x]]
E[ptry F [raise V]] → E[V]
E[ptry V]  → E[V]

Simulation of ptry/raise from Ocaml’s try-with/raise

raise t  ≜ raise (Exc t)
ptry t  ≜ try t with Exc x → x

Simulation of OCaml’s try-with/raise from ptry/raise

raise t  ≜ raise t
try t with E x → u ≜ match (ptry (Val t)) with Val x → x | E x → u | e → raise e

Typing callcc/throw and ptry/raise

(standard presentation)

Γ, k : cont A ⊢ t : A

Γ ⊢ callcc (fun k → t) : A

Γ, k : cont A ⊢ t : A
Γ, k : cont A ⊢ throw k t : B

Γ ⊢ t : exn

       Γ ⊢ ptry t : exn

Γ ⊢ t : exn

                        Γ ⊢ raise t : B

Typing callcc/throw and ptry/raise

(generalising the type of exceptions)

Γ, k : cont A ⊢ t : A

Γ ⊢ callcc (fun k → t) : A

Γ, k : cont A ⊢ t : A

Γ, k : cont A ⊢ throw k t : B

\begin{matrix}Γ ⊢ t : A \\ Γ ⊢ ptry t : A \end{matrix} \begin{matrix}Γ ⊢ t : A \\ Γ ⊢ raise t : B \end{matrix}

Typing callcc/throw and ptry/raise

(naming the dynamic ptry continuation)

Γ, k : cont A ⊢ t : A

Γ ⊢ callcc (fun k → t) : A

Γ, k : cont A ⊢ t : A
Γ, k : cont A ⊢ throw k t : B

Γ, tp: cont A ⊢ t : A Γ, tp: cont T ⊢ ptrytp t : A

Γ, tp: cont A ⊢ t : A

Γ, tp: cont A ⊢ raisetp t : B

Typing callcc/throw and ptry/raise

(naming the dynamic ptry continuation)

Γ, k : cont A ⊢ t : A

Γ ⊢ callcc (fun k → t) : A

Γ, k : cont A ⊢ t : A
Γ, k : cont A ⊢ throw k t : B

Γ, tp: cont A ⊢ t : A Γ, tp: cont T ⊢ ptrytp t : A

Γ, tp: cont A ⊢ t : A

Γ, tp: cont A ⊢ raisetp t : B

Generalisation of the type of ptry needs type effects on arrows to ensure the type correctness of dynamic binding:

Γ, tp: cont T ⊢ t : A →_{T} B Γ, tp: cont T ⊢ u : A Γ, tp: cont T ⊢ t u : B

Γ, x : B, tp: cont T ⊢ t : C
Γ, tp: cont U ⊢ λx.t : B →_{T} C
Γ, x : A, tp: cont T ⊢ x : A

Simple types: callcc is more expressive than ptry

(computing with infinity)

E.g. proof of ∀f : (nat → bool) ∃b : bool ∀m ∃n ≥ n f(m) = b

let pseudo_decide_infinity f =
  callcc (fun k -> (true, fun m1 ->
    callcc (fun k1 -> throw k (false (fun m2 ->
      callcc (fun k2 ->
        let n = max m1 m2 in
        if f n then throw k1 n else throw k2 n))))))

This is executable in SML, Objective Caml (and Scheme).

Any program whose result is a non-functional value and that uses pseudo_decide_infinity will yield a (correct) result.

Each call to throw will induce backtracking on the progress of the program that uses pseudo_decide_infinity.

Simple types: callcc is more expressive than ptry

(drinkers’ paradox)

E.g. proof of ∀P : (human → Prop) ∃x : human ∀y : human, P x → P y

(* drinkers : human * (human -> 'a -> 'a)
let drinkers =
  callcc (fun k -> (adam, fun y px ->
    callcc (fun k' -> throw k (y, fun y' py -> throw k' py))))

Simple types: ptry is more expressive than callcc

Derivation of a fixpoint using exceptions of functional type:

type dom = unit -> unit
(* lam : (dom -> dom) -> dom *)
let lam f   = fun () -> raise f
(* app : dom -> dom -> dom *)
let app t u = (ptry (let () = t () in t)) u
(* delta : dom *)
let delta = lam (fun x -> app x x)
(* omega : dom *)
let omega = app delta delta

Typing ptry shows that it raises exceptions of type dom ≜ unit →_{dom} unit which is a recursive type.

Which possible Curry-Howard interpretation for ptry/raise?

How to interpret type effects in the logical framework? Use a canonical type effect? Use ⊥? Type ptry/raise with the rules

Γ, tp: cont ⊥ ⊢ t : ⊥

Γ, tp: cont ⊥ ⊢ ptrytp t : ⊥

Γ, tp: cont ⊥ ⊢ t : ⊥

Γ, tp: cont ⊥ ⊢ raisetp t : B

The Curry-Howard interpretation for callcc

We have λx.callcc(λk.x k) : ((A → B) → A) → A which corresponds to Peirce law Minimal logic + Peirce law is called minimal classical logic λ-calculus + callcc and its reduction semantics corresponds to minimal classical logic

The hidden toplevel of callcc operational semantics

# let y = callcc (fun k -> fun x -> throw k (fun y -> x+y));;
val y : int -> int = <fun>
# y 3;;
val y : int -> int = <fun> (* !!!! *)

The reason is that the continuation of the definition of y is “print the value of y”. Let’s call it k_{0}.

The value of y is fun x -> throw k_{0} (fun y -> x+y).

When y is applied, throw is called and it returns to k_{0}.

Conventionally, this semantics is expressed using an abortion operator A which itself hides a call to the toplevel continuation.

Intermezzo: Felleisen’s C operator

Motivated by the possibility to reason on operators such as callcc in Scheme, Felleisen et al introduced the C operator.

Syntax

t ::= x | λx.t | t t | C(λk.t)

C is equivalent to the combination of callcc and A. C(λk.t) = callcc(λk.A t) callcc(λk.t) = C(λk.k t) A t = C(λ_.t)

Remark: in C(λk.t), “λk.” is part of the syntax. Alternative equivalent definitions of the language are

t ::= x | λx.t | t t | C t

or

t ::= x | λx.t | t t | C

Parigot’s λμ-calculus

(minimal version)

Use special variables α, β for denoting continuations.

Syntax

t ::= V | t t | μα.c  (terms)
c ::= [β]t  (commands or states)
V ::= x | λx.t  (values)

Use structural substitution for continuations:

E[μα.c] → μα.c[[α]E/[α]□]

More concisely:

E[μα.c] → μα.c[[α]E/α]

Parigot’s λμ-calculus

(expressing callcc)

callcc is approximable:

callcc(λk.(… k t …)) ≃ μk.[k](… [k]t …)

In fact, the actual operational semantics of callcc is:

E[callcc(λk.t)] → t[λx.A(E[x])/k] (∗)

The previous approximation of callcc is “too efficient” compared to the actual semantics (such as implemented in Scheme). The correct simulation, in Scheme, is

callcc ≜ λz.μα.[α](z λx.μ_.[α]x)

which corresponds to an operator of reification of the evaluation context as a function.

Yet, the full semantics of callcc above requires A and λμ-calculus is not strong enough to express it. Especially, it is not strong enough to simulate the capture of the toplevel continuation performed by the toplevel rule (∗) above.

Parigot’s λμ-calculus

(adding a denotation for the toplevel continuation)

Syntax

t ::= V | t t | μα.c (terms)
c ::= [β]t | [tp]t (commands or states)
V ::= x | λx.t  (values)

The operator A can now be expressed: A ≜ λx.μ_.[tp]x and the toplevel reduction rule of callcc gets simulable:

[tp] E[callcc(λk.t)] ≡ [tp]E[(λz.μα.[α](z λx.μ_.[α]x)) λk.t]
↓∗
[tp] E[t[λx.A(E[x])/k]] ≡ [tp] E[t[λx.μ_.[tp]E[x]/k]]

λμ-calculus extended with tp can faithfully simulate callcc or Felleisen’s λ_{C}-calculus. Moreover, it

- is able to substitute continuations directly as evaluation contexts

- allows notations for continuation constants

- is able to express states of abstract machine (tp plays the rôle of the bottom of the stack)

- has nice reduction and operational properties (almost as nice as \overline{λ}μμ̃!) [Ariola-Herbelin 2007] An example of “inefficiency” in call-by-value:

let loop() = callcc(λk.k(loop())) : loop()  → (λx.Ax) (loop()) → (λx.Ax) ((λx.Ax) (loop())) → …
let loop() = μk.[k](loop()) :  [tp](loop()) → [tp]loop())  → [tp](loop())  → …

Danvy and Filinski’s shift and reset [1989]

The operator reset locally “resets” the toplevel and delimits the current continuation of a computation. The operator shift captures the current delimited continuation and composes it with the continuation at the places it is invoked.

Syntax

t ::= V | t t | S(λk.t) | ⟨t⟩  (terms)
V ::= x | λx.t  (values)
F □ ::= □ | F [V □] | F [□ t]  (local ev. contexts)
E□ ::= □ | E[resetF □]  (global ev. contexts)

Historically, the semantics of shift/reset was defined by continuation-passing-style translation (CPS). Its operational semantics is now well established.

Operational Semantics

\begin{aligned}E[(λx.t) u] & → & E[t[u/x]] \\ E[⟨F [S(λk.t)]⟩] & → & E[⟨t[λx.⟨F [x]⟩/k]⟩] \\ E[⟨V ⟩] & → & E[V] \end{aligned}

Application: normalisation by evaluation with boolean type [Danvy 1996]

type term =
| Abs of string * term
| Var of string | App of term * term
| True | False | If of term * term * term
type types =
| Atom                            (* |Atom|         = term         *)
| Arrow of types * types          (* |Arrow(T1,T2)| = |T1| -> |T2| *)
| Bool                            (* |Bool|         = bool         *)
(* up : (T:types)term(T)->|T| *)
let rec up tt t = match tt with
| Atom            -> t
| Arrow (tt1,tt2) -> fun x -> up tt2 (App (t,down tt1 x))
| Bool            -> shift (fun k -> If (t,k true,k false)
(* down : (T:types)|T|->term(T) *)
and down tt mt = match tt with
| Atom            -> mt
| Arrow (tt1,tt2) -> let s = fresh () in
                    Abs (s,reset (down tt2 (mt (up tt1 (Var s)))))
| Bool            -> if mt then True else False

Filinski [1994]: shift/reset can simulate all concrete monads in direct style

(the example of references)

The monad that simulates a reference of type S

T (A) = S → A × S
η = λx.λs.(x, s) : A → T (A)
∗  = λf.λx.λs.let (x, s) = x s in (f x s) : (A → T (B)) → T (A) → T (B)

The resulting encoding of read and write

read ≜ λ().S(λk.λs.(k s s)) : unit → S
write ≜ λs.S(λk.λ_.(k () s)) : S → unit

The operators can be safely added to (call-by-value) classical logic preserving subject reduction. In general, if T is atomic, normalisability is preserved. In the case of the state monad, T is functional and nothing prevents (a priori) to derive a fixpoint.

Comparing shift and reset to the other operators

One can observe that reset behaves the same as ptry and that A behaves as raise. The correspondences are as follows:

A t  ≜ S(λ_.t)
callcc (λk.t) ≜ S(λk.k t[λx.A (k x)/k])
C (λk.t)  ≜ S(λk.t[λx.A (k x)/k])
ptry t  ≜ ⟨t⟩

                          raise t  ≜ A t

Conversely, shift can be macro-defined from callcc, A/raise and ptry/reset:

S(λk.t) ≜ callcc (λk.A(t[λx.⟨k x⟩/k]))

The shift/reset calculus can hence be seen as the marriage between the ptry/raise calculus and the

callcc/throw calculus.

Warning: callcc, as it occurs in programming languages (that do have exceptions) captures the full continuation and not just the delimited one. It is better to use the name K to denote the variant that captures the current delimited continuation.

λμμ̂tp-calculus

(a fine-grained shift/reset calculus)

The structural substitution, the presence of continuation variables and the distinction between commands and terms make of λμ-calculus a good candidate for finely analysing the shift/reset calculus.

Syntax

\begin{aligned}t & ::= & V | t t | μα.c | μ̂tp.c \\ c & ::= & [β]t | [tp]t \\ V & ::= & x | λx.t \end{aligned}

Macro-definability

⟨t⟩  ≜ μ̂tp.[tp]t
A t  ≜ μ_.[tp]t
S(λk.t)  ≜ μα.[tp](t[λx.μ̂tp.[α]x/k])
C(λk.t)  ≜ μα.[tp](t[λx.μ_.[α]x/k])
callcc(λk.t) ≜ μα.[α](t[λx.μ_.[α]x/k])

The fourth combination μα.[α](t[λx.μ̂tp.[α]x/k]) has no name (to our knowledge), it is equivalent to S(λk.k t).

λμμ̂tp-calculus

(a fine-grained shift/reset calculus)

Semantics

(β_{v})  (λx.t) V  → t[V/x]
(η_{v})  λx.(V x)  → t  if x not free in V
(μ_{app}) (μα.c) u  → μα.c[[α](□ u))/α]
(μ′_{app}) V (μα.c)  → μα.c[[α](V □))/α]
(μ_{var}) [β]μα.c  → c[β/α]  also if β is tp
(η_{μ})  μα.[α]t  → t  if α not free in t
(μ̂_{var}) [tp]μ̂tp.c  → c
(η_{μ̂v}) μ̂tp.[tp]V  → V  even if tp occurs in t
(let μ̂) μ̂tp.[β]((λx.t) μ̂tp.c) → (λx.μ̂tp.[β]t) μ̂tp.c
(let_{μ}) (λx.μα.[β]t) u  → μα.[β]((λx.t) u)
(let_{app}) (λx.t) u u′  → (λx.(t u′)) u
(let′_{app}) V ((λx.t) u)  → (λx.(V t)) u
(η_{let}) (λx.x) t  → t

λμμ̂tp-calculus and types

There are several possible systems of simple types and they all depend on a toplevel type, say T. They assign the following types to operators:

\begin{aligned}⟨t⟩ & : & T → T \\ A t & : & T → A \\ S(λk.t) & : & ((A → T) → T) → A \\ C(λk.t) & : & ((A → B) → T) → A \\ callcc(λk.t) & : & ((A → B) → A) → A \end{aligned}

A Curry-Howard correspondence holds if the toplevel type T is taken to be ⊥, in which case, we get types compatible with Griffin’s seminal observations [1990] on Curry-Howard for classical logic.

⟨t⟩  : ⊥ → ⊥  (no logical content)
A t  : ⊥ → A  (ex falso quodlibet)
S(λk.t)  : ((A → ⊥) → ⊥) → A (double negation elimination)
C(λk.t)  : ((A → B) → ⊥) → A (an instance of it is double negation elimination)
callcc(λk.t) : ((A → B) → A) → A (Peirce law)

Part II

Observational (Böhm) completeness in (call-by-name) λμ-calculus

Failure of separability in call-by-name λμ-calculus

The original syntax of λμ-calculus:

\begin{aligned}t & ::= & x | λx.t | t t | μα.c \\ c & ::= & [α]t \end{aligned}

Extending the call-by-name reduction semantics with η rules:

(β) (λx.t) u → t[u/x]
(η) λx.(t x) → t  if x not free in t
(μ_{app}) (μα.c) u → μα.c[[α](□ u))/α]
(μ_{var}) [β]μα.c → c[β/α]
(η_{μ}) μα.[α]t → t  if α not free in t

David-Py [2001]: There exist two closed terms W_{0} and W_{1} in λμ-calculus that are not equal w.r.t. the equalities β, η, μ_{app}, μ_{var} and η_{μ} but whose observational behaviour is not separable.

Success of separability in Saurin’s λμ-calculus

A slightly different syntax (originally from de Groote):

t ::= x | λx.t | t t | μα.t | [β]t

The same (apparent) reduction rules:

(β) (λx.t) u → t[u/x]
(η) λx.(t x) → t  if x not free in t
(μ_{app}) (μα.t) u → μα.t[[α](□ u))/α]
(μ_{var}) [β]μα.t → t[β/α]
(η_{μ}) μα.[α]t → t  if α not free in t

But a major difference: t [β]μα.u → t (u[β/α]). We can get rid of μ what was not possible in the original λμ-calculus (indeed the left-hand side is even not expressible).

Saurin [2005]: The modified syntax of λμ-calculus with the equalities β, η, μ_{app}, μ_{var} and η_{μ} has the Böhm separability property.

From Saurin’s λμ-calculus to call-by-name λμμ̂tp-calculus

In Saurin’s calculus, the syntactic distinction between terms and commands is lost, making difficult to understand it computationally (e.g. in an abstract machine, i.e. in \overline{λ}μμ̃-calculus).

The constructions μ̂tp and [tp] can be proved to be adequate coercions from Saurin’s calculus to a calculus well-suited for computation.

Macro-definition of Saurin’s calculus on top of λμμ̂tp

\begin{matrix}μα.t & ≜ & μα.[tp]t \\ [α]t & ≜ & μ̂tp.[α]t \end{matrix}

Call-by-name λμμ̂tp-calculus

(β) (λx.t) u → t[u/x]
(η) λx.(t x) → t  if x not free in t
(μ_{app}) (μα.c) u → μα.c[[α](□ u))/α]
(μ_{var}^{n}) [β]μα.c → c[β/α]  β ≠ tp
(η_{μ}) μα.[α]t → t  if α not free in t
(μ̂_{var}) [tp]μ̂tp.c → c
(ημ̂) μ̂tp.[tp]t → t  even if tp occurs in t

Obviously, we have: Proposition t = u in Saurin’s λμ-calculus iff t = u in λμμ̂tp-calculus. Corollary λμμ̂tp-calculus is observationally complete on finite normal forms. That the rules above are relevant for what can be considered as a call-by-name version of the shift/reset-calculus can be seen from the operational semantics and from the continuation-passing-style semantics of call-by-name λμμ̂tp-calculus.

Classification of the reduction semantics of λμμ̂tp-calculus

the fundamental critical pair of computation (λx.t) (μα.c)

↙ (CBV)
(β_{v}) + (μ′_{app}) + (η_{μ̂v}) + (η_{v})

subsidiary choice (λx.t) (μ̂tp.c)

(μ̂ not value) ↙  ↘ (μ̂ value)

shift/lazy reset           shift/reset

(Sabry)  (Danvy-Filinski)
cps-completion (Sabry)  cps-completion (Kameyama-Hasegawa)

typed “domain”-completion (Sitaram-Felleisen)

(CBN) ↘

(β) + (ημ̂) + (η)

subsidiary choice [tp]μα.c

(tp co-value) ↙  ↘ (tp not co-value)

                                               CBN shift/reset  Λμ

(Danvy)  (de Groote/Saurin)

Böhm-completion (Saurin)

Abstract machine for call-by-name λμμ̂tp-calculus

The language of the call-by-name abstract machine is an extension with explicit environments of the language of λμμ̂tp. We need an extra constant of evaluation context that we write ϵ. It is defined by:

K ::= α[e] | t[e] · K  (linear ev. contexts)
[S] ::= [ ] | [tp= K; S]  (dynamic environment)
[e] ::= [ ] | [x = t[e]; e] | [α = K; e] (environments)
s ::= c [e] [S] | t [e] K [S]  (states)

Abstract machine for call-by-name λμμ̂tp-calculus (continued)

The evaluation rules can be split into two categories: the rules giving priority to the evaluation of context (commands of the form [k]t [e] S) and the ones giving priority to the term (commands of the form t[e] K S). We write e(α) for the binding of α in e and similarly for e(x).

Control given to the evaluation context

[tp]t [e] [tp = K; S] → t [e] K [S]
[α]t [e] [S]  → t [e] α[e] [S]
[tp]t [e] [ ]  → stop on [tp]t[e]

Control given to the term

x  [e] K [S] → t  [e′] K  [S]  if e(x) = t[e′]
x  [e] K [S] → stop on S^{∗}[K^{∗}[x]]  if x not bound in e
λx.t [e] K [S] → λx.t[e]  K  [S]
t u [e] K [S] → t  [e] u[e] · K  [S]
μα.c [e] K [S] → c  [α = K; e] [S]
μ̂tp.c [e] K [S] → c [e] [tp = K; S]

Control given to the “linear” evaluation context

λx.t[e] u · K [S] → t  [x = u; e] K [S]
λx.t[e] α[e′] [S] → λx.t [e]  K [S] if e′(α) = K
λx.t[e] α[e′] [S] → stop on S^{∗}[[α](λx.t[e])] if α not bound in e′

To evaluate t, we need a linear toplevel free variables distinct from tp (which is not linear). Let ϵ be this variables. Then, the machine starts with the following initial state:

t [ ] ϵ[ ] [ ]

Note: terminal states are defined by

\begin{aligned}[α]^{∗} & = & [α](□) & [ ]^{∗} & = & □ \\ (t[e] · K)^{∗} & = & K^{∗}[□ t[e]] & [tp = K; S]^{∗} & = & [S]^{∗}[μ̂tp.K^{∗}] \end{aligned}

Abstract machine for call-by-value λμμ̂tp-calculus

The language of the abstract machine is an extension with explicit environments of the language of λμμ̂tp. It is defined by:

K ::= k[e] | t[e] · K | μ̃x.(W x · K) (ev. contexts)
[S] ::= [ ] | [tp= K; S]  (dynamic environment)
W ::= V [e]  (closure)
[e] ::= [ ] | [x = W; e] | [α = K; e] (environments)
k ::= α | tp  (ev. context variables)
s ::= W K [S] | t [e] K [S]  (states)

Abstract machine for call-by-value λμμ̂tp-calculus (continued)

The evaluation rules can be split into two categories: the rules giving priority to the evaluation of context (commands of the form W K S) and the ones giving priority to the term (commands of the form t[e] K S). We write e(α) for the binding of α in e and similarly for e(x).

Control given to the evaluation context

W tp[e]  [tp = K; S] → W  K  [S]
W tp[e]  [ ]  → stop on [tp]W
W α[e]  [S]  → W  K  [S]  if e(α) = K
W α[e]  [S]  → stop on S^{∗}[[α]W]  if α not bound in e
W t[e] · K  [S]  → t [e]  μ̃x.(W x · K) [S]
W μ̃x.(V [e] x · K) [S]  → V [e] W · K  [S]

Control given to the term

V  [e] K [S] → V [e]  K  [S]
t u  [e] K [S] → t  [e]  u[e] · K  [S]
μα.[k]t [e] K [S] → t  [α = K; e] k[α = K; e] [S]
μ̂tp.[k]t [e] K [S] → t  [e]  k[e]  [tp = K; S]

Control given to the functional value

λx.t [e] W · K [S] → t [x = W; e]  K [S]
x  [e] W · K [S] → V [e′]  W · K [S]  if e(x) = V [e′]
x  [e] W · K [S] → stop on S^{∗}[K^{∗}[x W]]  otherwise

To evaluate t, the machine starts with the following initial state:

t [ ] tp[ ] [ ]

References

[1]Zena M. Ariola and Hugo Herbelin. Control Reduction Theories: The Benefit of Structural Substitution. Journal of Functional Programming, 2007. To appear.

[2]Zena M. Ariola, Hugo Herbelin and Amr Sabry. A type-theoretic foundation of delimited continuations. In Higher-Order and Symbolic Computation, 2007. To appear.

[3]Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark, August 1989.

[4]Olivier Danvy and Andrzej Filinski. Abstracting Control. Proceedings of the 1990 ACM Conference on LISP and Functional Programming, Nice, pages 151–160, 1990.

[5]Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker and Bruce F. Duba. Reasoning with continuations. First symposium on logic and computer science, pages 131–141, 1986.

[6]Andrzej Filinski. Representing monads. In Conf. Record 21st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL ’94), Portland, OR, USA, pages 446–457. January 1994.

[7]Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning: International Conf. LPAR ’92 Proceedings, pages 190–201, 1992.

[8]Amr Sabry. Note on axiomatizing the semantics of control operators. Technical Report CIS-TR-96-03, Dept of Information Science, Univ. of Oregon, 1996.

[9]Alexis Saurin. Separation with streams in the λμ-calculus. In Proceedings, 20th Annual IEEE Symposium on Logic in Computer Science (LICS ’05), pages 356–365. IEEE Computer Society Press, 2005.