Chapter 15 Separation logic for control operators

• 15.1 Separation logic reminder
• 15.2 A separation logic for a functional-imperative language
• 15.3 A separation logic for callcc
• 15.4 A separation logic for linear undelimited continuations
• 15.5 A separation logic for effect handlers with linear continuations
• 15.6 Further reading

15.1 Separation logic reminder

Separation logic was introduced by Reynolds (2002) as an extension of Hoare logic with better support for programs that use pointers and dynamic memory allocation. Such programs may encounter issues that are difficult to rule out using plain Hoare logic alone. For example, aliasing (different pointer variables that point to the same block) can cause writes through one pointer variable to affect reads through another. One can forget to free a dynamically-allocated block when it is no longer needed, causing memory leaks. One can access a block after it was freed, causing undefined behavior. Similar issues arise with many types of resources besides memory blocks, such as system resources (file descriptors, etc.), security capabilities, and even some types of continuations, as we will see later in this chapter.

In Hoare logic, assertions have a truth value and describe the current state of the program’s mutable variables. In separation logic, assertions have both a truth value and a footprint, which is a set of resources, and describe both the current state of these resources and the fact that they are uniquely owned by the assertion. This makes it possible to define resource-aware logical connectives such as the separating conjunction A ∗ B, which holds if both assertions A and B hold and their footprints are disjoint. Thus, if a resource owned by A is modified, B will remain valid, since the resources owned by B remain unmodified.

In the case where resources are dynamically-allocated memory blocks, the assertions of separation logic are predicates on memory heaps. Below are the commonly-used assertions and their formal definitions as predicates on the heap h. We write D h for the domain of h, i.e. the set of valid locations in h.

For example, consider the assertion

It states that ℓ₁ and ℓ₂ are valid locations containing some integers n₁, n₂ that sum to 10. Because it uses a separating conjunction, it also guarantees that ℓ₁ ≠ ℓ₂, i.e. that there is no aliasing between the pointers ℓ₁ and ℓ₂. Consequently, if we increment the contents of ℓ₁, we can safely conclude that

This conclusion would be invalid without the guarantee that ℓ₁ ≠ ℓ₂: if both pointers alias, incrementing the contents of ℓ₁ also increments the contents of ℓ₂, resulting in a sum of 12.

15.2 A separation logic for a functional-imperative language

The FUNREF language.  Figure 15.1 shows the abstract syntax of FUNREF, the toy language employed in this chapter. FUNREF is a functional language that also supports imperative programming via references that can be modified in place, similar to OCaml and other languages from the ML family. References are presented via four operations:

• alloc creates a fresh, uninitialized reference;
• x := v (read: “assign v to x”) stores the value v in the reference x;
• ! x (read: “dereference x”) reads and returns the value contained in the reference x;
• free x deallocates the reference x.

Note that allocation is non-initializing and deallocation is explicit, as in C-like languages but not in ML-like or Java-like languages.

---

Values:  v		::=		c		constants
		∣		ℓ		memory locations
		∣		x		variables
		∣		λ x . e		function abstraction
		∣		v1  op  v2		arithmetic operations
Computations:  e		::=		v		trivial computation
		∣		let x = e1 in e2		sequencing of computations
		∣		v1 v2		function application
		∣		if v then e1 else e2		conditional
		∣		alloc		allocation of a reference
		∣		! v		dereference
		∣		v1 := v2		assignment
		∣		free v		deallocation

Derived forms:

λ _ . e   =  λ x . e    with x not free in e                   e1; e2   =  let x = e1 in e2    with x not free in e2                   ref v   =  let x = alloc in x := v; x

Figure 15.1: The FUNREF language of expressions and mutable references.

---

Inspired by the computational lambda-calculus (section 11.2), FUNREF syntactically distinguishes values, which are pure, effect-free expressions, from computations, which are effectful expressions that can create, update or free references. The let x = e₁ in e₂ binding sequences the executions of the two computations e₁ and e₂. We also write e₁; e₂ if e₂ does not use the value of e₁.

