tifact

st

eu

OPL *
* P se * Consi

* Easy to
ed
R
nt

at e d

arXiv:1608.06499v2 [cs.PL] 8 Nov 2016

Research

Jonathan Protzenko1

2 University

of Edinburgh

3 Inria

Abstract

Guido Martı́nez3,5

Aseem Rastogi1
Paris

4 ENS

Paris

alu

1 Microsoft

Kenji Maillard1,3,4

Ev

Gordon Plotkin1,2

Cătălin Hriţcu1,3

ll Docum
We
e

Danel Ahman1,2

A EC *

Dijkstra Monads for Free

* Complete

*

t
en

*

Ar

Nikhil Swamy1
5 Rosario

National University

delicate meta-theoretic arguments to establish the soundness of a
user-provided predicate-transformer semantics with respect to the
semantics of effectful programs. These typically require proofs of
various correctness and admissibility conditions, including the correspondence to the operational semantics and the monad laws. Furthermore, only a handful of primitively supported effects are provided
by the previous version of F? , and extending it with user-defined
effects is not possible.
Rather than being given manually, we show that these predicate
transformers can be automatically derived by CPS’ing purely functional definitions of monadic effects (with answer type Type). For
instance, rather than defining WP ST, one can simply compute it by
CPS’ing the familiar ST monad (i.e., state → a ∗ state), deriving

Dijkstra monads enable a dependent type theory to be enhanced
with support for specifying and verifying effectful code via weakest
preconditions. Together with their closely related counterparts,
Hoare monads, they provide the basis on which verification tools
like F? , Hoare Type Theory (HTT), and Ynot are built.
We show that Dijkstra monads can be derived “for free” by applying a continuation-passing style (CPS) translation to the standard
monadic definitions of the underlying computational effects. Automatically deriving Dijkstra monads in this way provides a correctby-construction and efficient way of reasoning about user-defined
effects in dependent type theories.
We demonstrate these ideas in EMF? , a new dependently typed
calculus, validating it via both formal proof and a prototype implementation within F? . Besides equipping F? with a more uniform and
extensible effect system, EMF? enables a novel mixture of intrinsic
and extrinsic proofs within F? .

WP ST a = ((a ∗ state) → Type) → state → Type

(unfolded)