Here are some examples of FUNREF functions:

The tally function is an example of a function that is sensitive to aliasing of its arguments: if r₁ ≠ r₂, it adds the contents of r₂ to those of r₁ and sets r₂ to 0; but if r₁ = r₂, both r₁ and r₂ are set to 0.

A separation logic.  Figure 15.2 shows the rules of a separation logic for FUNREF. Like in Hoare logic, these rules define triples {  P  }  e  {  Q  } , where e is a computation, P its precondition, and Q its postcondition. The precondition P is an assertion describing the state before e starts executing. The postcondition Q is a function that maps the value of e to an assertion describing the state when e returns its value. This asymmetry between P and Q makes it possible to specify the value of a computation, in addition to its effects. For example, we can write

---

P ⇒ Q v      (pure)  {  P  }  v  {  Q  }

 

{  P  }  e1  {  R  }      ∀v,  {  R v  }  e2 [x := v]  {  Q  }       (let)  {  P  }  let x=e1 in e2  {  Q  }

 

{  P  }  e [x := v]  {  Q  }       (fun)  {  P  }  (λ x . e) v  {  Q  }

 

{  P ∗ ⟨ v = true ⟩  }  e1  {  Q  }       {  P ∗ ⟨ v = false ⟩  }  e2  {  Q  }       (cond)  {  P  }  if v then e1 else e2  {  Q  }

 

{   emp   }  alloc  {  λ ℓ . ℓ ↦ _  }       (alloc)

 

{   ℓ ↦ v   }  ! ℓ  {  λ r . ⟨ r = v ⟩ ∗ ℓ ↦ v   }       (deref)

 

 

{   ℓ ↦ _   }  ℓ := v  {  λ _ . ℓ ↦ v  }       (assign)

 

{   ℓ ↦ _  }  free ℓ  {  λ _ . emp  }       (free)

 

{  P  }  e  {  Q  }       (frame)  {  P ∗ R  }  e  {  λ v . Q v ∗ R  }

 

P ⇒ P′      {  P′  }  e  {  Q′  }      ∀v, Q′ v ⇒ Q v      (consequence)  {  P  }  e  {  Q  }

 

Figure 15.2: Separation logic rules for the FUNREF language.

---

The rules (pure) and (let) describe trivial computations and the sequencing of computations:

These two rules are analogous to the (skip) and (assign) rules of Hoare logic (figure 14.1). In particular, from rule (let) we can derive a rule for sequences e₁;e₂.

The rules (cond) and (consequence) also resemble those of Hoare logic. In contrast, the rule (frame) is characteristic of separation logic:

This rule leverages a key property of separation logic: if {  P  }  e  {  Q  } holds, then the assertions P and Q v (where v is the value of e) describe all the locations that matter for the expression e; any location that is not in the footprint of P or Q v has no influence on the evaluation of e, and is not modified during this evaluation. Therefore, if the precondition P ∗ R holds, the part of the initial heap described by R remains unchanged during the execution of e, R still holds at the end of this execution, and the postcondition Q v ∗ R is true.

The four operations on references are given the so-called “small” rules

What is small here is not the rules but the footprints of the preconditions and postconditions. For instance, the rule for an assignment ℓ := v is stated in terms of a heap containing a single location ℓ, which is guaranteed to contain v after the assignment. To handle larger heaps, we simply combine the “small” rules with the frame rule, obtaining the following “large” rules:

Using these rules and those from figure 15.2, we can prove the following specifications for the incr, swap and tally functions shown above:

15.3 A separation logic for callcc

Many control operators, such as callcc and unrestricted effect handlers, make it possible to execute multiple times, or not at all, a program fragment that would otherwise run only once. This tremendously complicates the design of program logics for these control operators. Here is an example, taken from Timany and Birkedal (2019):