We apply this technique of deriving Dijkstra monads to F? . Our
goal is to make F? ’s effect system easier to configure and extensible
beyond its primitive effects. To do so, we proceed as follows:

Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory—Semantics; F.3.1 [Logics
and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Mechanical verification

A monadic metalanguage We introduce DM, a simply typed, pure,
monadic metalanguage in which one can, in the spirit of Wadler
(1992), define a variety of monadic effects, ranging from state and
exceptions, to continuations.

Keywords verification; proof assistants; effectful programming;
dependent types

A core dependent type theory with monadic reflection To formally study our improvements to F? , we define a new dependently
typed core calculus, EMF? (for Explicitly Monadic F? ) that features
an extensible effect system. EMF? is loosely based on the Calculus
of Constructions (Coquand and Huet 1988) with (among other features): (1) a predicative hierarchy of non-cumulative universes; (2)
a weakest-precondition calculus for pure programs; (3) refinement
types; and (4) a facility for representing user-defined effects using
the monadic reflection and reification of Filinski (1994), adapted to
the dependently typed setting. New effects can be introduced into
the language by defining them in terms of the built-in pure constructs, related to each other via monad morphisms; each such effect
obtains a suitable weakest precondition calculus derived from the
underlying pure WPs. We prove the calculus strongly normalizing
and the WP calculus sound for total correctness verification, for
both pure and effectful programs.

1.

Introduction

In Dijkstra’s (1975) weakest precondition semantics, stateful computations transform postconditions, relating results and final states
to preconditions on input states. One can express such semantics via
a monad of predicate transformers, a so-called “Dijkstra monad” (Jacobs 2015; Swamy et al. 2013). For instance, in the case of state,
the following monad arises:
WP ST a = post a → pre

where post a = (a ∗ state) → Type
pre = state → Type

return WP ST x post s0 = post (x, s0)
bind WP ST f g post s0 = f (λ (x, s1) → g x post s1) s0

The weakest precondition (WP) of a pure term e is computed to
be return WP ST e, and the WP of the sequential composition
let x = e1 in e2 is computed to be bind WP ST wp1 (λ x. wp2), where
wp1 and wp2 are the WPs of e1 and e2 respectively.
Building on previous work by Nanevski et al. (2008), Swamy
et al. (2013, 2016) designed and implemented F? , a dependently
typed programming language whose type system can express WPs
for higher-order, effectful programs via Dijkstra monads.
While this technique of specifying and verifying programs has
been relatively successful, there is still room for improvement. Notably, in the version of F? described by Swamy et al. (2016) specifying Dijkstra monads in F? is a tedious, manual process, requiring

Draft

A CPS translation We give a type-directed CPS translation from
DM to EMF ? . This can be used to extend EMF ? with a new effect.
One starts by defining a monadic effect (say ST) in DM. Next, via the
translation, one obtains the Dijkstra variant of that effect (WP ST) as
a monotone, conjunctive predicate EMF? transformer monad. Finally,
a second translation from DM produces expression-level terms
representing monadic computations in EMF? . A logical relations
proof shows that monadic computations are correctly specified by
their predicate transformers. We give examples of these translations
for monadic effects, such as state, exceptions, information-flow
control, continuations, and some combinations thereof.

1

2016/11/9

Intrinsic and extrinsic proofs in EMF? Effectful programs in
EMF ? can be proven correct using one or both of two different
reasoning styles. First, using the WP calculus, programs can be
proven intrinsically, by decorating their definitions with specifications that must be proven to be at least as strong as their WPs. We
refer to this as the intrinsic style, already familiar to users of F? , and
other tools like HTT (Nanevski et al. 2008), Dafny (Leino 2010),
and Why3 (Filliâtre and Paskevich 2013).
Second, through monadic reification, EMF? allows terminating
effectful programs to be revealed as their underlying pure implementations. Once reified, one can reason about them via the computational behavior of their definitions. As such, one may define
effectful programs with relatively uninformative types, and prove
properties about them as needed, via reification. This extrinsic style
of proving is familiar to users of systems like Coq or Isabelle, where
it is routinely employed to reason about pure functions; using monads this style extends smoothly to terminating effectful programs.
As in Coq an Isabelle, this extrinsic style only works for terminating
code; in this paper we do not consider divergent computations and
only discuss divergence as future work (§7)

with their WPs (§4). This is the first formal characterization of
the relation between WPs and CPS at arbitrary order.
(3)

(4) An implementation of these ideas within F? (§3.5, §4.6) and
several examples of free Dijkstra monads for user-defined effects
(§2). We highlight, in particular, the new ability to reason
extrinsically about effectful terms.
The auxiliary materials (https://www.fstar-lang.org/
papers/dm4free) contain appendices with complete definitions
and proofs for the formal results in §3, §4 (Appendix A below),
and §5. The F? source code (https://github.com/FStarLang/
FStar) now includes the extensions from §3.5 and §4.6 and the
examples from §2.

2.

Notation: The syntax λ (b1 ) ... (bn ) → t introduces a lambda abstraction, where bi ranges over binding occurrences x:t declaring a
variable x at type t. The type b1 → ... → bn → c is the type of a curried
function, where c is a computation type—we emphasize the lack of
enclosing parentheses on the bi . We write just the type in b when
the name is irrelevant, and t → t’ for t → Tot t’.

A prototype implementation for F? We have adapted F? to benefit
from the theory developed in this paper, using a subset of F? itself
as an implementation of DM, and viewing EMF?ST as a model of
its existing extraction mechanism to OCaml. Programmers can
now configure F? ’s effect system using simple monadic definitions,
use F? to prove these definitions correct, and then use our CPS
transformation to derive the Dijkstra monads required to configure
F? ’s existing type-checker. To benefit from the new extrinsic proving
capabilities, we also extended F? with two new typing rules, and
changed its normalizer, to handle monadic reflection and reification.
Several examples show how our work allows F? to be easily
extended beyond the primitive effects already supported, without
compromising its efficient primitive effect compilation strategy; and
how the new extrinsic proof style places reasoning about terminating
effectful programs in F? on an equal footing with its support for
reasoning about pure programs.

2.1

The central contribution of our work is designing three closely related lambda calculi, studying their metatheory and the connections
between them, and applying them to provide a formal and practical
foundation for a user-extensible effect system for F? . Specifically,
EMF ? : A new dependent type theory with user-extensible,
monadic effects; monadic reflection and reification; WPs; and
refinement types. We prove that EMF? is strongly normalizing
and that its WPs are sound for total correctness (§3).

(2)

DM : A simply typed language to define the expression-level
monads that we use to extend EMF? with effects. We define a
CPS transformation of DM terms to derive Dijkstra monads from
expression-level monads, as well as an elaboration of DM terms
to EMF? . Moreover, elaborated terms are proven to be in relation

Draft

WPs for Pure Programs

Reasoning about purely functional programs is a relatively wellunderstood activity: the type theories underlying systems like Coq,
Agda, and F? are already well-suited to the task. Consider proving
that pure term sqr = λ (x:int) → x ∗ x always returns a non-negative
integer. A natural strategy is an extrinsic proof, which involves
giving sqr a simple type such as int → Tot int, the type of total
functions on integers, and then proving a lemma ∀x. sqr x ≥ 0. In the
case of F? , the proof of the lemma involves, first, a little computation
to turn the goal into ∀x. x∗x ≥ 0, and then reasoning in the theory
of integer arithmetic of the Z3 SMT solver (de Moura and Bjørner
2008) to discharge the proof.
An alternative intrinsic proof style in F? involves giving sqr type
x:int → Pure int (λ post → ∀y. y≥ 0 =⇒ post y), a dependent function
type of the form x:t → c, where the formal parameter x:t is in scope in
the computation type c to the right of the arrow. Computation types
c are either Tot t (for some type t) or of the form M t wp, where M
is an effect label, t is the result type of the computation, and wp is a
predicate transformer specifying the semantics of the computation.
The computation type we give to sqr is of the form Pure t wp, the
type of t-returning pure computations described by the predicate
transformer wp: (t → Type) → Type, a function taking postconditions
on the result (predicates of type t → Type), to preconditions. These
predicate transformers form a Dijkstra monad. In this case, the wp
states that to prove any property post of sqr x, it suffices to prove
post y, for all non-negative y—as such, it states our goal that sqr x is
non-negative. To prove sqr can be given this type, F? infers a weakest
precondition for sqr x, namely λ post → post (x ∗ x) and aims to prove
that the predicate transformer we specified is at least as strong as the
weakest one it inferred: ∀post. (∀y. y≥ 0 =⇒ post y) =⇒ post (x∗x),
which is discharged automatically by Z3. For pure programs, this

Summary of Contributions

(1)

Illustrative Examples

We illustrate our main ideas using several examples from F? ,
contrasting with the state of affairs in F? prior to our work. We
start by presenting the core WP calculus for pure programs (§2.1),
then show how state and exceptions can be added to it (§2.2,
§2.3, §2.4 and §2.5). Thereafter, we present several additional
examples, including modeling dynamically allocated references
(§2.6), reasoning about primitive state (§2.7), information-flow
control (§2.8), and continuations (§2.9)—sections §3 and §4 may be
read mostly independently of these additional examples.

Primitive effects in a call-by-value semantics We see EMF? as a
meta-language in which to analyze and describe the semantics of
terms in an object language, EMF?ST , a call-by-value programming
language with primitive state. In the spirit of Moggi (1989), we show
that EMF? programs that treat their ST effect abstractly soundly
model EMF?ST reductions—technically, we prove a simulation between EMF?ST and EMF? . As such, our work is a strict improvement
on the prior support for primitive effects in F? : despite programming
and proving programs in a pure setting, stateful programs can still be
compiled to run efficiently in the primitively effectful EMF?ST , while
programs with other user-defined effects (e.g., information-flow
control) can, unlike before, be executed via their pure encodings.

1.1

EMF ?ST : A call-by-value language with primitive state, whose
reductions are simulated by well-typed EMF? terms (§5).

2

2016/11/9

intrinsic proof style may seem like overkill and, indeed, it often is.
But, as we will see, this mechanism for reasoning about pure terms
via WPs is a basic capability that we can leverage for reasoning
about terms with more complex, effectful semantics.
2.2

formally present DM, a simply typed language in which to define
monadic effects. DM itself contains a single primitive identity monad
τ , which (as will be explained shortly) is used to control the CPS
transform. We have implemented DM as a subset of F? , and for
the informal presentation here we use the concrete syntax of our
implementation. What follows is an unsurprising definition of a
state monad st a, the type of total functions from s to identity
computations returning a pair (a ∗ s).

Adding WPs for State

Consider proving that incr = let x = get() in put (x + 1) produces an
output state greater than its input state. Since this program has
the state effect, a proof by extrinsic reasoning is not completely
straightforward, because reducing an effectful computation within
a logic may not be meaningful. Instead, tools like Ynot (Chlipala
et al. 2009), HTT (Nanevski et al. 2008), and F? only support the
intrinsic proof style. In the case of F? , this involves the use of a
computation type ST0 t wp, where wp: WP ST t and for our simple
example we take WP ST t = ((t ∗ int) → Type) → int → Type, i.e., the
Dijkstra state monad from §1 with state=int.
Using the ST0 computation type in F? , one can specify for incr the
type unit → ST0 unit (λ post s0 → ∀s1. s1 > s0 =⇒ post ((), s1)). That
is, to prove any postcondition post of incr, it suffices to prove
post ((), s1) for every s1 greater than s0, the initial state—this is
the statement of our goal. The proof in F? currently involves:

let st a = s → τ (a ∗ s)
let return (x:a) : st a = λ s0 → x, s0
let bind (f:st a) (g:a → st b) : st b = λ s0 → let x,s1 = f s0 in g x s1
let get () : st a = λ s0 → s0, s0
let put (x:s) : st unit = λ → (), x

This being a subset of F? , we can use it to prove that this definition is
indeed a monad: proofs of the three monad laws for st are discharged
automatically by F? below (feq is extensional equality on functions,
and assert p requests F? to prove p statically). Other identities
relating combinations of get and put can be proven similarly.
let right unit st (f:st α) = assert (feq (bind f return) f)
let left unit st (x:α) (f:(α → st β )) = assert (feq (bind (return x) f) (f x))
let assoc st (f:st α) (g:(α → st β )) (h:(β → st γ))
= assert (feq (bind f (λ x → bind (g x) h)) (bind (bind f g) h))

(1) As discussed already in §1, one must define WP ST t, its return
and bind combinators, proving that these specifications are sound
with respect to the operational semantics of state.

We then follow a two-step recipe to add an effect like st to F? :
Step 1 To derive the Dijkstra monad variant of st, we apply a
selective CPS transformation called the ?-translation (§4.2); first,
on type st a; then, on the various monadic operations. CPS’ing only
those arrows that have τ -computation co-domains, we obtain:
(st a)?
= s → ((a ∗ s) → Type) → Type
return? = λ x s0 post → post (x, s0)
bind?
= λ f g s0 post → f s0 (λ (x,s1) → g x s1 post)
get?
= λ () s0 post → post (s0, s0)
put?
= λ x post → post ((), x)
Except for a reordering of arguments, the terms above are identical to
the analogous definitions for WP ST. We prove that the ?-translation
preserves equality: so, having shown the monad laws for st a, we
automatically obtain the monad laws for (st a)? . We also prove
that every predicate transformer produced by the ?-translation is
monotone (it maps weaker postconditions to weaker preconditions)
and conjunctive (it distributes over conjunctions and universals, i.e.,
infinite conjunctions, on the postcondition).

(2) The primitive effectful actions, get and put are assumed to have
the types below—again, these types must be proven sound with
respect to the operational semantics of F? .
get : unit → ST0 int (λ post s0 → post (s0, s0))
put : x:int → ST0 unit (λ post → post ((), x))

(3) Following the rule for sequential composition sketched in
§1, F? uses the specifications of get and put to compute
bind ST WP wp get (λ x → wp put (x + 1)) as the WP of incr,
which reduces to λ post s0 → post ((), s0 + 1).
(4) The final step requires proving that the computed WP is at least
as weak as the specified goal, which boils down to showing that
s0 + 1 > s0, which F? and Z3 handle automatically.
The first two steps above correspond to adding a new effect to
F? . The cost of this is amortized by the much more frequent and
relatively automatic steps 3 and 4. However, adding a new effect to
F? is currently an expert activity, carried out mainly by the language
designers themselves. This is in large part because the first two steps
above are both tedious and highly technical: a dangerous mixture
that can go wrong very easily.
Our primary goal is to simplify those first two steps, allowing
effects to be added to F? more easily and with fewer meta-level
arguments to trust. Besides, although F? supports customization of
its effect system, it only allows programmers to specify refinements
of a fixed set of existing effects inherited from ML, namely, state,
exceptions, and divergence. For example, an F? programmer can
refine the state effect into three sub-effects for reading, writing, and
allocation; but, she cannot add a new effect like alternative combinations of state and exceptions, non-determinism, continuations, etc.
We aim for a more flexible, trustworthy mechanism for extending
F? beyond the primitive effects it currently supports. Furthermore,
we wish to place reasoning about terminating effectful programs on
an equal footing with pure ones, supporting mixtures of intrinsic
and extrinsic proofs for both.
2.3

Step 2 The ?-translation yields a predicate transformer semantics
for a new monadic effect, however, we still need a way to extend
F? with the computational behavior of the new effect. For this, we
define a second translation, which elaborates the definitions of the
new monad and its associated actions to Pure computations in F? . A
first rough approximation of what we prove is that for a well-typed
DM computation e : τ t, its elaboration e has type Pure t e? in EMF? .
The first-order cases are particularly simple: for example,
return = return has type x:a → Pure a (return? x) in EMF? ; and
get = get has type u:unit → Pure s (get? u) in EMF? . For a higherorder example, we sketch the elaboration of bind below, writing
st t wp for s0:s → Pure t (wp s0):
bind : wpf:(st a)? → f:st a wpf
→wpg:(a → (st b)? ) → g:(x:a → st b wpgx)
→ st b (bind? wpf wpg)
= λ wpf f wpg g s0 → let x, s1 = f s0 in g x s1

Intuitively, a function in DM (like bind) that abstracts over
computations (f and g) is elaborated to a function (bind) in EMF?
that abstracts both over those computations (f and g again, but at
their elaborated types) as well as the WP specifications of those
computations (wpf and wpg). The result type of bind shows that it

CPS’ing Monads to Dijkstra Monads

Instead of manually specifying WP ST, we program a traditional
ST monad and derive WP ST using a CPS transform. In §4.1 we

Draft

3

2016/11/9

returns a computation whose specification matches bind? , i.e., the
result of the CPS’ing ?-translation.
In other words, the WPs computed by F? for monads implemented as Pure programs correspond exactly to what one gets by
CPS’ing the monads. At first, this struck us as just a happy coincidence, although, of course, we now know that it must be so. We see
our proof of this fact as providing a precise characterization of the
close connection between and WPs and CPS transformations.
2.4

and exnst a = s → τ (option (a ∗ s)). The former is more familiar to
most programmers: raising an exception preserves the state; the
latter discards the state when an exception is raised, which though
less common, is also useful. We focus first on exnst and then discuss
a variant of stexn.
Relating st and exnst Translating st (as before) and exnst to
F? gives us two unrelated effects ST and ExnST. To promote ST
computations to ExnST, we define a lift relating st to exnst, their
pure representations in DM, and prove that it is a monad morphism.

Reify and Reflect, for Abstraction and Proving

let lift (f:st a) : exnst a = λ s0 → Some (f s0)
let lift is an st exnst morphism =
assert (∀ x. feq (lift (ST.return x)) (ExnST.return x));
assert (∀ f g. feq (lift (ST.bind f g)) (ExtST.bind (lift f) (λ x → lift (g x))))

Unlike prior F? formalizations which included divergence, primitive
exception and state effects, the only primitive monad in EMF?
is for Pure computations. Except for divergence, we can encode
other effects using their pure representations; we leave divergence
for future work. Although the translations from DM yield pure
definitions of monads in F? , programming directly against those pure
implementations is undesirable, since this may break abstractions.
For instance, consider an integer-state monad whose state is expected
to monotonically increase: revealing its representation as a pure term
makes it hard to enforce this invariant. We rely on Filinski’s (1994)
monadic reflection for controlling abstraction.
Continuing our example, introducing the state effect in F?
produces a new computation type ST (a:Type) (wp: (st a)? ) and two
coercions

Applying our two-step translation to lift, we obtain in F? a
computation-type coercion from ST a wp to ExnST a (lift? wp).
Through this coercion, and through F? ’s existing inference algorithm (Swamy et al. 2011, 2016), ST computations are implicitly promoted to ExnST computations whenever needed. In
particular, the ST actions, get and put, are implicitly available
with ExnST. All that remains is to define an additional action,
raise = λ () s0 → None, which gets elaborated and reflected to F? at
the type unit → ExnST a (λ p → p None).
ExnST programs in F? can be verified intrinsically and extrinsically. For an intrinsic proof, we show div intrinsic below, which
raises an exception on a divide-by-zero. To prove it, we make use of
an abbreviation ExnSt a pre post, which lets us write specifications
using pre- and postconditions instead of predicate transformers.

reify : ST a wp → s0:s → Pure (a ∗ s) (wp s0)
reflect : (s0:s → Pure (a ∗ s) (wp s0)) → ST a wp

The reify coercion reveals the representation of an ST computation
as a Pure function, while reflect encapsulates a Pure function as a
stateful computation. As we will see in subsequent sections (§2.6
and §2.5), in some cases to preserve abstractions, one or both of
these coercions will need to be removed, or restricted in various
ways.
To introduce the actions from DM as effectful actions in F? , we
reflect the pure terms produced by the elaboration from DM to EMF? ,
obtaining actions for the newly introduced computation type. For
example, after reflection the actions get and put appear within F? at
the types below:

let ExnSt a pre post =
ExnST a (λ s0 p → pre s0 ∧ ∀x. post s0 x =⇒ p x)
let div intrinsic i j : ExnSt int
(requires (λ → True))
(ensures (λ s0 x → match x with
| None → j=0
| Some (z, s1) → s0 = s1 ∧ j <> 0 ∧ z = i / j))
= if j=0 then raise () else i / j

Alternatively, for an extrinsic proof, we give a weak specification
for div extrinsic and verify it by reasoning about its reified definition
separately. This time, we add a call to incr in the ST effect in case of
a division-by-zero. F? ’s type inference lifts incr to ExnST as required
by the context. However, as the proof shows, the incr has no effect,
since the raise that follows it discards the state.

get : unit → ST s (get? ())
put : s1:s → ST unit (put? s1)

As in §2.2, we can still program stateful functions and prove them
intrinsically, by providing detailed specifications to augment their
definitions—of course, the first two steps of the process there are
now automatic. However, we now have a means of doing extrinsic
proofs by reifying stateful programs, as shown below (taking s=int).

let ExnStNull a = ExnST a (λ s0 post → ∀x. post x)
let div extrinsic i j : ExnStNull int = if j=0 then (incr(); raise ()) else i / j
let lemma div extrinsic i j =
assert (match reify (div extrinsic i j) 0 with
| None → j = 0
| Some (z, 0) → j <> 0 ∧ z = i / j)

let StNull a = ST a (λ s0 post → ∀x. post x)
let incr : StNull unit = let n = get() in put (n + 1)
let incr increases (s0:s) = assert (snd (reify (incr()) s0) = s0 + 1)

Using reify and reflect we can also build exception handlers,
following ideas of Filinski (Filinski 1999). For example, in try div
below, we use a handler and (under-)specify that it never raises an
exception.

The StNull unit annotation on the second line above gives a weak
specification for incr. However, later, when a particular property of
incr is required, we can recover it by reasoning extrinsically about
the reification of incr() as a pure term.
2.5

let try div i j : ExnSt int
(requires (λ → True))
(ensures (λ x → Option.isSome x))
= reflect (λ s0 → match reify (div intrinsic i j) s0 with
| None → Some (0, s0)
| x → x)

Combining Monads: State and Exceptions, in Two Ways

To add more effects to F? , one can simply repeat the methodology outlined above. For instance, one can use DM to define
exn a = unit → τ (option a) in the obvious way (the unit is necessary,
cf. §4.1), our automated two-step recipe extends F? with an effect
for terminating programs that may raise exceptions. Of course, we
would like to combine the effects to equip stateful programs with
exceptions and, here, we come to a familiar fork in the road.
State and exceptions can be combined in two mutually incompatible ways. In DM, we can define both stexn a = s → τ ((option a) ∗ s)

Draft

More systematically, we can first program a Benton and Kennedy
(2001) exception handler in DM, namely, as a term of type
exnst a → (unit → exnst b) → (a → exnst b) → exnst b

and then translate it to F? , thereby obtaining a weakest precondition
rule for it for free. More generally, adapting the algebraic effect

4

2016/11/9

handlers of Plotkin and Pretnar (2009) to user-defined monads m,
handlers can be programmed in DM as terms of type

type heap = h:pre heap{∀ (n:nat). n ≥ h.next addr
=⇒ h.mem n==None}

m a → (m b → b) → (a → b) → b

A pre heap is a pair of next addr, the next free memory location
and a memory mem mapping locations to possibly allocated values.
(“a:Type & a” is a dependent pair type of some type a:Type and a
value at that type). A heap is a pre heap with an invariant (stated as
a refinement type) that nothing is allocated beyond next addr.
By taking s=heap in the ST monad of the previous section, we
can program derived actions for allocation, reading, writing and
deallocating references—we show just alloc below; deallocation
is similar, while reading and writing require their references to
be allocated in the current state. First, however, we define an
abbreviation St a pre post, which lets us write specifications using
pre- and postconditions instead of predicate transformers, which can
be more convenient—the F? keywords, requires and ensures are only
there for readability and have no semantic content.

and then imported to F? . We leave a more thorough investigation of
such effect handlers for Dijkstra monads to the future.
An exception-counting state monad: stexnC For another combination of state and exceptions, we define stexnC, which in addition to
combining state and exceptions (in the familiar way), also introduces
an additional integer output that counts the number of exceptions
that are raised. In DM, we write:
let stexnC a = s → τ (option a ∗ (s ∗ int))
let return (x:a) = λ s → Some x, (s, 0)
let bind (m:stexnC a) (f:a → stexnC b) = λ s0 → let r0 = m s0 in
match r0 with
| None, (s1, c1) → None, (s1, c1)
| Some r, (s1, c1) → let res, (s, c2) = f r s1
in res (s, c1 + c2)
let raise () : stexnC a = λ s → None, (s, 1)
let lift (f:st a) : stexnC a = λ s → let x, s1 = f s in Some x, (s1, 0)

let St a pre post = ST a (λ h0 p →
pre h0 ∧ (∗ pre: a predicate on the input state ∗)
∀x h1. post h0 x h1 (∗ post relates result, initial and final states ∗)
=⇒ p (x, h1))

Notice that raise returns an exception count of 1. This count is added
up in bind, à la writer monad. Adding stexnC to F? proceeds as
before. But, we need to be a bit careful with how we use reflection. In
particular, an implicit invariant of stexnC is that the exception count
field in the result is non-negative and actually counts the number
of raised exceptions. If a programmer is allowed to reflect any
s → Pure (option a ∗ (s ∗ int)) wp into an stexnC computation, then
this invariant can be broken. Programmers can rely on F? ’s module
system to simply forbid the use of stexnC.reflect in client modules.
Depending on the situation, the module providing the effect may
still reveal a restricted version of the reflect operator to a client, e.g.,
we may only provide reflect nonneg to clients, which only supports
reflecting computations whose exception count is not negative. Of
course, this only guarantees that the counter over-approximates the
number of exceptions raised, which may or may not be acceptable.

abstract let ref (a:Type) = nat (∗ other modules cannot treat ref as nat ∗)
let alloc (a:Type) (init:a) : St (ref a)
(requires (λ h → True)) (∗ can allocate, assuming infinite mem. ∗)
(ensures (λ h0 r h1 →
h0.mem r == None ∧ (∗ the ref r is fresh ∗)
h1.mem r == Some (| a, init |) ∧ (∗ initialized to init ∗)
(∀ s. r6=s =⇒ h0.mem s == h1.mem s))) (∗ other refs not modified ∗)
= let h0 = get () in (∗ get the current heap ∗)
let r = h0.next addr in (∗ allocate at next addr ∗)
let h1 = {
next addr=h0.next addr + 1; (∗ bump and update mem ∗)
mem = (λ r0 → if r = r0 then Some (| a , x |) else h0.mem r0 )
} in
put h1; r (∗ put the new state and return the ref ∗)

let reflect nonneg (f: s → Pure (option a ∗ (s ∗ int)) wp)
: stexnC a (λ s0 post →
wp s0 (λ (r, (s1, n)) → post (r, (s1, n)) ∧ n ≥ 0))
= reflect f

Forbidding recursion through the store The reader may wonder
if adding mutable references would allow stateful programs to
diverge by recursing through the memory. This is forbidden due
to universe constraints. The type Type in F? includes an implicit
level drawn from a predicative, countable hierarchy of universes.
Written explicitly, the type heap lives in universe Typei+1 since it
contains a map whose co-domain is in Typei , for some universe
level i. As such, while one can allocate references like ref nat or
ref (nat → Tot nat), importantly, ref (a → ST b wp) is forbidden, since
the universe of a → ST b wp is the universe of its representation
a → h:heap → Pure (b ∗ heap) (wp h), which is Typei+1 . Thus, our
heap model forbids storing stateful functions altogether. More finegrained encodings are possible too, e.g., stratifying the heap into
fragments and storing stateful functions that can only read from
lower strata.

The standard combination of state and exceptions (i.e., stexn)
was already provided primitively in F? . The other two combinations
shown here were not previously supported, since F? only allowed
OCaml effects. In the following more advanced subsections, we
present a heap model featuring dynamic allocation (§2.6), the
reconciliation of primitive state and extrinsic reasoning via reify
and reflect (§2.7), and encodings of two other user-defined effects (a
dynamic information-flow control monitor in §2.8 and continuations
in §2.9).
2.6

State with References and Dynamic Allocation

The state monads that we have seen so far provide global state, with
get and put as the only actions. Using just these actions, we can
encode references and dynamic allocation by choosing a suitable
representation for the global state. There are many choices for this
representation with various tradeoffs, but a (simplified) model of
memory that we use in F? is the type heap shown below:1

2.7

type pre heap = {
next addr: nat;
mem : nat → Tot (option (a:Type & a))
}
expressible in F? , types like heap are not expressible in the EMF?
calculus of §3 since it lacks support for features like inductive types and
universe polymorphism.

1 Although

Draft

Relating heap to a Primitive Heap

While one can execute programs using the ST monad instantiated
with heap as its state, in practice, for efficiency, the F? compiler
provides primitive support for state via its extraction facility to
OCaml. In such a setting, one needs a leap of faith to believe that
our model of the heap is faithful to the concrete implementation of
the OCaml heap, e.g., the abstraction of ref a is important to ensure
that F? programs are parametric in the representation of OCaml
references.
More germane to this paper, compiling ST programs primitively
requires that they do not rely concretely on the representation of
ST a wp as h:heap → Pure (a ∗ heap) (wp h), since the OCaml heap
cannot be reified to a value. In §5, we show that source programs

5

2016/11/9

that are free of reflect and reify can indeed be safely compiled
using primitive state (Theorem 10). Without reflect and reify, one
may rely on intrinsic proof to show generally useful properties of
programs. For example, one may use intrinsic proofs to show that ST
computations never use references after they are deallocated, since
reading and writing require their references to be allocated in the
current state. Note, we write r ∈ h for h.mem r == Some , indicating
that r is allocated in h.

The intrinsic specification of incr does not constrain the final
value of r, so calling incr directly here would not be enough for
proving the final assertion. By tagging the call-site with refine St,
we strengthen the specification of incr extrinsically, allowing the
proof to complete as in incr increases.
2.8

let incr (r:ref int) : St unit (requires (λ h → r ∈ h))
(ensures (λ h0 s h1 → r ∈ h1))
= r := !r + 1

Of course, one would still like to show that incr increments its
reference. In the rest of this section, we show how we can safely
restore reflect and reify in the presence of primitive state.

let ifc h = if h then (incr(); let y = get() in decr(); y) else get() + 1

Restoring reify and reflect for extrinsic proofs F? programs using primitive state are forbidden from using reify and reflect only in
the executable part of a program—fragments of a program that are
computationally irrelevant (aka “ghost” code) are erased by the F?
compiler and are free to use these operators. As such, within specifications and proofs, ST programs can be reasoned about extrinsically
via reification and reflection (say, for functional correctness), while
making use of intrinsically proven properties like memory safety.
To restrict their use, as described in §2.5, we rely on F? ’s module
system to hide both the reify and reflect operators from clients of
a module FStar.State defining the ST effect. Instead, we expose
to clients only ghost reify, a function equivalent to reify, but at the
signature shown below. Notice that the function’s co-domain is
marked with the Ghost effect, meaning that it can only be used
within specifications (e.g., WPs and assertions)—any other use will
be flagged as a typing error by F? .

It is easy to prove this program non-interferent via the extrinsic,
relational proof below, which states that regardless of its secret input
(h0, h1), ifc when run in the same public initial state (s0) produces
identical public outputs. This generic extrinsic proof style is in
contrast to Barthe et al. (2014), whose rF? is a custom extension to
F? supporting only intrinsic relational proofs.
let ni ifc = assert (∀ h0 h1 s0. reify (ifc h0) s0 = reify (ifc h1) s0)

Aside from such relational proofs, with user-defined effects, it is
also possible to define monadic, dynamic information-flow control
monitors in DM, deferring non-interference checks to runtime, and to
reason about monitored programs in F? . Here’s a simplified example,
inspired by the floating label approach of LIO (Stefan et al. 2011).
For simplicity, we take the underlying monad to be exnst, where the
state is a security label from a two-point lattice that represents the
secrecy of data that a computation may have observed so far.

ghost reify: (x:a → ST b (wp x))
→ Ghost (x:a → s0:s → Pure (b ∗ s) (wp x s0))

type label = Low | High
let difc a = label → τ (option (a ∗ label))

The FStar.State module also provides refine St, a total function
that allows a client to strengthen the postcondition of an effectful
function f to additionally record that the returned value of f on
any argument and input state h0 corresponds to the computational
behavior of the (ghostly) reification of f. This allows a client to relate
f to its reification while remaining in a computationally relevant
context.

Once added to F? , we can provide two primitive actions to interface with the outside world, where DIFC is the effect corresponding
to difc. Importantly, writing to a public channel using write Low
when the current label is High causes a dynamic failure signaling a
potential Leak of secret information.
let join l1 l2 = match l1, l2 with | , High | High, → High | → Low
val read : l:label → DIFC bool (λ l0 p → ∀b. p (Some (b, join l0 l)))
let flows l1 l2 = match l1, l2 with | High, Low → false | → true
val write : l:label → bool → DIFC unit (λ l0 p →
if flows l0 l then p (Some ((), l0)) else p None)

let refine St (f :(x:a → St b (pre x) (post x)))
: Tot (x:a → St b (pre x) (λ h0 z h1 → post x h0 z h1 ∧
ghost reify f x h0 == z, h1)
= λ x → STATE.reflect (reify (f x))

As before, it is important to not allow untrusted client code
to reflect on DIFC, since that may allow it to declassify arbitrary
secrets. Arguing that DIFC soundly enforces a form of terminationinsensitive non-interference requires a meta-level argument, much
like that of Stefan et al. (2011).
We can now write programs like the one below, and rely on the
dynamic checks to ensure they are secure.

Reasoning using reify ghost instead of reify, clients can still prove
incr increases as in §2.4, making use of incr’s intrinsic specification
to show that if the reference r is allocated before calling incr it will
still be allocated afterwards.

let b1, b2 = read Low, read Low in write Low (b1 && b2)
let b3 = read High in write High (b1 || b3); write Low (xor b3 b3)

let incr increases (r:ref int) (h0:heap{r ∈ h0}) : Ghost unit =
let Some x0 = h0.mem r in
let , h1 = ghost reify incr r h0 in
let Some x1 = h1.mem r in
assert (x1 = x0 + 1)

In this case, we can also prove that the program fails with a None
at the last write Low. In contrast to the relational proof sketched
earlier, dynamic information-flow control is conservative: even
though the last write reveals no information on the low channel,
the monitor still raises an error.

Further, in computationally relevant (non-ghost) code, refine St
allows us to reason using the concrete definition of incr:
let r = ST.alloc 42 in
let n0 = !r in
refine St incr r;
let n1 = !r in
assert(n1 == n0 + 1)

Draft

Information Flow Control

Information-flow control (Sabelfeld and Myers 2006) is a paradigm
in which a program is deemed secure when one can prove that its
behavior observable to an adversary is independent of the secrets
the program may manipulate, i.e., it is non-interferent. Monadic
reification allows us to prove non-interference properties directly,
by relating multiple runs of an effectful program (Benton 2004). For
example, take the simple stateful program below:

2.9

CPS’ing the Continuation Monad

As a final example before our formal presentation, we ask the
irresistible question of whether we can get a Dijkstra monad for free
for the continuation monad itself—indeed, we can.

6

2016/11/9

We start by defining the standard continuation monad, cont, in
Being a subset of F? , we can prove that it is indeed a monad,
automatically.

Terms
e,t, wp, φ

DM .

::= x | T | x:t{φ } | λ x:t.e | x:t → c | e1 e2
|
caset (e as y) x.e1 x.e2 | run e | reify e
|
reflect e | M.liftM 0 t wp e | F.act ē
|
M.return t e | M.bind t1 t2 wp1 e1 wp2 x.e2
Computation types
c
::= Tot t | M t wp where M ∈ {Pure, F}

let cont a = (a → τ ans) → τ ans
let return x = λ k → k x
let bind f g k = f (λ x → g x k)
(∗ cont is a monad ∗)
let right unit cont (f:cont α) = assert (bind f return == f);
let left unit cont (x:α) (f:(α → cont β )) = assert (bind (return x) f == f x)
let assoc cont (f:cont α) (g:(α → cont β )) (h:(β → cont γ)) =
assert (bind f (λ x → bind (g x) h) == bind (bind f g) h)

Signatures of monadic effects and lifts
S ::= D | S, D | S, L

repr
= t ; wp type


return = e ; return?
D ::= F
= e ; bind?

 bind
act j
= e ; act?j
L ::= { M.liftM 0 = e; M.lift? 0 = wp }
M

Following our two-step recipe, we derive the Dijkstra variant
of cont, but first we define some abbreviations to keep the notation
manageable. The type kwp a is the type of a predicate transformer
specifying a continuation a → τ ans; and kans is the type of a
predicate transformer of the computation that yields the final answer.
kwp a =
a → kans
= (a → τ ans)?
kans
= (ans → Type) → Type = (τ ans)?
Using these abbreviations, we show the ?-translation of cont,
return and bind. Instead of being just a predicate transformer,
(cont a)? is a predicate-transformer transformer.
(cont a)? = kwp a → kans
return?
= λ (x:a) (wp k:kwp a) → wp k x
bind?
= λ f g (wp k:kwp b) → f (λ (x:a) → g x wp k)
For step 2, we show the elaboration of return and bind to F? ,
using the abbreviation kt a wp for the type of the elaborated term k,
where the DM term k is a continuation of type a → τ ans and wp=k? .
As illustrated in §2.3, elaborating higher-order functions from DM to
F? introduces additional arguments corresponding to the predicate
transformers of abstracted computations.
kt a wp = x:a → Pure ans (wp x)
return : x:a → wpk:kwp a → k:kt a wpk → Pure ans (return? x wpk)
= λ x wpk k → k x
: wpf:(cont a)?
bind







(Swamy et al. 2016) so that source programs may omit all explicit
uses of the monadic return, bind and lift operators. We do not
revisit that inference algorithm here. Furthermore, EMF? lacks F? ’s
support for divergent and ghost computations, fixed points and their
termination check, inductive types, and universe polymorphism. We
leave extending EMF? to accommodate all these features as future
work, together with a formal proof that after inference, F? terms
can be elaborated into EMF? (along the lines of the elaboration of
Swamy et al. (2011)).
3.1

Syntax

Figure 1 shows the EMF? syntax. We highlight several key features.
Expressions, types, WPs, and formulae are all represented uniformly as terms; however, to evoke their different uses, we often
write e for expressions, t for types, wp for WPs, and φ for logical
formulae. Terms include variables (x, y, a, b, w etc.); refinement types
x:t{φ }; λ abstractions; dependent products with computation-type
co-domains, x:t → c (with the sugar described in §2); and applications. Constants T include Typei , the ith level from a countable
hierarchy of predicative universes.2 We also include constants for
non-dependent pairs and disjoint unions; the former are eliminated
using fst and snd (also constants), while the latter are eliminated
using caset (e as y) x.e1 x.e2 , which is standard dependent pattern
matching with an explicit return type t and a name for the scrutinee
y, provided only when the dependency is necessary.

f:(wpk:kwp a → k:kt a wpk → Pure ans (wpf wpk))
wpg:(a → (cont b)? )
g:(x:a → wpk:kwp b → k:kt b wpk → Pure ans (wpg x wpk))
wpk:kwp b
k:kt b wpk
Pure ans (bind? wpf wpg wpk)
= λ wpf f wpg g wpk k → f (λ x → wpg x wpk) (λ x → g x wpk k)

In the case of return, we have one additional argument for the
predicate transformer of the continuation k—the type of the result
shows how return relates to return? . The elaboration bind involves
many such additional parameters, but the main point to take away is
that its specification is given in terms of bind? , which is applied to
the predicate transformers wpf, wpg, wpk, while bind was applied to
the computations f, g, k. In both cases, the definitions of return and
bind match their pre-images in DM aside from abstracting over and
passing around the additional WP arguments.
To better see the monadic structure in the types of return and
bind we repeat these types, but this time writing cont a wp for the
type wpk:kwp a → k:kt a wpk → Pure ans (wp wpk):
return : x:a → cont a (return? x)
bind : wpf:(cont a)? → f:cont a wpf

Computation types (c) include Tot t, the type of total t-returning
terms, and M t wp, the type of a computation with effect M, return
type t, and behavior specified by the predicate transformer wp. Let
M range over the Pure effect as well as user-defined effects F.
Explicit monadic returns, binds, actions, lifts, reify, and reflect.
M.return and M.bind are the monad operations for the effect M,
with explicit arguments for the types and predicate transformers.
M.liftM 0 t wp e lifts the e : M t wp to M 0 . A fully applied F action
is written F.act ē. The reify and reflect operators are for monadic
reflection, and run coerces a Pure computation to Tot.
Signatures for user-defined effects EMF? is parameterized by a
signature S. A user-defined effect F t wp is specified using D,
the result of translating a DM monad. A definition D is a record
containing several fields: repr is the type of an F computation reified

b)? )