Here, e is an expression that does not mention x and that returns a function from unit to unit. We expect the example above to always return 1, since x starts at 0, is unaffected by e, then incremented once, unaffected by the call f(), and finally returned. Now, replace e by the following expression:

The continuation k that is bound by callcc is λ f . incr x;  f(); … It starts just before the incr x and extends until the end of the program. After e completes, f is bound to λ _ . throw k (λ _ . ()), then incr x is executed once, then f is applied. The continuation k restarts, binding f to λ _ . () and executing incr x a second time. The final ! x returns 2.

Here is another example of callcc oddity, not involving any mutable state:

Here, e is an expression of type unit → int. This example should always return 0, since n × 0 = 0 for all integers n. This can be proved using the (let) and (pure) rules:

However, if e = callcc (λ k . λ _ . throw k 1), the call to f () causes let n = f() in n × 0 to return 1, skipping over the computation of n × 0.

As these examples show, the combination of the full, unrestricted callcc with the unrestricted (let) and (frame) rules is unsound.

Timany and Birkedal (2019) propose to work around this issue by restricting the (let) rule to expressions not containing callcc or throw, and using whole-program, operational-style rules to reason about callcc and throw. More precisely, they first define rules {{  P  }}  p  {{  Q  }} that apply to the whole program p rather than arbitrary subexpressions e of p. Each rule applies to a decomposition of p as C[e₁], where C is an evaluation context and e₁ a reducible subexpression. For example, here are the rules for let, conditionals, callcc, and throw:

Note the similarity between these deduction rules and the reduction rules for callcc of section 8.4. For each reduction rule p → p′, there is a corresponding deduction rule that states “to prove {{  P  }}  p  {{  Q  }} , it suffices to prove {{  P  }}  p′  {{  Q  }} ”. This allows us to reason about program executions by performing a kind of symbolic execution of the program. For instance, we can show that the following toy program evaluates to n+2:

Here, (*) uses the callcc rule with the context C = [ ] + 2, and (**) uses the throw rule with the context C = ([ ] + 4) + 2.

To facilitate verification and recover some of the modular reasoning capabilities of separation logic, Timany and Birkedal (2019) define local triples {  P  }  e  {  Q  } as the triples that can be used in any context C. More precisely, local triples are those that satisfy the following context rule

It can be shown that all the triples that can be derived by the usual rules of separation logic (the rules shown in figure 15.2) are local triples. This allows us to reason normally about the program parts that do not use callcc or throw, using a standard separation logic and the full power of the (let) and (frame) rules. Only program parts involving callcc and throw require whole-program, operational reasoning.

15.4 A separation logic for linear undelimited continuations

As shown at the beginning of section 15.3, a reason callcc and other control operators complicate reasoning is that the captured continuations can execute multiple times. In the example of Timany and Birkedal (2019),

the continuation of the expression e runs twice: once when e returns normally, and once when f is applied and the continuation captured by e is invoked.

As the rest of this chapter shows, continuations that are used linearly (exactly once) or affinely (at most once) do not exhibit these problems and can be described in a standard separation logic. These one-shot continuations, as they are called in the literature, are sufficient for many applications of control operators, such as the implementations of exceptions (section 8.3), cooperative multithreading (sections 8.3 and 10.4), and control inversion on iterators (sections 8.7 and 10.3). The only uses of control operators where continuations are invoked multiple times are those that implement backtracking (the choose-and-assert examples of sections 8.3 and 8.7) or use nondeterminism (the flip effect of section 12.2).

The call1cc operator is a “one-shot” variant of callcc introduced by Bruggeman et al. (1996). Its uses look like those of callcc:

captures the current continuation and binds it to k during the evaluation of e. However, k must be used exactly once. Returning normally from e counts for one use of k. Therefore, e has three possible behaviors:

1. it does not restart k and returns normally with a value, which counts for one use of k;
2. it restarts k on some value v, using throw k v, which causes call1cc to return with value v;
3. it saves k in memory, allowing k to be used later, and restarts another continuation k′ that was previously captured and has not been invoked already.

Here is an example of behaviors 1 and 2, where the continuation is used as a local exception:

If n < 0, the body of call1cc returns normally with the opposite of n (behavior 1). If n ≥ 0, the continuation k is applied to n, causing call1cc to return n (behavior 2).

Here is an example of behavior 3. This example implements two coroutines that interleave executions by calling the yield function to transfer control to the other coroutine.

The two coroutines are the function parameters f and g, which take the yield function as argument. Their type is (unit → unit) → unit. First, we capture an exit continuation k₀, then we allocate a one-element ready queue. This queue is just a reference containing a continuation in the other coroutine (the one that is not currently executing). The yield function captures its continuation k and swaps it with the continuation k′ contained in ready, then restarts k′. The terminate function is called when either f or g terminates. It explicitly discards the ready continuation before invoking the exit continuation k₀. This is in keeping with our policy of using each continuation exactly once. Finally, ready is initialized with a continuation that will start the execution of g yield, and f yield is run. When either f or g returns, terminate is called and the entire coroutine function returns.

Specifying continuations.  To a first approximation, a continuation is a function that never returns. Therefore, it has a precondition, which is a function from values to assertions describing the resources needed by the continuation and constraining the value of the function parameter, but no postcondition. We write iscont k P to mean that k is a continuation with precondition P. Note that P is also the postcondition for the call1cc that captured k, since invoking k with value v causes this call1cc to return v.

The major difference between linear continuations and functions is that functions can be called multiple times, or not at all, whereas linear continuations must be used exactly once. Therefore, iscont k P is not a pure assertion: it has a nonempty footprint and cannot be duplicated or ignored.

An intuitive justification is that each continuation can run on its own stack, as in the OCaml implementation of effect handlers (see section 10.2). Therefore, iscont k P asserts ownership of the memory area containing this stack.

Continuation specifications have an interesting “framing” property. Consider a continuation k that requires resources P v ∗ R. It can be viewed as requiring fewer resources P v, provided that the missing resources R are available and can be set apart:

Equivalently, this property can be written as a monotonicity property of iscont:

Rules for linear continuations.  Using the iscont assertion, we can give the following separation logic rules for the call1cc, throw and discard operators.

For throw k v to execute safely, k must be a valid continuation with precondition P, and P v must be satisfied. Hence, the precondition is iscont k P ∗ P v. Since throw k v never returns normally, the postcondition is λ _ . false, which can be replaced by any postcondition Q by the consequence rule.

For call1cc (λ k . e), the body e can assume P ∗ iscont k Q as precondition, where P is the precondition of the call1cc expression and Q its postcondition. Indeed, any application of k will jump to the return point of the call1cc expression, so it must guarantee the postcondition Q. If e terminates normally with value v, it must not only guarantee the postcondition Q v, but also the iscont k Q assertion, as evidence that it did not use k at all.

An example of verification.  We now outline the verification of the two-coroutine example above. Inspired by the Hoare logic rules for coroutines and cooperative threads of section 14.4, we assume that an invariant P holds at each “context switch”, i.e. when a yield operation is executed by f or by g. It turns out that P must also be the precondition of f and g, which must also share a postcondition Q. Therefore, we assume that f and g satisfy the following contract:

The universally-quantified proposition R is the internal invariant of the implementation of yield. We now use it to describe the ready reference and the exit continuation k₀ that are internal to the coroutine function. To this end, we take

Note that R is recursive: before the continuation k stored in ready can be invoked, not only the user invariant P must hold, but also the internal invariant R must have been restored by storing a suitable continuation k′ in ready. This is exactly what yield does, as seen in the following verification outline:

Therefore, we have

which implies

according to the specification of f, and likewise for g. We can also show