→ wpg:(a → (cont
→ g:(x:a → cont b (wpg x))
→ cont b (bind? wpf wpg)

Explicitly Monadic F?

have yet to model F? ’s universe polymorphism, making the universes
in EMF? less useful than the ones in F? . Lacking universe polymorphism, we
restrict computation to have results in Type0 . A simple remediation would
be replicate the monad definitions across the universe levels.
2 We

We begin our formal development by presenting EMF? , an explicitly
typed, monadic core calculus intended to serve as a model of F? . As
seen above, the F? implementation includes an inference algorithm

Draft

t
wp
wp
x j :t j → c j

Figure 1. Syntax of EMF?

→
→
→
→
→
→

3.

=
=
=
=

7

2016/11/9

as a pure term, wp type is the type of the wp argument to F; return,
bind, and act j are EMF? expressions, and return? , bind? , and act?j
are EMF? WPs (act j is the jth action of F). We use S.F.return to
denote the lookup of the return field from F’s definition in the
signature S, and similar notation for the other fields.
For example, for the ST monad from §2.3, we have3 :
ST{

wp type
repr
return
return?
bind
bind?
get
get?
put
put?

=
=
=
=
=
=
=
=
=
=

T-R EFINE

S; Γ ` e : Tot t
S; Γ ` M.return t e : M t (S.M.return? t e)
T-B IND

S; Γ ` t2 : Type0
S; Γ ` wp2 : x:t1 → S.M.wp type t2
S; Γ ` e1 : M t1 wp1 S; Γ, x:t1 ` e2 : M t2 (wp2 x)
S; Γ ` M.bind t1 t2 wp1 e1 wp2 x.e2 : M t2 (S.M.bind? t1 t2 wp1 wp2 )

λ a.s → (a ∗ s → Type0 ) → Type0
λ a w.s0 :s → Pure (a ∗ s) (w s0 )
λ a.return
λ a.return?
λ a b.bind
λ a b.bind?
get
get?
put
put?
}

T-ACT

S.F.act? = x:t → c
S; Γ ` e : M t wp
∀i. S; Γ ` ei : ti
S; Γ ` M.liftM 0 t wp e : M 0 t (S.M.lift?M 0 wp) S; Γ ` F.act ē : c[ē/x̄]
T-L IFT

T-R EFLECT

T-R EIFY

S; Γ ` e : F t wp
S; Γ ` reify e : Tot (S.F.repr t wp)

where (as described in §2.3) return : a → x:a → repr a (return? a x);
and similarly for bind, get, and put.
In addition to the monad definitions D, the signature S contains
the definitions of lifts that contain an EMF? expression and an EMF?
WP. We use notations S.M.liftM 0 and S.M.lift? 0 to look these up in
M
S. Finally, the signature always includes a fixed partial definition for
the Pure monad, only containing the following definitions:

S; Γ ` e : Pure t wp S; Γ |= ∃p.wp p S; Γ ` e : c0 S; Γ ` c0 <: c
S; Γ ` run e : Tot t
S; Γ ` e : c

C-P URE

S; Γ ` t : Type0
S; Γ ` wp : (t → Type0 ) → Type0
S; Γ ` Pure t wp : Type0

S-T OT

S; Γ ` t 0 <: t
S; Γ ` Tot t 0 <: Tot t

S; Γ ` S.F.repr t wp : Type0
S; Γ ` F t wp : Type0

S-P URE

S; Γ ` t 0 <: t S; Γ |= ∀p.wp p ⇒ wp0 p
S; Γ ` Pure t 0 wp0 <: Pure t wp
S-P ROD

S-F

S; Γ ` S.F.repr t 0 wp0 <: S.F.repr t wp
S; Γ ` F t 0 wp0 <: F t wp

Static Semantics

The expression typing judgment in EMF? has the form S; Γ ` e : c,
where Γ is the list of bindings x : t as usual. Selected rules for the
judgment are shown in Figure 2. In the rules, we sometimes write
S; Γ ` e : t as an abbreviation for S; Γ ` e : Tot t.

S-R EFINE R

S; Γ ` t <: t 0
S; Γ, x : t ` c0 <: c
S; Γ ` x:t 0 → c0 <: x:t → c

S-C ONV

S ` t 0 −→∗ t ∨ S ` t −→∗ t 0
S; Γ, x : t |= φ
S; Γ ` x:t{φ } <: t S; Γ ` t <: x:t{φ }
S; Γ ` t 0 <: t

S-R EFINE L

Monadic returns, binds, lifts, and actions. Rules T-R ETURN,
T-B IND, and T-L IFT simply use the corresponding wp specification from the signature for M to compute the final wp. For example, in the case of the ST monad from §2.3, S.ST.return? t =
λ x:t.λ s0 :s.λ post.post (x, s0 ). Rule T-ACT is similar; it looks up
the type of the action from the signature, and then behaves like the
standard function application rule.

Figure 3. Selected subtyping rules for EMF?
and p =⇒ q from §2, are encoded as x:unit{p ∗ q} and x:unit{p → q},
and reside in Type0 . Similar to T-R EFINE, in C-P URE, the universe
of a computation type is determined only by the result type. Since
the wp is proof irrelevant, the use of Type0 in the type of wp is
quite natural, because its proof content is always squashed. For
user-defined monads F, the rule C-F delegates to their underlying
representation S.F.repr.

Monadic reflection and reification. Rules T-R EIFY and TR EFLECT are dual, coercing between a computation type and its
underlying pure representation. Rule T-RUN coerces e from type
Pure t wp to Tot t. However, since the Tot type is unconditionally
total, the second premise of the rule checks that the wp is satisfiable.

Subsumption and subtyping judgment. T-S UB is a subsumption
rule for computations, which makes use of the two judgments S; Γ `
c <: c0 and S; Γ ` t <: t 0 , shown (selectively) in Figure 3. Rule SP URE checks that t 0 <: t, and makes use of the S; Γ |= φ relation to
check that wp is stronger than wp0 , i.e. for all postconditions, the
precondition computed by wp implies the precondition computed
by wp0 .
Similar to C-F, the rule S-F delegates the check to the underlying
representation of F. Rule S-P ROD is the standard dependent function
subtyping. Rule S-R EFINE L permits dropping the refinement from
the subtype, and rule S-R EFINE R allows subtyping to a refinement

Refinements, computations types, and proof irrelevance. EMF? ’s
refinement and computation types include a form of proof irrelevance. In T-R EFINE, the universe of x:t{φ } is determined by the
universe of t alone, since a witness for the proposition φ is never materialized. Refinement formulas φ and wps are manipulated using an
entailment relation, S; Γ |= φ , for a proof-irrelevant, classical logic
where all the connectives are “squashed” (Nogin 2002), e.g., p ∧ q

Draft

C-F

Figure 2. Selected typing rules for EMF?

The other fields are not defined, since Pure is handled primitively
in the EMF? dynamic semantics (§3.3).
The well-formedness conditions on the signature S (shown in
the auxiliary material) check that the fields in definitions D and the
lifts in L are well-typed as per their corresponding WPs. In addition,
each effect definition can make use of the previously defined effects,
enabling a form of layering. However, in this paper, we mainly focus
on combining effects using the lift operations.

3 We

S; Γ ` e : Tot (S.F.repr t wp)
S; Γ ` reflect e : F t wp
T-S UB

T-RUN

Pure { wp type = λ a:Type0 . (a → Type0 ) → Type0
return? = λ a:Type0 . λ x:a. λ p:(a → Type0 ). p x
bind? = λ a. λ b. λ w1 . λ w2 . λ p. w1 (λ x. (w2 x) p) }

3.2

S; Γ ` t : Typei
S; Γ, x:t ` φ : Type j
S; Γ ` x:t{φ } : Typei

T-R ETURN

use sans serif font for the actual field values.

8

2016/11/9

R-A PP

R-RUN

S ` (λ x:t.e) e0 −→ e[e0 /x]

S ` run (Pure.return t e) −→ e

Note that in this case, we don’t need to reify e (as we did in bind),
because e is already a Tot term.
Semantics for monadic lifts and actions. Rules R-R EIFYACT
and R-R EIFY L IFT also lookup the underlying implementations
of the lifts and actions in the signature and use them. Rule RR EIFY L IFT in addition reifies the computation e. For lifts, the
arguments ē are already Tot.

R-P URE B IND

S ` Pure.bind t1 t2 wp1 (Pure.return t e1 ) wp2 x.e2 −→ e2 [e1 /x]
R-R EIFY R EFLECT

R-R EIFY R ET

S ` reify (F.return t e) −→ S.F.return t e S ` reify (reflect e) −→ e

3.4

EMF ?

Metatheory

We prove several metatheoretical results for EMF? . First, we prove
strong normalization for EMF? via a translation to the calculus of
inductive constructions (CiC) (Paulin-Mohring 2015).

R-R EIFY B IND

e0 = S.F.bind t1 t2 wp1 (reify e1 ) wp2 x.(reify e2 )
S ` reify (F.bind t1 t2 wp1 e1 wp2 x.e2 ) −→ e0

Theorem 1 (Strong normalization). If S; Γ ` e : c and CiC is
strongly normalizing, then e is strongly normalizing.

R-R EIFYACT

S ` reify(F.act ē) −→ S.F.act ē
Proof. (sketch) The proof proceeds by defining a translation from
EMF ? to CiC, erasing refinements and WPs, inlining the pure
implementations of each monad, and removing the reify and reflect
operators. We show that this translation is a type-preserving, forward
simulation. If CiC is strongly normalizing, then EMF? must also be,
since otherwise an infinite reduction sequence in EMF? could not be
matched by CiC, contradicting the forward simulation.

R-R EIFY L IFT

S ` reify(M.liftM 0 t wp e) −→ S.M.liftM 0 t wp (reify e)
Figure 4. Dynamic semantics of EMF? (selected reduction rules)
type, if we can prove the formula φ for an arbitrary x. Finally, rule SC ONV states that the beta-convertible types are subtypes of each
other (S ` t −→ t 0 is the small-step evaluation judgment, introduced
in the next section).
3.3

EMF ?

Theorem 2 (Subject Reduction). If S; Γ ` e : c and S ` e −→ e0 ,
then S; Γ ` e0 : c.
This allows us to derive a total correctness property for the
Pure monad saying that run-ing a Pure computation produces a
value which satisfies all the postconditions that are consistent with
the wp of the Pure computation.

Dynamic Semantics

We now turn to the dynamic semantics of EMF? , which is formalized
as a strong small-step reduction relation. Evaluation context are
defined as follows:
E ::= • | λ x:t.E | E e | e E | run E | reify E | reflect E
|
M.bind t1 t2 wp1 E wp2 x.e2 | M.return t E
|
M.liftM 0 t wp E | F.act ē E ē0 | caset (E as ) x.e1 x.e2
|
caset (e as ) x.E1 x.e2 | caset (e as ) x.e1 x.E2

Corollary 3 (Total Correctness of Pure). If S; · ` e : Pure t wp, then
∀p. S; · ` p : t → Type0 and S; · |= wp p, we have S ` run e −→∗ v
such that S; · |= p v.
For the user-defined monads F, we can derive their total correctness property by appealing to the total correctness of the
Pure monad. For instance, for the ST monad from §2.3, we can derive the following corollary simply by using the typing of reify and
Corollary 3.

S ` e −→ e0 .

The judgment has the form
We show some selected
rules in Figure 4. The main ideas of the judgment are: (a) the Tot
terms reduce primitively in using a strong reduction semantics, (b)
Pure.bind is also given a primitive semantics, however (c) to β reduce other monadic operations (binds, returns, actions, and lifts),
they need to be reified first, which then makes progress using their
underlying implementation in the signature.

Corollary 4 (Total Correctness of ST ). If S; · ` e : ST t wp, then
∀p, s0 . S; · ` s0 : s, S; · ` p : t × s → Type0 and S; · |= wp s0 p, then
S ` run ((reify e) s0 ) −→∗ v such that S; · |= p v.

Order of evaluation. Since the effectful terms reduce via reification, the semantics does not impose any evaluation order on the
effects—reification yields Tot terms (T-R EIFY), that reduce using
the strong reduction semantics. However, the more familiar sequencing semantics of effects can be recovered by controlled uses of reify
that do not break the abstraction of effects arbitrarily. Indeed, we
formalize this notion in Section 5, and prove that by sequencing the
effects as usual using bind, and then reifying and reducing the entire
effectful term, one gets the expected strict evaluation semantics
(Theorem 10).

3.5

The implementation of F? was relatively easy to adapt to EMF? . In
fact, EMF? and DM and the translation between them were designed
to match F? ’s existing type system, as much as possible. We describe
the main changes that were made.
User-defined non-primitive effects are, of course, the main new
feature. Effect configurations closely match the D form from Figure 1, the main delta being that non-primitive effects include pure
implementations or M.bind, M.return, M.liftM 0 etc.

Semantics for Pure terms. Rule R-P URE B IND reduces similarly
to the usual β -reduction. For run e, the semantics first evaluates e to
Pure.return t e0 , and then run removes the Pure.return and steps
to the underlying total computation e0 via R-RUN.

Handling reify and reflect in the type-checker involved implementing the two relatively simple rules for them in Figure 2. A more
significant change was made to F? ’s normalization machinery, extending it to support rules that trigger evaluation for reified, effectful
programs. In contrast, before our changes, F? would never reduce
effectful terms. The change to the normalizer is exploited by F? ’s
encoding of proof obligations to an SMT solver—it now encodes the
semantics of effectful terms to the solver, after using the normalizer
to partially evaluate a reified effectful term to its pure form.

Semantics for monadic returns and binds. Rule R-R EIFY B IND
looks up the underlying implementation S.F.bind in the signature,
and applies it to e1 and e2 but after reifying them so that their effects
are handled properly. In a similar manner, rule R-R EIFY R ET looks
up the underlying implementation S.F.return and applies it to e.

Draft

Implementation in F?

9

2016/11/9

4.

Dijkstra Monads for Free

The syntax for terms is (κ standing for constants):

This section formally presents DM, a language for defining effects
by giving monads with their actions and lifts between them. Via a
pair of translations, we export such definitions to EMF? as effect
configurations. The first translation of a term e, a CPS, written e?
produces a predicate-transformer from DM term; the second one is
an elaboration, e, which produces an EMF? implementation of a
DM term. The main result shows that for any DM term the result of
the ?-translation is in a suitable logical relation to the elaboration
of the term, and thus a valid specification for this elaboration. We
also show that the ?-translation always produces monotonic and
conjunctive predicates, properties that should always hold for WPs.
Finally, we show that the ?-translation preserves all equalities in
DM , and thus translates DM monads into EMF ? Dijkstra monads.

e

::=
|
|
|

x | e e | λ x:H. e | κ(e, . . . , e)
(e, e) | fst(e) | snd(e)
inl(e) | inr(e) | case e inl x:A. e; inr y:A. e
returnτ e | bindτ e to x in e

Typing judgments have the forms ∆ | Γ ` e : H ! n and ∆ | Γ ` e : A ! τ,
where ∆ is a finite sequence of type variables and Γ is a normal
typing context, whose types only use type variables from ∆. Here
are some example rules:
ε

∆ | Γ ` bindτ e1 to x in e2 : A0 !τ

4.2

The ?-translation

The essence of the ?-translation is to translate returnτ e and
bindτ e1 to x in e2 to the returns and binds of the continuation
monad. We begin by defining a translation H ? , that translates any H
type to the type of its predicates by CPS’ing the τ-arrows. First, for
any τ-free type A, A? is essentially the identity, except we replace
n
every arrow →
− by a →. Then, for computation types, we define:

n

X |b|A→
− A | A+A | A×A
A|C
τ
n
H−
→A|H →
− C | C ×C

n

(H →
− C)?
(C ×C0 )?
τ
(H −
→ A)?

=
=
=

H ? → C?
C? ×C0?
H ? → (A? → Type0 ) → Type0

Note that all arrows on the right hand side have a Tot codomain, as
per our notational convention.
In essence, the codomains of τ-arrows are CPS’d into a WP,
which takes as argument a predicate on the result and produces a
predicate representing the “precondition”. All other constructs are
just translated recursively: the real work is for the τ-arrows.
τ
For example, for the state monad S −
→ (X × S), the ?-translation
?
produces the EMF type S → (X × S → Type0 ) → Type0 . It is the
type of predicates that map an initial state and a postcondition (on
both result and state) into a proposition. Modulo isomorphism (of
the order of the arguments and currying)5 this is exactly the type of
WPs in current F? ’s state monad (cf. §1, §2.3).
The two main cases for the ?-translation for well-typed DM
terms are shown below; every other case is simply a homomorphic
application of ? on the sub-terms.

Here X ranges over type variables (needed to define monads)
and b are base types. The τ-arrows represent functions with a
monadic result, and our translations will provide WPs for these
arrows. A types are referred to as “τ-free”, since they contain no
monadic operations. C types are inherently computational in the
sense that they cannot be eliminated into an A type: every possible
elimination will lead to a monadic term. They are referred to as
“computational types”. H types are the union of both, and are called
“hypothesis” types, as they represent the types of possible functional
arguments. As an example, the state monad is represented as the
τ
type S −
→ (X × S), where X is a type variable and S is some type
representing the state. We will exemplify our main results for terms
of this type, thus covering every stateful computation definable in
DM .
DM types do not include “mixed” A × C pairs, computational
n
sums C + H, functions of type C →
− A, or types with right-nested
τ-arrows. We do allow nesting τ-arrows to the left, providing the
generality needed for the continuation monad, and others. These
restrictions are crafted to carefully match EMF? . Without them, our
translations, would generate ill-typed or logically unrelated EMF?
terms, and these restrictions do not appear to be severe in practice,
as evidenced by the examples in §2.

(returnτ e)?
=λ p:(A? → Type0 ). p e? when ∆ | Γ ` e : A!n
(bindτ e1 to x in e2 )? =λ p:(A0? → Type0 ). e?1 (λ x:A. e?2 p)
0
when ∆ | Γ, x : A ` e2 : A !τ
Formally, the ?-translation and elaboration are defined over a
typing derivation, as one needs more information than what is
present in the term. The ?-translations of terms and types are
related in the following sense, where we define the environments
∆ as X1 : Type0 , . . . , Xn : Type0 when ∆ = X1 , . . . , Xn ; and Γ? as
x1 : t1? , . . . xn : tn? when Γ = x1 : t1 , . . . xn : tn (we assume that variables
and type variables are also EMF? variables).

4 In this formalization, bind and return appear explicitly in source programs.
When using our implementation, however, the user need not call bind and
return; rather, they write programs in a direct style, and let-bindings are
turned into binds as needed. §4.6 provides some details on the interpretation
and elaboration of concrete F? terms as DM terms.

Draft

∆ | Γ, x : A ` e2 : A0 !τ

In these rules we implicitly assume that all appearing types are
well-formed with respect to the grammar, e.g., one cannot form a
n
function of type C →
− A by the abstraction rule.
As an example, returnST = λ x:X. λ s:S. returnτ (x, s) has type
n
τ
X→
− S−
→ (X × S), using these rules.
When defining effects and actions, one deals (at a top level) with
non-effectful C types (C ! n).

The source language DM is a simply-typed lambda calculus augmented with an abstract monad τ, as in §2.3. The language is essentially that of Filinski (1994) with certain restrictions on allowed
types to ensure the correctness of elaboration.
There are two effect symbols: n (non-effectful) and τ. The typing
judgment is split accordingly, and ε ranges over both of them. Every
monadic term needs to be bound via bindτ to be used.4 Functions
can only take non-effectful terms as arguments, but may return a
monadic result.
The set of DM types is divided into A types, H types, and C types,
ranged over by A, C, and H, respectively. They are given by the
grammar:
::=
::=
::=

∆ | Γ ` f e : H 0 !ε
∆ | Γ ` e1 : A!τ

∆ | Γ ` e : A!n

Source: DM Effect Definition Language

A
H
C

∆|Γ` f :H →
− H 0 !n ∆ | Γ ` e : H!n

∆ | Γ ` λ x:H. e : H →
− H 0 !n
∆ | Γ ` returnτ e : A!τ

4.1

ε

∆ | Γ, x:H ` e : H 0 !ε

5 One

can tweak our translation to generate WPs that have the usual
postcondition to precondition shape. However we found the current shape to
be generally easier to work with.

10

2016/11/9

Theorem 5 (well-typing of ?-translation).
∆ | Γ ` e : C ! n implies ∆, Γ? ` e? : C? .

Computational abstractions and applications (cases 4 and 10)
Case (4) translates a function with a computational argument x:C
to a function that expects two arguments, a specification xw :C? and
x itself, related to xw at a suitably translated type. We track the
association between x and xw using a substitution sΓ , which maps
every computational hypothesis x : C in Γ to xw (of type C? ) in Γ,
In case (10), when passing a computation argument e2 , we need
to eliminate the double abstraction introduced in case (4), passing
both e?2 sΓ , i.e. the specification of e2 where we substitute the free
computation variables, and e2 itself.

After translating a closed term e, one can abstract over the
variables in ∆ to introduce the needed polymorphism in EMF? . This
will also be the case for elaboration.
As an example, for the previous definition of returnST we get the
translation λ x:X. λ s:S. λ p:(X × S → Type0 ). p(x, s), which has the
required transformer type: X → S → (X × S → Type0 ) → Type0
(both with X as a free type variable). It is what one would expect: to
prove a postcondition p about the result of running returnST x, one
needs to prove p(x, s) where s is the initial state.
4.3

Return and bind (cases 14 and 15) The last two rules show the
translation of return and bind for τ to return and bind for Pure in
EMF? . This is one of the key points: in the elaboration, we interpret
the τ as the identity monad in EMF? , whereas in the ?-translation,
we interpret τ as the continuation monad. Theorem 6, our main
theorem, shows that EMF? ’s WP computation in the Pure monad for
e produces a WP that is logically related to the ?-translation of e,
i.e., WPs and the CPS coincide formally, at arbitrary order.

Elaboration

Elaboration is merely a massaging of the source term to make it
properly typed in EMF? . During elaboration, monadic operations are
translated to those of the identity monad in EMF? , namely Pure.
Elaboration of types We define two elaboration translations
for DM types, which produce the EMF? types of the elaborated
expression-level terms. The first translation A maps an A type to
a simple EMF? type, while the second one FC wp maps a C type
and a specification wp of type C? into an EMF? computation type
containing Tot and Pure arrows. The A translation is the same as the
CPS one, i.e., A = A? .
The FC wp (where wp : C? ) translation is defined by:
(1)

FC×C0 wp

=def

FC (fst wp) × FC0 (snd wp)

(2)

F

ε

wp

=def

w0 :C? → FC w0 → GεH (wp w0 )

(3)

F

ε

wp

=def

x:A → GεH (wp x)

C−
→H
A−
→H

Theorem 6 (Logical relations lemma).
1.
2.

=⇒
=⇒

∆, Γ ` e : FC (e? sΓ )
∆, Γ ` e : Pure A (e? sΓ )

Where Γ is defined by mapping any “x : A” binding in Γ to
“x : A” and any “y : C” binding to “yw : C? , y : FC yw ”. Instantiating
(1) for an empty Γ, we get as corollary that ∆ ` e : FC e? , representing the fact that e? is a proper specification for e. Following
the ST monad example, this implies that for any source term e
τ
such that X | · ` e : S −
→ (X × S) holds, then X : Type0 ` e : s0 :S →
?
Pure (X × S) (e s0 ), will hold in EMF? , as intuitively expected.

Here we define GCn (wp) = FC wp and GτA (wp) = Pure A wp.
The main idea is that if an EMF? term e has type FC wp, then
wp is a proper specification of the final result. Putting pairs aside
for a moment, this means that if one applies enough arguments
ei to e in order to eliminate it into a Pure computation, then
e e¯i : Pure A (wp s¯i ), where each si is the specification for each
ei . This naturally extends to pairs, for which the specification is a
pair of proper specifications, as shown by case (1) above.
In case (2), the w0 : C? arguments introduced by F are relevant for
the higher-order cases, and serve the following purpose, as illustrated
in §2.3 (for the translation of bind for the ST monad) and §2.9 (for
the continuation monad): when taking computations as arguments,
we first require their specification in order to be able to reason
about them at the type level. Taking these specification arguments
is also the only way for being WP-polymorphic in EMF? . Note that,
according to the dependencies, only the C? argument is used in the
specifications, while we shall see in the elaboration of terms that
only the FC wp argument is used in terms. When elaborating terms,
we pass this specification as an extra argument where needed.
In case (3), when elaborating functions taking an argument of A
type there is no need to take a specification, since the argument is
completely non-effectful and can be used at both the expression
and the type levels. Informally, a non-effectful term is its own
specification.
Returning to our state monad example, the result of F τ
wp
S−
→(X×S)
is s:S → Pure (X × S) (wp s), i.e., the type of a function f such that
for any post-condition p and states s for which one can prove the
pre-condition wp s p, we have that f s satisfies p.

4.4

Monotonicity and Conjunctivity

A key property of WPs is monotonicity: weaker postconditions
should map to weaker preconditions. This is also an important F?
invariant that allows for logical optimizations of WPs. Similarly,
WPs are conjunctive: they distribute over conjunction and universal
quantification in the postcondition. We show that any EMF? term
obtained from the ?-translation is monotonic and conjunctive,
for higher-order generalizations of the usual definitions of these
properties (Dijkstra 1997).
We first define a logical relation between EMF? terms t1 .t t2 ,
read “t1 stronger than t2 at type t” and producing an EMF? formula
in Type0 , by recursion on the structure of t:
x .Type0 y =def
x .b y
=def
x .X y
=def
f .t1 →t2 g =def
x .t1 ×t2 y =def
x .t1 +t2 y =def

x⇒y
x == y
x == y
∀x, y : t1 . x .t1 x ∧ x .t1 y ∧ y .t1 y ⇒ f x .t2 g y
fst x .t1 fst y ∧ snd x .t2 snd y
(∃v1 , v2 : t1 , x == inl v1 ∧ y == inl v2 ∧ v1 .t1 v2 ) ∨
(∃v1 , v2 : t2 , x == inr v1 ∧ y == inr v2 ∧ v1 .t2 v2 )

where b represents any EMF? base type (i.e., a type constant in
Type0 ) and X any type variable6 . The symbol == represents EMF? ’s
squashed propositional equality. The . relation is only defined for
the subset of EMF? types that are all-Tot and non-dependent. All
types resulting from the ?-translation are in this subset, so this not a
limitation for our purposes. A type t in this subset is called predicatefree when it does not mention Type0 . For any predicate-free type t
the relation .t reduces to extensional equality.
The . relation is not reflexive. We say that an EMF? term e of
type t is monotonic when e .t e. Note that monotonicity is preserved
by application. For first-order WPs this coincides with the standard

Elaboration of terms is defined in Figure 5 and is, as expected,
mostly determined by the translation of types. The translation is
formally defined over typing derivations, however, for brevity, we
present each translation rule simply on the terms, with the important
side-conditions we rely on from the derivation shown in parenthesis.
We describe only the most interesting cases.

Draft

∆ | Γ ` e : C!n
∆ | Γ ` e : A!τ

6 We can get a stronger result if we don’t restrict the relation on type variables

to equality and treat it abstractly instead. For our purposes this is not needed
as we plan to instantiate type variables with predicate-free types.

11

2016/11/9

(1)
(2)
(3)
(4)
(9)
(10)
(11)
(12)
(13)
(14)
(15)

x
κ(e1 , . . . , en )
λ x:A. e
λ x:C. e
e1 e2
e1 e2
(e1 , e2 )
case e inl x:A1 . e1 ; inr y:A2 . e2
case e inl x:A1 . e1 ; inr y:A2 . e2
returnτ e
bindτ e1 to x:A in e2

=
=
=
=
=
=
=
=
=
=
=

x
(5) fst(e)
κ e1 . . . en
(6) snd(e)
λ x:A. e
(7) inl(e)
λ xw :C? . λ x:FC xw . e (8) inr(e)
e1 e2
e1 (e?2 sΓ ) e2
(e1 , e2 )
case(e) x.e1 y.e2
caseFC case(z) x.(e?1 sΓ ) y.(e?2 sΓ ) (e as z) x.e1 y.e2
Pure.return A e
Pure.bind A A0 (e?1 sΓ ) e1 (λ x:A? . e?2 sΓ ) x.e2

= fst e
= snd e
= inl e
= inr e
(∆ | Γ ` e2 : A ! n)
(∆ | Γ ` e2 : C ! n)
(∆ | Γ, x:A1 ` e1 : A ! ε)
(∆ | Γ, x:A1 ` e1 : C ! n)
(∆ | Γ ` e : A ! τ)
(∆ | Γ, x : A ` e2 : A0 ! τ)

Figure 5. The elaboration of DM terms to EMF?
definitions, and for higher-order predicates it gives a reasonable
extension. Since the relation reduces to equality on predicate-free
types, every term of such a type is trivially monotonic. The reader
can also check that every term of a type t = d1 → · · · → dn → Type0
(where each di is predicate-free) is monotonic; it is only at higherorder that monotonicity becomes interesting.
For a first-order example, let’s take the type of WPs for programs
in the ST monad: S → (X × S → Type0 ) → Type0 , making use of
the previous simplification:
≡
⇐⇒
≡
⇐⇒

describes the predicate-free types (including variables).
C(a→Type0 )→Type0 (w) =def
Ca (x)
=def
Ct1 →t2 ( f )
=def
=def
Ct1 ×t2 (p)

Again, the relation is not defined on all types, but it does include
the image of the type-level ?-translation, so it is enough for our
purposes. This relation is trivially preserved by application, which
allows us to prove the following theorem:

f .S→(X×S→Type0 )→Type0 f
∀s1 , s2 . s1 = s1 ∧ s1 = s2 ∧ s2 = s2 ⇒ f s1 . f s2
∀s. f s .(X×S→Type0 )→Type0 f s
∀s, p1 , p2 . p1 . p2 ⇒ f s p1 .Type0 f s p2
∀s, p1 , p2 . (∀x, s0 . p1 (x, s0 ) ⇒ p2 (x, s0 )) ⇒ ( f s p1 ⇒ f s p2 )

Theorem 8 (Conjunctivity of ?-translation).
For any e and C, ∆ | · ` e : C ! n implies ∆  CC? (e? )
For the ST monad, this implies that for any e such that
τ
e:S−
→ X × S we know, again within EMF? , that e? s p1 ∧ e? s p2 =
?
e s (λ x.p1 x ∧ p2 x) for any s, p1 , p2 . This is the usual notion of
conjunctivity for WPs of this type.

This is exactly the usual notion of monotonicity for imperative
programs (Dijkstra 1997): “if p2 is weaker than p1 , then f s p2 is
weaker than f s p1 for any s”.
Now, for a higher-order example, consider the continuation
τ
τ
monad in DM: Cont X = (X −
→ R) −
→ R, where X is the type variable and R some other variable representing the end result of the
computation. The type of WPs for this type is

4.5

The ?-translation Preserves Equality and Monad Laws

We define an equality judgment on DM terms that is basically β ηequivalence, augmented with the monad laws for the abstract τ
monad. We show that the ?-translation preserves this equality.
Theorem 9 (Preservation of equality by CPS).
If ∆ | · ` e1 = e2 : H ! ε then ∆  e?1 == e?2 .

Contwp X = (X→(R→Type0 )→Type0 ) → (R→Type0 )→Type0
Modulo argument swapping, this maps a postcondition on R to a
precondition on the specification of the continuation function. The
condition wp .Contwp X wp reduces and simplifies to:

Since the monad laws are equalities themselves, any source
monad will be translated to a specification-level monad of WPs.
This also applies to lifts: source monad morphisms are mapped to
monad morphisms between Dijkstra monads.

kw1 . kw1 ∧ kw1 . kw2 ∧ kw2 . kw2 ∧ p1 . p2
=⇒ wp kw1 p1 =⇒ wp kw2 p2

4.6

for any kw1 , kw2 , p1 , p2 of appropriate types. Intuitively, this means
that wp behaves monotonically on both arguments, but requiring
that the first one is monotonic. In particular, this implies that for any
monotonic kw, wp kw is monotonic at type (R → Type0 ) → Type0 .
We proved that the ?-translation of any well-typed source term
e : C ! n gives a monotonic e? at the type C? . This result is more
general than it appears at a first glance: not only does it mean that
the WPs of any defined return and bind are monotonic, but also
those of any action or function are. Also, lifts between monads
and other higher-level computations will preserve this monotonicity.
Furthermore, the relation  in the conclusion of the theorem below
is EMF? ’s validity judgment, i.e., we show that these properties are
actually provable within F? without relying on meta-level reasoning.

Implementing the Translations in F?

We devised a prototype implementation of the two translations in
F? . Users define their monadic effects as F? terms in direct style,
as done in §2, and these definitions get automatically rewritten
τ
into DM. As explained in §2, instead of τ-arrows (H −
→ A), we
?
use a distinguished F effect τ to indicate where the CPS should
occur. The effect τ is defined to be an alias for F? ’s Tot effect,
which allows the programmer to reason extrinsically about the
definitions and prove that they satisfy various properties within
F? , e.g., the monad laws. Once the definitions have been typechecked in F? , another minimalist type-checker kicks in, which
has a twofold role. First, it ensures that the definitions indeed belong
to DM, e.g., distinguishing A types from C types. Second, it performs
bidirectional inference to distinguish monadic computations from
pure computations, starting from top-level annotations, and uses
this type information to automatically introduce returnτ and bindτ
as needed. For instance, in the st example from §2.3, the typechecker rewrites x, s0 into returnτ (x, s0 ); and let x, s1 = f s0 in ...
into bindτ f s0 to x, s1 in . . . ; and g x s1 into returnτ (g x s1 ).
The elaboration maps let-bindings in DM to let-bindings in F? ; the

Theorem 7 (Monotonicity of ?-translation).
For any e and C, ∆ | · ` e : C ! n implies ∆  e? ≤C? e? .
We give a similar higher-order definition of conjunctivity, and
prove similar results ensuring the ?-translation produces conjunctive
WPs. The definition for conjunctivity is given below, where a

Draft

∀p1 , p2 . w p1 ∧ w p2 = w (λ x.p1 x ∧ p2 x)
true
∀x : t1 . Ct1 (x) ⇒ Ct2 ( f x)
Ct1 (fst p) ∧ Ct2 (snd p)

12

2016/11/9

general inference mechanism in F? takes care of synthesizing the
WPs, meaning that the elaboration, really, is only concerned about
extra arguments for abstractions and applications.
Once the effect definition is rewritten to DM, our tool uses the
?-translation and elaboration to generate the WP transformers for
the Dijkstra monad, which previously would be written by hand.
Moreover, several other WP combinators are derived from the WP
type and used internally by the F? type-checker; again previously
these had to be written by hand.

5.

EMF?

state threaded sequentially as the telescope evolves. We describe this
invariant structure as an EMF? context, K, parameterized by a state
s. In the definition, Ê is a single-hole, reify-and-reflect-free EMF?
context, a refinement of the evaluation contexts of §3, to be filled by
a reify-and-reflect free EMF? term, f . Additionally, we separate the
Ê contexts by their effect into several sorts: Ê : Tot and Ê : Pure are
contexts which when filled by a suitably typed term produce in EMF?
a Tot or Pure term, respectively; the case Ê : Inert is for an un-reified
stateful EMF? term. The last two cases are the most interesting: they
represent the base and inductive case of the telescope of a stateful
term “caught in the act” of reducing—we refer to them as the Active
contexts. We omit the sort of a context when it is irrelevant.

with Primitive State

As we have seen in §3, EMF? encodes all its effects using pure
functions. However, one would like to be able to run F? programs
efficiently using primitively implemented effects. In this section, we
show how EMF? ’s pure monads apply to F? ’s existing compilation
strategy, which provides primitive support for state via compilation
to OCaml, which, of course, has state natively.7 The main theorem
of §5.2 states that well-typed EMF? programs using the state monad
abstractly (i.e., not breaking the abstraction of the state monad
with arbitrary uses of reify and reflect) are related by a simulation
to EMF?ST programs that execute with a primitive notion of state.
This result exposes a basic tension: although very useful for proofs,
reify and reflect can break the abstractions needed for efficient
compilation. However, as noted in §2.6, this restriction on the use
of reify and reflect only applies to the executable part of a program—
fragments of a program that are computationally irrelevant are erased
by the F? compiler and are free to use these operators.
5.1

EMF ?ST :

K s ::= Ê : Tot | Ê : Pure | Ê : Inert | reify Ê s : Active
| Pure.bind (K s) p.((λ x.reify f ) (fst p) (snd p)) : Active
(if K s : Active)
Next, we define a simple translation {[·]} from contexts K s to EMF?ST .
{[Ê]} = Ê
{[reify Ê s]} = Ê
{[Pure.bind (K s) p.((λ x.reify f ) (fst p) (snd p))]}
= ST.bind {[K s]} x. f
The definition of {[·]} further illustrates why we need to structure
the Active contexts as a telescope—because not every stateful
computation that can reduce in EMF? is of the form reify e. For
example, the reduction rule R-R EIFY B IND pushes reify inside
the arguments of bind. As a result, one needs to perform several
“administrative” steps of reduction to get the resulting term back
to being of the form reify e. However, in order to show that EMF?ST
can indeed be used as a compiler target for EMF? , we crucially
need to relate all such intermediate redexes to ST computations in
EMF?ST —thus the telescope-like definition of the Active contexts.
Finally, we prove the simulation theorem for EMF? and EMF?ST ,
which shows that one or more steps of reduction in EMF?ST are
matched by one or more steps in EMF? , in a compatible way.

A Sub-Language of EMF? with Primitive State

The syntax of EMF?ST corresponds to EMF? , except, we configure it to
just use the ST monad. Other effects that may be added to EMF? can
be expanded into their encodings in its primitive Pure monad—as
such, we think of EMF?ST as modeling a compiler target for EMF?
programs, with ST implemented primitively, and other arbitrary
effects implemented purely. We thus exclude reify and reflect from
EMF ?ST , also dropping type and WP arguments of return, bind and
lift operators, since these are no longer relevant here.
The operational semantics of EMF?ST is a small-step, call-byvalue reduction relation between pairs (s, e) of a state s and a
term e. The relation includes the pure reduction steps of EMF?
that simply carry the state along (we only show ST-beta), and three
primitive reduction rules for ST, shown below. The only irreducible
ST computation is ST.return v. Since the state is primitive in EMF?ST ,
the term ST.bind e x.e0 reduces without needing an enclosing reify.
(s, (λ x:t.e)v) (s, e[v/x])
(s, ST.bind (ST.return v) x.e) (s, e[v/x])
(s, ST.get ()) (s, ST.return s)
(s, ST.put s0 ) (s0 , ST.return ())
5.2

Relating

EMF ?

to

Theorem 10 (Simulation). For all well-typed, closed, filled contexts
K s f , either K s is Inert, or one of the following is true:
(1) ∃K 0 s0 f 0 . (s, {[K s]} f ) + (s0 , {[K 0 s0 ]} f 0 )
and K s f −→+ K 0 s0 f 0 and sort (K s) = sort (K 0 s0 )
and if K 0 s0 is not Active then s = s0 .
(2) K s is Active and ∃v s0 . (s, {[K s]} f ) ∗ (s0 , ST.return v)
and K s f −→+ Pure.return (v, s0 ).
(3) K s is Pure and ∃v. {[K s]} f = K s f = Pure.return v.
(4) K s is Tot and ∃v. {[K s]} f = K s f = v.

ST-beta
ST-bind
ST-get
ST-put

6.

We have already discussed many elements of related work throughout the paper. Here we focus on a few themes not covered fully
elsewhere.
Our work builds on the many uses of monads for programming
language semantics found in the literature. Moggi (1989) was the
first to use monads to give semantics to call-by-value reduction—our
Theorem 10 makes use of the monadic structure of EMF? to show
that it can safely be executed in a strict semantics with primitive state.
Moggi (1989), Wadler (1990, 1992), Filinski (1994, 1999, 2010),
Benton et al. (2002) and others, use monads to introduce effects into
a functional language—our approach of adding user-defined effects
to the pure EMF? calculus follows this well-trodden path. Moggi
(1989), Flanagan et al. (1993), Wadler (1994) and others, have used
monads to provide a foundation on which to understand program
transformations, notably CPS—we show that weakest precondition
semantics can be formally related to CPS via our main logical
relation theorem (Theorem 6).

EMF?

ST

EMF?

We relate
to EMF?ST by defining a (partial) translation from the
former to the latter, and show that one or more steps of reduction
in EMF?ST are matched by one or more steps in EMF? . This result
guarantees that it is sound to verify a program in EMF? and execute
it in EMF?ST : the verification holds for all EMF? reduction sequences,
and EMF?ST evaluation corresponds to one such reduction.
The main intuition behind our proof is that the reduction of
reflect-free EMF? programs maintains terms in a very specific
structure—a stateful redex (an ST computation wrapped in reify)
reduces in a context structured like a telescope of binds, with the
7 F?

also compiles exceptions natively to OCaml, however we focus only on
state here, leaving a formalization of primitive exceptions to the future—we
expect it to be similar to the development here.

Draft

Related Work

13

2016/11/9

Representing monads Our work also draws a lot from Filinski’s
(1994) monadic reflection methodology, for representing and controlling the abstraction of monads. In particular, our DM monad
definition language is essentially the language of (Filinski 1994)
with some restrictions on the allowed types. Beyond controlling abstraction, Filinski shows how monadic reflection enables a universal
implementation of monads using composable continuations and a
single mutable cell. We do not (yet) make use of that aspect of his
work, partly because deploying this technique in practice is challenging, since it requires compiling programs to a runtime system
that provides composable continuations. Filinski’s (1999) work on
representing layered monads generalizes his technique to the setting
of multiple monads. We also support multiple monads, but instead
of layering monads, we define each monad purely, and relate them
via morphisms. This style is better suited to our purpose, since one
of our primary uses of reification is purification, i.e., revealing the
pure representation of an effectful term for reasoning purposes. With
layering, multiple steps of reification may be necessary, which may
be inconvenient for purification. Finally, Filinski (2010) gives an
operational semantics that is extensible with monadic actions, taking
the view of effects as being primitive, rather than encoded purely.
We take a related, but slightly different view: although effects are
encoded purely in EMF? , we see it as language in which to analyze
and describe the semantics of a primitively effectful object language,
EMF ?ST , relating the two via a simulation.

Continuations and predicate transformers We are not the first to
study the connection between continuations and predicate transformers. For example, Jensen (1978) and Audebaud and Zucca (1999)
both derive WPs from a continuation semantics of first-order imperative programs. While they only consider several primitive effects,
we allow arbitrary monadic definitions of effects. Also while their
work is limited to the first-order case, we formalize the connection between WPs and CPS also for higher-order. The connection
between WPs and the continuation monad also appears in Keimel
(2015); Keimel and Plotkin (2016).

7.

Dependent types and effects Nanevski et al. developed Hoare
type theory (HTT) (Nanevski et al. 2008) and Ynot (Chlipala
et al. 2009) as a way of extending Coq with effects. The strategy
there is to provide an axiomatic extension of Coq with a single
catch-all monad in which to encapsulate imperative code. Being
axiomatic, their approach lacks the ability to reason extrinsically
about effectful terms by computation. However, their approach
accommodates effects like non-termination, which EMF? currently
lacks. Interestingly, the internal semantics of HTT is given using
predicate transformers, similar in spirit to EMF? ’s WP semantics. It
would be interesting to explore whether or not our free proofs of
monotonicity and conjunctivity simplify the proof burden on HTT’s
semantics.
Zombie (Casinghino et al. 2014) is a dependently typed language
with general recursion, which supports reasoning extrinsically about
potentially divergent code—this approach may be fruitful to apply
to EMF? to extend its extrinsic reasoning to divergent code.
Another point in the spectrum between extrinsic and intrinsic
reasoning is Charguéraud’s (2011) characteristic formulae, which
provide a precise formula in higher-order logic capturing the semantics of a term, similar in spirit to our WPs. However, as opposed
to WPs, characteristic formulae are used interactively to prove program properties after definition, although not via computation, but
via logical reasoning. Interestingly enough, characteristic formulae
are structured in a way that almost gives the illusion that they are
the terms themselves. CFML is tool in Coq based on these ideas,
providing special tactics to manipulate formulas structured this way.
Brady (2013, 2014) encodes algebraic effects with pre- and
postconditions in Idris in the style of Atkey’s (2009) parameterized
monads. Rather than speaking about the computations themselves,
the pre- and postconditions refer to some implicit state of the world,
e.g., whether or not a file is closed. In contrast, F? ’s WPs give a
full logical characterization of a computation. Additionally, the WP
style is better suited to computing verification conditions, instead of
explicitly chaining indices in the parameterized monad.
It would be interesting, and possibly clarifying, to link up with
recent work on the denotational semantics of effectful languages
with dependent types (Ahman et al. 2016); in our case one would
investigate the semantics of EMF? and EMF?ST , which has state, but
extended with recursion (and so with nontermination).

Draft

Looking Back, Looking Ahead

While our work has yielded the pleasant combination of both a
significant simplification and boost in expressiveness for F? , we
believe it can also provide a useful foundation on which to add
user-defined effects to other dependently typed languages. All that
is required is the Pure monad upon which everything else can be
built, mostly for free.
On the practical side, going forward, we hope to make use of the
new extrinsic proving capabilities in F? to simplify specifications
and proofs in several ongoing program verification efforts that
use F? . We are particularly interested in furthering the relational
verification style, sketched in §2.8. We also hope to scale EMF? to
be a definitive semantics of all of F? —the main missing ingredients
are recursion and its semantic termination check, inductive types,
universe polymorphism, and the extensional treatment of equality.
Beyond the features currently supported by F? , we would like to
investigate adding indexed effects and effect polymorphism.
We would also like to generalize the current work to divergent
computations. For this we do not plan any changes to DM. However,
we plan to extend EMF? with general recursion and a primitive Div
effect (for divergence), following the current F? implementation
(Swamy et al. 2016). Each monad in DM will be elaborated in two
ways: first, to Pure for total correctness, as in the current paper; and
second, to Div, for partial correctness. The reify operator for a partial
correctness effect will produce a Div computation, not a Pure one.
With the addition of Div, the dynamic semantics of EMF? will force
a strict evaluation order for Div computations, rather than the nondeterministic strong reduction that we allow for Pure computations.
Along another axis, we have already mentioned our plans to
investigate translations of effect handlers (§2.5). We also hope to
enhance DM in other ways, e.g., relaxing the stratification of types
and adding inductive types. The latter would allow us to define
monads for some forms of nondeterminism and probabilities, as
well as many forms of I/O, provided we can overcome the known
difficulties with CPS’ing inductive types (Barthe and Uustalu 2002).
Enriching DM further, one could also add dependent types, reducing
the gap between it and F? , and bringing within reach examples
like Ahman and Uustalu’s (2013) dependently typed update monads.
Acknowledgments We are grateful to Clément Pit-Claudel for all
his help with the F? interactive mode; to Pierre-Evariste Dagand and
Michael Hicks for interesting discussions; and to the anonymous
reviewers for their helpful feedback.

14

2016/11/9

A.

Appendix

Lemma 12 (Well-typing of ?-translation — elaboration contexts).
For any Γ, e, A and C we have:

In this appendix we provide proofs and auxiliary results for the
theorems that appear in the body of the paper. We also show the full
type system for the source language.
A.1

∆ | Γ ` e : H !n
∆ | Γ ` e : A!τ

A.4

Theorem 13. For any A, ∆ | Γ ` e : A ! n =⇒ e = e? sΓ . (That is,
syntactic equality).
Proof. By induction on the typing derivation. The cases for (STR ET ) and (ST-B IND ) do not apply.
(1) (ST-VAR )
Our goal is to show x = x sΓ . Since the type of x is A the
substitution does not affect x, thus they’re trivially both x.
(2) (ST-C ONST )
Say ∆ | Γ ` κ(b1 , . . . , bn ) : b ! n. By the induction hypothesis we
know that bi = b?i sΓ for each i. We thus trivially get our goal by
substitution of the arguments.
(3) (ST-A BS )
n
Say we concluded ∆ | Γ ` λ x : A. e : A →
− A0 ! n. Our premise is
(note the substitution from the IH does not affect x, as it has an
A-type) the fact that e = e? sΓ . We need to show that:
λ x : A. e = (λ x : A. e)?

Γ = x1 : H1 , . . . , xn : H1
Γ? = x1 : H1? , . . . , xn : H1?

which is just
λ x : A. e = λ x : A? . e?
which is trivial from our hypothesis and since A =def A? .
(4) (ST-A PP )
Say we concluded ∆ | Γ ` f e : A0 ! n by the premises

One can then prove the following:
Lemma 11 (Well-typing of ?-translation). For any Γ, e, A and H:
=⇒ ∆? , Γ? ` e? : H ?
=⇒ ∆? , Γ? ` e? : (A? → Type0 ) → Type0

n

∆|Γ` f :A→
− A0 ! n

f e = f e = ( f ? sΓ ) (e? sΓ ) = ( f e)? sΓ

In this lemma statement, and in those that follow, when writing
e? we refer to the translation of e using the typing derivation from
the premise.

As required.
(5) (ST-F ST ), (ST-S ND ), (ST-PAIR ), (ST-I NL ), (ST-I NR )
All of these are trivial by applying the IH. For (ST-PAIR ) one
needs to note that the restrictions will ensure that the type of the
pair will be an A-type.
(6) (ST-C ASE )
Say we concluded ∆ | Γ ` case e inl x : A0 . e1 ; inr y : A1 . e2 :
A2 ! n. As inductive hypothesis we have:

Elaboration

The definitions of A and the F relation were previously given.
For elaboration, we also translate environments, in the following
manner:
∆ = X1 , . . . , Xm
∆ = X1 : Type0 , . . . , Xm : Type0

x:A=x:A

x : C = xw : C? , x : FC xw

e = e? sΓ

e1 = e?1 sΓ

e2 = e?2 sΓ

(e1 and e2 are typed in Γ extended with x and y respectively,
however since they are A-typed the sΓ substitution is the same)
The goal is:

Γ = x1 : H1 , . . . , xn : Hn
Γ = x1 : H1 , . . . , xn : Hn

=

Note that for any computational variable in the context, we introduce
two variables: one for its WP and one for its actual expression. The
xw variable, which is assumed to be fresh, is used only at the WP
level. Also note that ∆ = ∆? .
For any Γ, we define the substitution sΓ as [xiw1 /xi1 , . . . , xiwk /xik ],
for the computational variables xi1 , . . . , xik ∈ Γ.
Similarly to Lemma 11 we show that:

Draft

∆ | Γ ` e : A!n

(it cannot be the case that e has some C type, because of the type
restrictions). Using the inductive hypotheses we have:

Proof. By induction on the typing derivation.

A.3

Proof of the Logical Relation Lemma

We shall prove some intermediate lemmas before.

The full ?-translation for DM expressions is given in Figure 7. The
one for types was previously defined. We define translation on
environments in the following way:

∆ | Γ ` e : H !n
∆ | Γ ` e : A!τ

∆ | Γ ` e : A!τ
∆, Γ ` e : Pure A (e? sΓ )

∆ | Γ ` e : C!n
∆, Γ ` e : FC e? sΓ

∆ | Γ ` e : A!n
∆, Γ ` e : A

CPS Translation (WP Generation)

∆ = X1 , . . . , Xm
∆? = X1 : Type0 , . . . , Xm : Type0

∆, Γ ` e? sΓ : H ?
∆, Γ ` e? sΓ : (A? → Type0 ) → Type0

For expression elaboration we aim to show that:

The Definitional Language DM

In the typing judgment, the metavariable ∆ represents a set of type
variables that remains fixed throughout typing. It is used to introduce
top-level let-polymorphism on all CPS’d/elaborated terms. A type
is well-formed in the context ∆ if all of its variables are in ∆. In
rigor, all judgments from here onwards are subject to that constraint,
which we do not write down. A context Γ is well-formed if both
(1) all of its types are well-formed according to ∆ (2) no variable
names are repeated. This last condition simplifies reasoning about
substitution and does not limit the language in any way.
We assume that every base type in DM is also a base type in
EMF? (or that there exists a mapping from them, formally), and that
source constants are also present and with the same type (formally,
also a mapping for constants that respects the previous one).
The typing judgment for DM is given in Figure 6. We assume
that the types appearing in the rules are well-formed. For example,
in the (ST-PAIR ) rule, either both H and H 0 are in A or both are in
C etc.
A.2

=⇒
=⇒

(case(e) x.e1 y.e2 )
(case(e? sΓ ) x.e?1 sΓ y.e?2 sΓ )

We trivially get our goal from the IHs.

Theorem 14. If ∆ | Γ ` e : A ! n, then ∆, Γ ` e : A.
Proof. By induction on the typing derivation.

15

2016/11/9

ST-VAR

ST-C ONST

ST-A BS

x:H ∈Γ
∆ | Γ ` x : H !n

∆ | Γ ` ei : bi ! n
κ : b1 , . . . , bn → b
∆ | Γ ` κ(e1 , . . . , en ) : b ! n

∆ | Γ ` λ x : H. e : H −
→ H0 ! n

ST-A PP

∆ | Γ, x : H ` e : H 0 ! ε
ε

ST-PAIR

∆|Γ`e:H −
→ H0 ! n
∆ | Γ ` e0 : H ! n
∆ | Γ ` ee0 : H 0 ! ε

ST-F ST

∆ | Γ ` e : H !n
∆ | Γ ` e0 : H 0 ! n
∆ | Γ ` (e, e0 ) : H × H 0 ! n

ε

∆ | Γ ` e : H × H0 ! n
∆ | Γ ` fst(e) : H ! n

ST-C ASE

ST-I NL

∆ | Γ ` e : A!n
∆ | Γ ` inl(e) : A + A0 ! n

∆ | Γ ` e : A + A0 ! n
∆ | Γ, x : A ` e1 : H ! ε
∆ | Γ, x : A0 ` e2 : H ! ε
0
∆ | Γ ` case e inl x : A. e1 ; inr y : A . e2 : H ! ε
ST-B IND

ST-R ET

∆ | Γ ` e : A!τ
∆ | Γ, x : A ` e : A0 ! τ
∆ | Γ ` bindτ e to x : A in e0 : A0 ! τ

∆ | Γ ` e : A!n
∆ | Γ ` returnτ e : A ! τ

Figure 6. Typing rules of DM
x?
( f e)?
fst(e)?
inl(e)?
(e1 , e2 )?

=
=
=
=
=

x
f ? e?
fst e?
inl e?
(e?1 , e?2 )

K(e1 , . . . , en )?
(λ x : H. e)?
snd(e)?
inr(e)?
(case e0 inl x : A. e1 ; inr y : A0 . e2 )?

(returnτ e)?
(bindτ e1 to x in e2 )?

=
=

λ p : A? → Type0 . p e?
λ p : A0? → Type0 . e?1 (λ x : A. e?2 p)

=
=
=
=
=

K e?1 . . . e?n
λ x : H ? . e?
snd e?
inr e?
case(e?0 ) x.e?1 y.e?2

(when ∆ | Γ ` e : A!n)
(when ∆ | Γ, x : A ` e2 : A0 !τ)

Figure 7. Definition of the ?-translation for DM terms
Lemma 15 (Invariancy of FC w). If Γ  w1 = w2 , then Γ ` FC w1 <:
FC w2 .

(1) (ST-VAR )
We have ∆ | Γ ` x : A ! n, with x ∈ Γ. By the translation for
environments, we have x : A in Γ, so this is trivial.
(2) (ST-C ONST )
For any constant κ : (b1 , . . . , bn ) → b say we have ∆ | Γ `
κ(e1 , . . . , en ) : b ! n by (ST-C ONST ) (note that b and all the bi
are in A). This means that for every i we have as inductive
hypothesis:

Proof. By induction on C.
τ

(1) C −
→A
We need to show that
Γ`F

w1 <: F

τ

C−
→A

w2

Which is

Since κ is also a target constant of the same type, we thus have:

Γ ` xw : C? → FC xw → Pure A (w1 xw )
<: xw : C? → FC xw → Pure A (w2 xw )

∆, Γ ` κ e1 . . . en : b
Which is exactly our goal as b = b.
(3) (ST-F ST ), (ST-S ND ), (ST-PAIR ), (ST-I NL ), (ST-I NR )
Trivial by using IH.
(4) (ST-C ASE )
Say we concluded ∆ | Γ ` case e inl x : A0 . e1 ; inr y : A1 . e2 :
A2 ! n by (ST-C ASE ). Our IHs give us

After two applications of (ST-P ROD ) (and some trivial reflexivity discharges), the required premise to show is:
Γ, xw : C? , : FC xw ` Pure A (w1 xw ) <: Pure A (w2 xw )
By (S-P URE ) we’re required to show that A is a subtype of itself
(which is trivial by reflexivity of subtyping (S-C ONV )) and that
w2 is stronger than w1 , which can be easily proven as they are
equal.
τ
(2) A −
→A
Very similar to the previous case, but simpler.
n
(3) C →
− C0
We need to show that

∆, Γ
` e : A0 + A1
∆, Γ, x : A0 ` e1 : A2
∆, Γ, y : A1 ` e2 : A2
By a non-dependent application of T-CaseTot we get
∆, Γ ` case(e) x.e1 y.e2 : A2

n
n
Γ ` FC→
− C0 w1 <: FC→
− C0 w2

Which is our goal.
(5) (ST-A BS ), (ST-A PP )
Both trivial from IHs.

Which is
Γ ` xw : C? → FC xw → FC0 w1 xw
<: xw : C? → FC xw → FC0 w2 xw
After two applications of (ST-P ROD ) (and some trivial reflexivity discharges), the required premise to show is:

Before jumping into the logical relation lemma, we will require
the following auxiliary lemma, of which we make heavy use.

Draft

τ

C−
→A

∆, Γ ` ei : bi

Γ, xw : C? , : FC xw ` FC0 w1 xw <: FC0 w2 xw
16

2016/11/9

As in this context we can show w1 xw = w2 xw we apply our IH
to the type C0 and are done.
n
(4) A →
− C0
Also very similar to the previous case, but simpler.
(5) C ×C0
Trivial by IHs and concluding that fst w1 = fst w2 , and similarly
for snd.

Using T-Abs twice we can conclude this via
∆, Γ, xw : C? , x : FC xw ` e : GεH ((λ x : C? .e? ) sΓ xw )
Since the substitution does not cover x, the argument to F
reduces to e? sΓ [xw /x], thus we use our IH to conclude this
easily.
(5) (ST-A PP )
Again, There are two possible cases:
ε
• A−
→H
We concluded ∆ | Γ ` f e : G ! ε. Our premises are ∆ | Γ ` f :
ε
A−
→ C ! n and ∆ | Γ ` e : A ! n. The IH for f is, expanding F:

Proof of Theorem 6 (Logical relations lemma)

∆, Γ ` f : x : A → GεH (( f ? sΓ ) x)

Proof. The two parts are proved by a joint structural induction.

By T-App, and since e : A, this is just:

(1) (ST-VAR )
We have ∆ | Γ ` x : C ! n, with x ∈ Γ. By the translation for
environments, we have xw : C? and x : FC xw in Γ. Since x is
covered by the substitution sΓ , what we need to prove is ∆, Γ `
x : FC xw , which is exactly what we have in the environment.
(2) (ST-PAIR )
Suppose we proved (e1 , e2 ) : C1 × C2 ! n by (ST-PAIR ). We
want to show: ∆, Γ ` (e1 , e2 ) : FC1 ×C2 (e?1 , e?2 ) sΓ , i.e., that (after
reduction inside F):
∆, Γ ` (e1 , e2 ) : FC1 e?1 sΓ × FC2

∆, Γ ` f e : GεH (( f ? sΓ ) e)
Since from a previous theorem we know we have e = e? sΓ
(syntactically), we can conclude:
∆, Γ ` f e : GεH (( f ? sΓ ) (e? sΓ ))
This is exactly:
∆, Γ ` f e : GεH (( f e)? sΓ )

e?2 sΓ

which is our goal, in either the C ! n or the A ! τ case.
ε

• C−
→H

This is trivial by applying both IHs.
(3) (ST-F ST ), (ST-S ND )
Suppose we proved ∆ | Γ ` fst(e) : C1 ! n by (ST-F ST ). We need
to then show
∆, Γ ` fst e : FC1 fst e? sΓ
By our induction hypothesis we have ∆, Γ ` e : FC1 ×C2 e? sΓ ,
which is

We concluded ∆ | Γ ` f e : H ! ε. Our premises are ∆ | Γ ` f :
ε
C−
→ H ! n and ∆ | Γ ` e : C ! n The IHs are, expanding F:

∆, Γ ` f (e? sΓ ) e : GCε 0 (( f ? sΓ ) (e? sΓ ))

It is therefore easy to see that we have our goal.
(4) (ST-A BS )
There are two cases:
ε
• A−
→H
ε
Suppose we concluded ∆ | Γ ` λ x : A. e : A −
→ H ! n. Then we
have ∆ | Γ, x : A ` e : H ! ε and so, by the induction hypothesis,
in both cases for ε we have

This is just, syntactically:
∆, Γ ` f e : GCε 0 (( f ? sΓ ) (e? sΓ ))
which is our goal, in either the C ! n or the A ! τ case.
(6) (ST-C ASE )
There are two cases depending on wether we eliminate into C ! n
or A ! τ. Both of these cases are quite dull, and deal mostly with
the typing judgment on the target. This may be skipped without
hindering any of the main ideas.
• C!n
Suppose that ∆ | Γ ` e : A + A0 ! n, ∆ | Γ, x : A ` e1 : C ! n,
and ∆ | Γ, y : A0 ` e2 : C ! n, so that ∆ | Γ ` case e inl x :
A. e1 ; inr y : A0 . e2 : C ! n. We will go into detail only for e1
as the typing and reasoning for e2 is exactly analogous. As
inductive hypothesis for e1 we have

∆, Γ, x : A ` e : GεH (e? sΓ )
And we have to show:
? ?
n
∆, Γ ` λ x : A. e : FA→
− H (λ x : A .e ) sΓ

Which is
∆, Γ ` λ x : A. e : x : A → GεH ((λ x : A? .e? ) sΓ x)
Since the substitution does not cover x, the argument to G is
just e? sΓ , thus we use our IH to conclude this easily.
ε
• C−
→H
ε
Suppose we concluded ∆ | Γ ` λ x : C. e : C −
→ H ! n. Then we
have ∆ | Γ, x : C ` e : H ! ε and so, by the induction hypothesis
we have, in either case for ε:

∆, Γ, x : A ` e1 : FC e?1 sΓ
We wish to show:
∆, Γ ` caseFC

∆, Γ ` caseFC

∆, Γ ` λ x : C . λ x : FC x . e : F

ε

C−
→H

? ?

(λ x : C .e ) sΓ

case(z) x.e?1 sΓ y.e?2 sΓ (e

as z) x : A. e1 y : A0 . e2

: FC case(e? sΓ ) x.e?1 sΓ y.e?2 sΓ

Which is

Since e = e? sΓ we will prove this has type

∆, Γ ` λ xw : C? . λ x : FC xw . e
: xw : C? → FC xw → GεH ((λ x : C? .e? ) sΓ xw )
Draft

as z) x.e1 y.e2

Which is

And we have to show:
w

case(z) e?1 sΓ e?2 sΓ (e

: FC (case(e? ) x.e?1 y.e?2 ) sΓ

∆, Γ, xw : C? , x : FC xw ` e : GεH (e? sΓ [xw /x])
?

f : xw : C? → FC xw → GεH (( f ? sΓ ) xw )
e : FC e? sΓ

Thus by two uses of T-App (noting that it’s well typed by
our IH for e), we can conclude:

∆, Γ ` e : FC1 fst e? sΓ × FC2 snd e? sΓ

w

`
`

∆, Γ
∆, Γ

FC case(e) x.e?1 sΓ y.e?2 sΓ
17

2016/11/9

By T-CaseTot, we should show:

First we define equality for the source language. It is basically
standard β η-equivalence adding the monad laws for the base monad
T . We keep the type and effect of each equality. It is an invariant
that if we can derive an equality, both sides are well-typed at the
specified type and effect.
The definition of the equality judgment is in Figure 8. Besides
those rules, there is a congruence rule for every source construct, as
expected.
We then prove that:

e : A + A0

∆, Γ
`
∆, Γ, x : A ` e1 : FC case(inl x) x.e?1 sΓ y.e?2 sΓ

(And the one for e2 ). We get the first one trivially by theorem
14. The second is by reduction equivalent to:
∆, Γ, x : A ` e1 : FC e?1 sΓ
Which is exactly our IH for e1 , so we’re done.
• A!τ

∆ | Γ ` e1 = e2 : H ! ε
∆, Γ  e?1 sΓ == e?2 sΓ

Our hypotheses are:
∆, Γ
` e : A0 + A1
∆, Γ, x : A0 ` e1 : Pure A2 (e?1 sΓ )
∆, Γ, y : A1 ` e2 : Pure A2 (e?2 sΓ )

Where by  it is meant the validity judgment of EMF? .
Theorem 16 (Preservation of equality by CPS). If ∆ | Γ ` e1 = e2 :
H ! ε for any ∆, Γ, e1 , e2 , H, ε, then one has ∆, Γ  e?1 sΓ == e?2 sΓ .

Applying T-Case (non-dependently) we get.
∆, Γ ` case(e) x.e1 y.e2 :
Pure A2 (case(e) x.e?1 sΓ y.e?2 sΓ )

Proof. By induction on the equality derivation. Most of the cases are
trivial, since EMF? has very similar rules for equality. The interesting
cases are the monadic equalities, which we show here:

Since we know e = e? sΓ and since A =def A? this is exactly:
∆, Γ ` case(e) x.e1 y.e2 :
Pure A2 ((case(e? ) x.e?1 y.e?2 ) sΓ )

Which is our goal.
(7) (ST-R ET )
We have ∆ | Γ ` e : A ! n. We need to show:

(1) (E Q -M1)
We concluded
∆ | Γ ` bindτ m to x in (returnτ x) = m : A ! τ

∆, Γ ` returnτ e : Pure A (returnτ e? sΓ )

Thus we need to show that

i.e.

∆, Γ  (bindτ m to x in (returnτ x))? sΓ == m? sΓ

∆, Γ ` Pure.return A e : Pure A (λ p : A? → Type0 . (e? sΓ ))

That is:

This is a trivial consequence of Theorem 13 by using the T-Ret
rule of EMF? , and the fact that A =def A? .
(8) (ST-B IND )
Suppose we have ∆ | Γ ` e1 : A ! τ, and ∆ | Γ, x : A ` e2 : A0 ! τ,
and so ∆ | Γ ` bindτ e1 to x : A in e2 : A0 ! τ. We have to show:

∆, Γ  (λ p. (m? sΓ )(λ x. (λ p0 . p0 x) p)) == m? sΓ
This is trivially provable by β η-reduction.
(2) (E Q -M2)
We concluded

∆, Γ ` bindτ e1 to x : A in e2 : Pure A0 ((bindτ e1 to x : A in e2 )? sΓ )
that is:

thus we need to show that

∆, Γ ` Pure.bind A A0 (e?1 sΓ ) e1 (λ x : A? . e?2 sΓ ) (λ x : A. e2 ) :
Pure A0 (λ p : A0? → Ty. e?1 (λ x : A? . e?2 p))

∆, Γ  (bindτ (returnτ e) to x in f x)? sΓ == ( f e)? sΓ

By our IHs we have:

That is:

` e1 : Pure A (e?1 sΓ )
∆, Γ
∆, Γ, x : A ` e2 : Pure A0 (e?2 sΓ )

∆, Γ  (λ p. (λ p0 . p0 e? ) (λ x. f ? x p)) sΓ = ( f ? sΓ )(e? sΓ )
Note that since x ∈
/ FV ( f ) =⇒ x ∈
/ FV ( f ? sΓ ), this is easily
shown by β η-reduction as well.
(3) (E Q -M3)
We concluded

So we get:
∆, Γ ` λ x : A. e2 : x : A → Pure A0 (e?2 sΓ )
By the T-Bind rule we can conclude:

∆ | Γ ` bindτ (bindτ m to x in e1 ) to y in e2
= bindτ m to x in (bindτ e1 to y in e2 ) : A00 ! τ

∆, Γ ` Pure.bind A A0 (e?1 sΓ ) e1 (λ x : A? . e?2 sΓ ) (λ x : A. e2 ) :
Pure A0 (λ p : A0 → Ty. e?1 (λ x : A. e?2 p))

thus we need to show that

Since A = A? and A0 = A0? this is exactly our goal.

∆, Γ  (bindτ (bindτ m to x in e1 ) to y in e2 )? sΓ
== (bindτ m to x in (bindτ e1 to y in e2 ))? sΓ

That is:

Note: in this proof, we didn’t use any specific fact about Pure,
except the relation between monad operations and their WPs, so this
is all generalizable to another target monad that’s already defined
and satisfies the base conditions for return and bind.
A.5

∆, Γ  (λ p. (λ p0 . (m? sΓ ) (λ x. (e?1 sΓ )p0 )) (λ y. (e?2 sΓ ) p))
== (λ p. (m? sΓ ) (λ x. (λ p0 . (e?1 sΓ ) (λ y. (e?2 sΓ ) p0 )) p))

Note that since x ∈
/ FV (e2 ) =⇒ x ∈
/ FV (e?2 ), this is also easily
shown by β η-reduction.

Equality Preservation

We want to show that any source monad will give rise to specificationlevel monads in the target. This will be a consequence on the fact
that equality is preserved by the ?-translation. From equality preservation we also get the property that lifts are monad morphisms
without further effort.

Draft

∆ | Γ ` bindτ (returnτ e) to x in f x = f e : A0 ! τ

The proof above is easy, and that should not be surprising, as
we are translating our abstract monadic operations into a concrete
monad (continuations), thus our source equalities should be trivially
satisfied after translation.

18

2016/11/9

E Q -E TA

E Q -B ETA

∆|Γ`e:H −
→ H0 ! n
ε

∆ | Γ, x : H ` e1 : H 0 ! ε
∆ | Γ ` e2 : H ! n
∆ | Γ ` (λ x : H. e1 )e2 = e1 [e2 /x] : H 0 ! ε

x∈
/ FV (e)

∆ | Γ ` (λ x : H. e x) = e : H −
→ H0 ! n
ε

E Q -A PP

E Q -A BS

∆ | Γ ` e1 = e01 : H −
→ H0 ! n
∆ | Γ ` e2 = e02 : H ! n
∆ | Γ ` e1 e2 = e01 e02 : H 0 ! ε
ε

∆ | Γ, x : H ` e = e0 : H 0 ! ε

∆ | Γ ` (λ x : H. e) = (λ x : H. e0 ) : H −
→ H0 ! n
ε

E Q -R EFL

E Q -S YMM

E Q -T RANS

∆ | Γ ` e : H !ε
∆ | Γ ` e = e : H !ε

∆ | Γ ` e1 = e2 : H ! ε
∆ | Γ ` e2 = e1 : H ! ε

∆ | Γ ` e1 = e2 : H ! ε
∆ | Γ ` e2 = e3 : H ! ε
∆ | Γ ` e1 = e3 : H ! ε

E Q -PAIR

∆ | Γ ` e : H × H0 ! n
∆ | Γ ` (fst(e), snd(e)) = e : H × H 0 ! n

E Q -C ASE

∆ | Γ ` e : A + A0 ! n
∆ | Γ ` case e inl x.inl(x); inr x.inr(x) = e : A + A0 ! n
E Q -M2

E Q -M1

∆ | Γ ` m : A!τ
∆ | Γ ` bindτ m to x in (returnτ x) = m : A ! τ

∆ | Γ ` e : A!n
∆|Γ` f :A−
→ A0 ! n
x∈
/ FV ( f )
∆ | Γ ` bindτ (returnτ e) to x in f x = f e : A0 ! τ
τ

E Q -M3

∆ | Γ ` m : A!τ
∆ | Γ, x : A ` e1 : A0 ! τ
∆ | Γ, y : A0 ` e2 : A00 ! τ
x∈
/ FV (e2 )
∆ | Γ ` bindτ (bindτ m to x in e1 ) to y in e2 = bindτ m to x in (bindτ e1 to y in e2 ) : A00 ! τ
Figure 8. Equality rules for DM

A.6

Monotonicity

By our IH we get:
Γ12  ∀x1 , x2 .[x1 . x1 ∧ x1 . x2 ∧ x2 . x2 ] =⇒ φ [2 → 1]

We’re interested in the monotonicity of WPs. Firstly, we need a
higher-order definition for this property. Throughout this section we
mostly ignore DM’s typing restrictions and work with a larger source
language. This gives us a stronger result than strictly necessary.
The types where the translation is defined are those nondependent and monad-free (meaning every arrow in them is a
Tot-arrow). No ocurrence of Pure is allowed. The types of specifications are always of this shape, so this is not a limitation.
For non-empty environments the theorem states:

By weakening (note that x1 and x2 are not free in the RHS) we get
that:
(Γ, x : t)12  ∀x1 , x2 .[x1 . x1 ∧ x1 . x2 ∧ x2 . x2 ] =⇒ φ [2 → 1]
We can instantiate this (via (V-∀E )) with x1 on both variables to get:
(Γ, x : t)12  [x1 . x1 ∧ x1 . x1 ∧ x1 . x1 ] =⇒ φ [2 → 1][x1 /x2 ]
Furthermore, it is trivial to show this antecedent in the context
(Γ, x : t)12 and so we get our goal of:

Theorem 17 (Monotonicity of ?-translation— environments). For
any ∆, Γ, e, H, A one has:
1.
2.

∆ | Γ ` e : H !n
∆ | Γ ` e : A!τ

=⇒
=⇒

(Γ, x : t)12  φ [2 → 1][x1 /x2 ]

∆, Γ12  e?1 .H ? e?2
∆, Γ12  e?1 .(A? →Type0 )→Type0 e?2

Where we define
·12 = ·
(Γ, x : t)12 = Γ12 , x1 : t ? , x12 : t ? , [x1 .t ? x1 ∧ x1 .t ? x2 ∧ x2 .t ? x2 ]

Lemma 19. For any e, if Γ12  e? 1 . e? 2 , then Γ12  e? 1 .
e? 1 ∧ e? 1 . e? 2 ∧ e? 2 . e? 2 .

which essentially duplicates each variable and asserts both monotonicity for each of them and their ordering ([φ ] is notation for h : φ ,
where h does not appear free anywhere). We then define the −1
substitution as [x11 /x1 , . . . , xn1 /xn ] and similarly for −2 . This trivially
implies the previous monotonicity theorem.
Before jumping into the proof, we define and prove the following
lemma:

Proof. Trivial from previous lemma by noting that e? 1 [1 → 2] = e? 2
and likewise for [2 → 1], and then using (V-A ND I NTRO ).
Proof of Theorem 17 (Monotonicity of ?-translation— environments)
Proof. We prove these two propositions by induction on the typing
derivation for e. Throughout the proof ∆ plays no special role, so
we just drop it from the reasoning, keeping in mind that it has to be
there for having well-formed types (but nothing else).
Note that during the proof we treat .X abstractly, so any
instantiation with a proper type (not necessarily those where .
reduces to equality) would be OK.
Throughout this proof we sometimes skip the subindices for .
in favor of compactness. Hopefully, they should be clear from the
context.

Lemma 18. For any φ , Γ12  φ implies Γ12  φ [2 → 1]. Where
[2 → 1] is the substitution mapping x2 to x1 for every x in Γ.
Analogously Γ12  φ [1 → 2].
Proof. By induction on Γ. This is trivial for an empty gamma. For
Γ0 = Γ, x : t, assume (Γ, x : t)12  φ holds. By applying (V-∀I ) three
times, we get:
Γ12  ∀x1 , x2 .[x1 . x1 ∧ x1 . x2 ∧ x2 . x2 ] =⇒ φ
Draft

19

2016/11/9

(1) (ST-VAR )
We need to show Γ12  xi1 .ti? xi2 . This is trivial from the context
and by using the (V-A SSUME ) and (V-A ND E LIMi) rules.
(2) (ST-C ONST )
The constants only deal with base types, so all inductive hypotheses for the arguments reduce to an equality, as does our goal. Our
goal is is then trivially provable by applications of (V-E Q P).
(3) (ST-A BS )
Say we concluded Γ, x : t ` e : s ! ε As IH we have:

(6) (ST-B IND )
Say Γ ` m : a ! τ and Γ, x : a ` e : b ! τ, so we get Γ ` bindτ m to x in e :
b ! τ. Our IHs are:
Γ12  m?1 .(a→Type0 )→Type0 m?2
(Γ, x : a)12  e?1 [x1 /x] .(b→Type0 )→Type0 e?2 [x2 /x]

We need to show that:
Γ12  (λ p. m? 1 (λ x. e? 1 p)) .(b? →Type0 )→Type0 (λ p. m? 2 (λ x. e? 2 p))
Which by expanding the definition, applying (V-∀I ), and reducing can be simplified to:

(Γ, x : t)12  e? 1 [x1 /x] .s0 e? 2 [x2 /x]
Where s0 is either s? or (s? → Type0 ) → Type0 depending on ε.
The proof is independent of this. What we need to prove is:

Γ12 , p1 , p2 , [p1 . p1 ∧ p1 . p2 ∧ p2 . p2 ] 
m? 1 (λ x. e? 1 p1 ) . m? 2 (λ x. e? 2 p2 )

Γ12  (λ x : t ? .e? 1 ) .t ? →s0 (λ x : t ? .e? 2 )

By our IH we know that m? 1 . m? 2 , so it would be enough to
show that:

Which by definition is:

Γ12 , p1 , p2 , [p1 . p1 ∧ p1 . p2 ∧ p2 . p2 ] 
(λ x. e? 1 p1 ) . (λ x. e? 2 p2 )

Γ12  ∀x1 , x2 : t ? . x1 .t ? x1 ∧ x1 .t ? x2 ∧ x2 .t ? x2 =⇒
(λ x : t ? .e? 1 ) x1 .s0 (λ x : t ? .e? 2 ) x2

and then use Lemma 19. Expanding the definitions, applying
(V-∀I ) and reducing this can be shown by:

By reduction ((V-E Q R ED ) + (V-E Q *)), this is equivalent to:
Γ12  ∀x1 , x2 : t ? . x1 .t ? x1 ∧ x1 .t ? x2 ∧ x2 .t ? x2 =⇒
e? 1 [x1 /x] .s0 e? 2 [x2 /x]

Γ12 , p1 , p2 , [p1 . p1 ∧ p1 . p2 ∧ p2 . p2 ]
x1 , x2 , [x1 . x1 ∧ x1 . x2 ∧ x2 . x2 ] 
e? 1 [x1 /x] p1 . e? 2 [x2 /x] p2

Which we can conclude from three applications of (V-∀I ), and
our IH.
(4) (ST-A PP )
ε
Say Γ ` f : t −
→ s ! n and Γ ` e : a ! n. As inductive hypothesis we
get:

Because of our assumptions for p1 and p2 , this can be shown
by proving e? 1 [x1 /x] . e? 2 [x2 /x]. This is trivial by our IH for e,
weakening it into this extended environment that includes pi .
(7) (ST-PAIR ), (ST-F ST ), (ST-I NL )
All trivial from IHs.
(8) (ST-C ASE )
By case analysis on the IH for the sum type, and reduction.

Γ12  e? 1 .t ? e? 2
Γ12  f ? 1 .t ? →s0 f ? 2
?
?
Where is either s or (s → Type0 ) → Type0 depending on ε.
Again, the proof is independent of this. Applying Lemma 19 for
our second IH we get that:
s0

Γ12  e? 1 .t ? e? 1 ∧ e? 1 .t ? e? 2 ∧ e? 2 .t ? e? 2

Having this proof implies that any well-typed term will be given a
monotonic specification. And, as a consequence, functions preserve
monotonicity.

Expanding the definition of . on the IH for f we get:
Γ12  ∀x1 , x2 : t ? . x1 .t ? x1 ∧ x1 .t ? x2 ∧ x2 .t ? x2 =⇒
f ∗1 x1 .s0 f ∗2 x2
e? 1 , e? 2 ,

(V-∀E )) x1 , x2
?1

We instantiate (using
(V-MP) with our proof about e

with
and e? 2 to get:

A.7

The definition of conjunctivity on EMF? predicate types was given
previously. The full theorem which we prove is this:

and apply

Theorem 20 (Conjunctivity of ?-translation— environments). For
any ∆, Γ, e, H, A one has:

Γ12  f ∗1 e? 1 .s0 f ∗2 e? 2
n

τ

Which is exactly our goal in any (→
− ,−
→) case.
(5) (ST-R ET )
Say Γ ` returnτ e : t ! τ. Our IH gives us:
12

Γ

?1

e

Conjunctivity

1.
2.

∆ | Γ ` e : C!n
∆ | Γ ` e : A!τ

=⇒
=⇒

∆, ΓC  CC? (e? )
∆, ΓC  C(A? →Type0 )→Type0 (e? )

Where when Γ = x1 : t1 , . . ., we define ΓC = x1 : t1? , [Ct1? (x1 )], . . ..
This trivially implies the previously stated theorem by taking Γ = ·.

?2

.t ? e

And we need to show that:
Γ12  (λ p. p e? 1 ) .(t ? →Type0 )→Type0 (λ p. p e? 2 )

Proof. By induction on the typing derivations. Once again, ∆ does
not play a big role and we omit it.

That is:
Γ12  ∀p1 , p2 . p1 . p1 ∧ p1 . p2 ∧ p2 . p2 =⇒
(λ p. p e? 1 ) p1 .s0 (λ p. p e? 2 ) p2

(1) (ST-VAR )
Trivial from context, for any type.
(2) (ST-C ONST )
Does not apply as no constant gives a type C ! n nor A ! τ
(3) (ST-A BS )
Say we concluded Γ, x : t ` e : s ! ε (where that might be C ! n or
A ! τ, we treat both cases uniformly). From the IH we get

By reduction this is:
Γ12  ∀p1 , p2 . p1 . p1 ∧ p1 . p2 ∧ p2 . p2 =⇒
p1 e? 1 .s0 p2 e? 2

ΓC , x : t ? , [Ct ? (x)]  Cs0 (e)

By applying Lemma 19 to e we get:
?1

Γ12  e

?1

.t ? e

?1

∧e

?2

.t ? e

?2

∧e

s0

Where is or (s? → Type0 ) → Type0 according to (s, ε). By
applying (V-∀I ) twice we get:

?2

.t ? e

With this, we can easily prove our goal by applying (V-∀I ), and
then the assumption of p1 . p2 applied to this last proof.
Draft

s?

ΓC  ∀x : t ? .Ct ? (x) ⇒ Cs0 (e)
20

2016/11/9

Which is the same, by reduction, as:

that proof, but it’s the wanted result as WPs (which can be taken as
arguments) might not distribute over empty universals (in particular,
non-satisfiable WPs do not).

?

ΓC  ∀x : t .Ct ? (x) ⇒ Cs0 ((λ x. e x) x)
Thus by definition of C:

References

ΓC  Ct→s0 (λ x. e x)

D. Ahman and T. Uustalu. Update monads: Cointerpreting directed containers. TYPES, 2013.

As required for both cases.
(4) (ST-A PP )
Trivial by the preservation of C by application, in both cases
(applies (V-MP)).
(5) (ST-R ET )
Say we concluded Γ ` returnτ e : A ! τ. Our goal is then:

D. Ahman, N. Ghani, and G. D. Plotkin. Dependent types and fibred
computational effects. FOSSACS, 2016.
R. Atkey. Parameterised notions of computation. Journal of Functional
Programming, 19:335–376, 2009.

ΓC  C(A? →Type0 )→Type0 (λ p. p e? )

P. Audebaud and E. Zucca. Deriving proof rules from continuation semantics.
Formal Asp. Comput., 11(4):426–447, 1999.

ΓC  ∀p1 , p2 . (λ p. p e? )p1 ∧ (λ p. p e? )p2
= (λ p. p e? )(λ x.p1 x ∧ p2 x)

G. Barthe and T. Uustalu. CPS translating inductive and coinductive types. In
P. Thiemann, editor, Proceedings of the 2002 ACM SIGPLAN Workshop
on Partial Evaluation and Semantics-Based Program Manipulation
(PEPM ’02), Portland, Oregon, USA, January 14-15, 2002. 2002.

Which is:

By reduction that’s equivalent to:

G. Barthe, C. Fournet, B. Grégoire, P.-Y. Strub, N. Swamy, and S. ZanellaBéguelin. Probabilistic relational verification for cryptographic implementations. POPL. 2014.

ΓC  ∀p1 , p2 . p1 e? ∧ p2 e? = p1 e? ∧ p2 e?
Which is trivially true (without use of any IH) by (V-R EFL ).
(6) (ST-B IND )
Say we concluded Γ ` bindτ e1 to x in e2 : A0 ! τ, where e1 : A ! τ.
Our IHs are:
ΓC  C(A? →Type0 )→Type0 (e?1 )
ΓC , x : A? , [CA? (x)]  C(A0? →Type0 )→Type0 (e?2 )

N. Benton. Simple relational correctness proofs for static analyses and
program transformations. POPL. 2004.
N. Benton and A. Kennedy. Exceptional syntax. J. Funct. Program., 11(4):
395–410, 2001.
N. Benton, J. Hughes, and E. Moggi. Monads and Effects, pages 42–122.
Springer Berlin Heidelberg, Berlin, Heidelberg, 2002.
E. Brady. Programming and reasoning with algebraic effects and dependent
types. ICFP, 2013.

We need to show:
ΓC  C(A0? →Type0 )→Type0 (λ p.e?1 (λ x.e?2 p))

E. Brady. Resource-dependent algebraic effects. TFP, 2014.

Expanding the definition, this is:

C. Casinghino, V. Sjöberg, and S. Weirich. Combining proofs and programs
in a dependently typed language. POPL, 2014.

ΓC  ∀p1 , p2 . (λ p.e?1 (λ x.e?2 p)) p1 ∧ (λ p.e?1 (λ x.e?2 p)) p2
= (λ p.e?1 (λ x.e?2 p))(λ x.p1 x ∧ p2 x)

A. Charguéraud. Characteristic formulae for the verification of imperative
programs. ICFP. 2011.

By reduction, this is equivalent to:

A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky.
Effective interactive proofs for higher-order imperative programs. ICFP,
2009.

ΓC  ∀p1 , p2 . e?1 (λ x.e?2 p1 ) ∧ e?1 (λ x.e?2 p2 )
= e?1 (λ x.e?2 (λ x.p1 x ∧ p2 x))

T. Coquand and G. Huet. The calculus of constructions. Information and
Computation, 76(2):95 – 120, 1988.

By the IH for e2 we know ∀x. e?2 (λ x.p1 x ∧ p2 x) = e?2 p1 ∧
e?2 p2 . By reduction and (V-E XT ) this means (λ x.e?2 (λ x.p1 x ∧
p2 x)) = (λ x.e?2 p1 ∧ e?2 p2 ) Thus we replace on the RHS (via
(V-S UBST )) and get:

L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. TACAS. 2008.
E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation
of programs. Commun. ACM, 18(8):453–457, 1975.

ΓC  ∀p1 , p2 . e?1 (λ x.e?2 p1 ) ∧ e?1 (λ x.e?2 p2 )
= e?1 (λ x.e?2 p1 ∧ e?2 p2 )

E. W. Dijkstra. A Discipline of Programming. Prentice Hall PTR, Upper
Saddle River, NJ, USA, 1st edition, 1997.

By some η-expansion and the IH for e1 we can turn this to:

A. Filinski. Representing monads. POPL. 1994.

ΓC  ∀p1 , p2 . e?1 (λ x.e?2 p1 ) ∧ e?1 (λ x.e?2 p2 )
= e?1 (λ x.e?2 p1 ) ∧ e?1 (λ x.e?2 p2 )

A. Filinski. Representing layered monads. POPL. 1999.
A. Filinski. Monads in action. POPL. 2010.

Which is trivially provable by (V-R EFL ).
(7) (ST-PAIR ), (ST-F ST )
All trivial by IHs.
(8) (ST-I NL )
Does not apply for the cases we consider.
(9) (ST-C ASE )
Trivial by (V-S UM I ND ) and the IHs.

J.-C. Filliâtre and A. Paskevich. Why3 — where programs meet provers.
ESOP. 2013.
C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of
compiling with continuations. PLDI, 1993.
B. Jacobs. Dijkstra and Hoare monads in monadic computation. Theor.
Comput. Sci., 604:30–45, 2015.
K. Jensen. Connection between Dijkstra’s predicate-transformers and
denotational continuation-semantics. DAIMI Report Series 7.86, 1978.
K. Keimel. Healthiness conditions for predicate transformers. Electr. Notes
Theor. Comput. Sci., 319:255–270, 2015.

Thus, any term obtained by the ?-translation (return, bind,
actions, lifts, ...) will be conjunctive in this sense, which means
they also preserve the property through application.
With a completely analogous definition and proof we get the
expected result of conjunctivity over (non-empty) universal quantification. The non-empty requirement is not actually stressed during

Draft

K. Keimel and G. Plotkin. Mixed powerdomains for probability and
nondeterminism. submitted to LMCS, 2016.
K. R. M. Leino. Dafny: An automatic program verifier for functional
correctness. LPAR. 2010.
E. Moggi. Computational lambda-calculus and monads. LICS. 1989.

21

2016/11/9

A. Nanevski, J. G. Morrisett, and L. Birkedal. Hoare type theory, polymorphism and separation. JFP, 18(5-6):865–911, 2008.
A. Nogin. Quotient Types: A Modular Approach, pages 263–280. Springer
Berlin Heidelberg, Berlin, Heidelberg, 2002.
C. Paulin-Mohring. Introduction to the Calculus of Inductive Constructions.
In B. W. Paleo and D. Delahaye, editors, All about Proofs, Proofs for
All, volume 55 of Studies in Logic (Mathematical logic and foundations).
College Publications, 2015.
G. Plotkin and M. Pretnar. Handlers of Algebraic Effects, pages 80–94.
Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.
A. Sabelfeld and A. C. Myers. Language-based information-flow security.
IEEE J.Sel. A. Commun., 21(1):5–19, 2006.
D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières. Flexible dynamic
information flow control in haskell. SIGPLAN Not., 46(12):95–106, 2011.
N. Swamy, N. Guts, D. Leijen, and M. Hicks. Lightweight monadic
programming in ML. ICFP, 2011.
N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. Verifying
higher-order programs with the Dijkstra monad. PLDI, 2013.
N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest,
K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue,
and S. Z. Beguelin. Dependent types and multi-monadic effects in F*.
POPL. 2016.
P. Wadler. Comprehending monads. In Proceedings of the 1990 ACM
Conference on LISP and Functional Programming. 1990.
P. Wadler. The essence of functional programming. POPL. 1992.
P. Wadler. Monads and composable continuations. Lisp Symb. Comput., 7
(1):39–56, 1994.

Draft

22

2016/11/9