From these specifications of yield and terminate, it follows that

This concludes the verification of the function coroutine.

15.5 A separation logic for effect handlers with linear continuations

Effect handlers (chapter 10) differ from callcc in several ways. In particular, handlers receive delimited continuations, whereas callcc captures undelimited continuations. However, when reasoning about effect handlers using a program logic, the same problems arise with the repeated executions of a code fragment. Consider the Flip effect for nondeterminism (section 12.2):

In this example, perform Flip returns twice: once with the value false and once with the value true. This causes incr x to be executed twice. This is not accounted for by the standard (let) rule of separation logic.

However, we can restrict the continuations captured by handlers to be linear, i.e. used exactly once. This is what OCaml does (see section 10.2). In this case, we can reason about effect handlers using the unrestricted (let) and (frame) rules of separation logic. This is what the Hazel logic of de Vilhena and Pottier (2021) does.

Effect protocols.  To support modular verification, de Vilhena and Pottier (2021) introduce the notion of an effect protocol, which acts as a contract between the code fragments that perform effects and those that handle effects. The syntax of protocols Ψ is the following:

The protocol ⊥ states that no effects can be performed. The protocol Ψ₁ + Ψ₂ states that any effect allowed by Ψ₁ or by Ψ₂ can be performed. The protocol ! x (F v)  {  P  } . ? y (w)  {  Q  } states that for all choices of x, the program can perform the effect F with argument value v, provided that the precondition P holds; then, for some choice of y, the result value w of F will satisfy the postcondition Q. Here, P and Q are separation logic assertions, and x and y are sets of mathematical variables that can occur in v, P, and Q.

For example, here is a protocol for an Abort effect that behaves like an exception: perform Abort never returns, and the handlers for Abort discard the captured continuations.

The false postcondition indicates that this effect never returns.

Here is a protocol for a Next effect that simulates incrementing a counter:

The abstract assertion Count n keeps track of the current value of the counter. If the counter is implemented as a single memory location ℓ, we can take

However, more complex implementations involving multiple memory locations are also possible and can be hidden in the appropriate Count predicate. According to the contract, Next can be performed in any state that satisfies Count n for some value of n, and perform Next returns the value n in a state that satisfies Count (n+1).

We can extend the Next protocol with a Reset effect that sets the counter to 0:

Separation logic.  The separation logic defines quadruples {  P  }  e  ⟨  Ψ  ⟩   {  Q  } , where e is an expression, P is its precondition, Q is its normal postcondition describing the case where e returns normally, and Ψ is an effect protocol describing the effects that e is allowed to perform. Note the similarity with the Hoare logics for goto jumps of section 14.3: the Arbib-Alagic-de Bruijn approach uses quadruples {  P  }  s  {  Q  }   {  J  } , where Q is the normal postcondition and J is the “goto protocol” specifying the jumps that s can perform.

The separation logic rules of figure 15.2 extend straightforwardly to quadruples. The Ψ postcondition is either ignored or distributed over the subcomputations, as seen in the (pure) and (let) rules:

The (consequence) rule allows us to weaken both postconditions Ψ and Q:

The relation Ψ′ ⊑ Ψ means that Ψ is more permissive than Ψ′: any effect that is allowed by Ψ′ is also allowed by Ψ, with an identical or more restrictive protocol. (See de Vilhena and Pottier (2021) for the precise definition.)

Performing effects.  The rule for the perform construct is:

Here, Ψ  allows  (F v)  {  Q  } stands for the condition necessary to perform effect F with argument v and ensure that Q holds when the effect returns. This condition is defined by the following equations:

The last case above reads as follows: if we choose x so that the actual argument v of the effect and the formal parameter v′ of the contract are equal, then the precondition A of F must hold, and for any choice of y that satisfies the postcondition B of F, the postcondition Q(w) holds.

The first two cases are straightforward: the ⊥ contract allows no effects to be performed, while the Ψ₁ + Ψ₂ contract allows whatever effects Ψ₁ or Ψ₂ allows.

Specifying continuations.  As in section 15.4, we introduce the special assertion iscont k P Ψ Q to specify the continuations k captured by effect handlers. These continuations are delimited, so they have both a precondition P, which describes the values to which they can be applied, and two postconditions: Q, which describes the values they can return and Ψ, which describes the effects they can perform. In this respect, delimited continuations resemble functions. However, a function can be applied multiple times, whereas our delimited continuations are linear and must be applied exactly once. Therefore, the iscont k P Ψ Q predicate is not duplicable. Moreover, it is monotonic in P:

The two operations on delimited continuations are continue, which restarts a continuation, and discontinue, which discards a continuation. Their rules are simple:

Handling effects.  We use the same presentation of effect handlers as in section 10.5: handle e with e_ret, e_eff handles the effects performed by e using e_eff and the return value of e using e_ret. We assume a shallow handling semantics. The separation logic rule for this construct is:

Just like the handler describes how to transform the outcome of e (return value and effects) into a different outcome, the ishandler predicate describes how to transform the postconditions ⟨  Ψ  ⟩   {  Q  } of e into the postconditions ⟨  Ψ′  ⟩   {  Q′  } of the handler.

If e terminates normally, its value v satisfies Q, and e_ret v is executed. Therefore, this computation must satisfy

If e terminates by performing an effect F with argument v and continuation k, e_eff (F v) k is executed and must satisfy

for some precondition R. What can R guarantee about the value v, the continuation k, and the resources that e_eff can use? We could search Ψ to find the protocol associated with F, and derive a precondition A and a postcondition B for the performed effect F v. Then, in the handler e_eff (F v) k, we could assume that A holds, and that k is a continuation with precondition B and postconditions ⟨  Ψ  ⟩   {  Q  } . (These are the same postconditions as the handled expression e, since we consider a shallow handler, which does not apply when the continuation runs.)

Alternatively, and more concisely, de Vilhena and Pottier (2021) characterize v and k as any argument value and any continuation allowed for F by the protocol Ψ, in the sense of the allows predicate. This leads to the following precondition for e_eff (F v) k:

This can be read as follows: for any response x to F v allowed by the protocol Ψ, we can assume that the continuation k can be applied to x and will, then, satisfy the postconditions ⟨  Ψ  ⟩   {  Q  } .

Putting it all together, we have

This definition of ishandler corresponds to the shallow semantics of effect handling. For the definition corresponding to deep handlers, see de Vilhena and Pottier (2021).

15.6 Further reading

O’Hearn (2019) provides an overview of separation logic and some of its applications. It has many uses beyond reasoning about pointer programs and linear continuations. In particular, its extension to concurrency, concurrent separation logic (O’Hearn, 2007), is an essential tool for reasoning about non-cooperative multithreading and shared-memory parallelism.

Program logics for effect handlers and other control operators is an active area of research. We have emphasized the case of linear (one-shot) continuations, because it is simpler and the corresponding rules resemble those for goto jumps (for undelimited continuations) and for function applications (for delimited continuations). Delbianco and Nanevski (2013) develop a Hoare logic for callcc with general (multi-shot) continuations. The Maze separation logic of de Vilhena (2022, chapter 6) applies to effect handlers with general (multi-shot) continuations, at the cost of a restricted frame rule. It supports reasoning about callcc via an encoding in terms of effects. van Rooij and Krebbers (2025) give a unified treatment of effect handlers with either affine (one-shot) or general (multi-shot) continuations, using a substructural type system to track affine effects.

The programs logics for control operators mentioned in this chapter (Timany and Birkedal, 2019, de Vilhena and Pottier, 2021, de Vilhena, 2022, van Rooij and Krebbers, 2025) were developed using the Iris framework for separation logic (Jung et al., 2018) and mechanically verified using the Rocq proof assistant.