=Paper=
{{Paper
|id=Vol-1949/ICTCSpaper06
|storemode=property
|title= Effectful Applicative Similarity for Call-by-Name Lambda Calculi
|pdfUrl=https://ceur-ws.org/Vol-1949/ICTCSpaper06.pdf
|volume=Vol-1949
|authors=Ugo Dal Lago,Francesco Gavazzo,Ryo Tanak
|dblpUrl=https://dblp.org/rec/conf/ictcs/LagoGT17
}}
== Effectful Applicative Similarity for Call-by-Name Lambda Calculi==
https://ceur-ws.org/Vol-1949/ICTCSpaper06.pdf
Effectful applicative similarity
for call-by-name lambda calculi
Ugo Dal Lago1 , Francesco Gavazzo2 , and Ryo Tanaka3
1
Università di Bologna & INRIA Sophia Antipolis
ugo.dallago@unibo.it
2
Università di Bologna & INRIA Sophia Antipolis
francesco.gavazzo2@unibo.it
3
The University of Tokyo
anaphalis.alpicola@gmail.com
Abstract. We introduce a notion of applicative similarity in which
not terms but monadic values arising from the evaluation of effectful
terms, can be compared. We prove this notion to be fully abstract when-
ever terms are evaluated in call-by-name order. This is the first full-
abstraction result for such a generic, coinductive methodology for pro-
gram equivalence.
1 Introduction
Program equivalence is a crucial notion in the theory of programming languages,
and its study is at the heart of programming language semantics. When higher-
order functions are available, programs have a non-trivial interactive behaviour,
and giving a satisfactory and at the same time handy definition of program
equivalence becomes complicated. The problem has been approached, in many
different ways, e.g. by denotational semantics or by contextual equivalence. These
two approaches have their drawbacks, the first one relying on the existence of
a denotational model, the latter quantifying over all contexts, thus making the
task of proving programs equivalent quite hard. Handier methodologies for prov-
ing programs equivalent have been introduced along the years based on logical
relations and applicative bisimilarity. Logical relations were originally devised
for typed, normalising languages, but later generalised to more expressive for-
malisms, e.g., through step-indexing [2] and biorthogonality [3]. Starting from
Abramsky’s pioneering work on applicative bisimilarity [1], coinduction has also
been proved to be a useful methodology for program equivalence, and has been
applied to a variety of calculi and language features [17].
The just described scenario also holds when the underlying calculus is
not pure, but effectful. There have been many attempts to study effectful λ-
calculi [19,16] by way of denotational semantics [9,8], logical relations [4], and
applicative bisimilarity [14,7,5]. But while the denotational and logical relation
semantics of effectful calculi have been studied in the abstract [11,13], the same
cannot be said about applicative bisimilarity and related coinductive techniques.
There is a growing body of literature on applicative bisimilarity for calculi with,
e.g., nondeterministic [14], and probabilistic effects [7], but each notion of an
effect has been studied independently, often getting different results. Distinct
proofs of congruence for applicative bisimilarity, even if done through a common
methodology, namely the so-called Howe’s method [12], do not at all have the
same difficulty in each of the cases cited above.
The observations above naturally lead to some questions. Is there any way to
factor out the common part of the congruence proof for applicative bisimilarity in
effectful calculi? Where do the limits on the correctness of applicative bisimilarity
lie, in presence of effects?
This paper is part of a longstanding research effort directed to giving answers
to the questions above. The first two authors, together with Paul Blain Levy,
have recently introduced a general notion of applicative bisimilarity for lambda-
calculi based on monads and relators [6]. This provides, under mild conditions, a
sound methodology for checking contextual equivalence of programs. The central
idea is to take simulations as relations on terms and to use a relator to lift a
(candidate) simulation to a relation on the monadic images of values. There is
however little hope to prove a generic full-abstraction result in such a setting,
although for certain notions of an effect, full abstraction is already known to
hold [1,5].
In this paper, we study a different notion of simulation, which puts in relation
not terms but their semantics. This way, interaction between terms and the
environment can be modeled by an ordinary, deterministic, transition system
and, with minimal side conditions, similarity can be proved to be not only a
sound, but also to coincide with the contextual preorder. This, however, only
holds when terms are call-by-name evaluated.
We first of all introduce a computational λ-calculus in which general alge-
braic effects can be represented, and give a monadic call-by-name operational
semantics for it, showing how the latter coincides with the expected one in many
distinct concrete examples. We then show how applicative bisimilarity can be
defined for any instance of such a monadic λ-calculus, and that in all cases it is
also fully-abstract. Along the lines, we also prove a CIU Theorem.
2 Mathematical Preliminaries
In this section, we recall some basic definitions and results on complete partial
orders, categories, and monads. Due to space constraints, there is no hope to be
comprehensive. The reader can refer to [6] for details and further references.
We assume basic familiarity with domain theory. In particular, we do not
define the notions of directed complete partial order (dcpo for short), and of
pointed dcpo (dcppo for short). Similarly, we do not give the notions of mono-
tone, continuous, and strict functions, which are standard. Following [19,20],
we consider operations producing effects coming from a signature. Semantically,
dealing with operation symbols requires the introduction of appropriate algebraic
structures interpreting such operation symbols as suitable functions. Combining
the algebraic and the order theoretic structures just described, leads to consider
algebras carrying a domain structure (dcppo, in this paper), and with all func-
tion symbols interpreted as continuous functions. The formal notion capturing
all these desiderata is the one of a continuous Σ-algebra [10]. Recall that a signa-
ture Σ = (F, α) consists of a set F of operation symbols and a map α : F → N,
assigning to each operation symbol a (finite) arity.
Definition 1. Given a signature Σ, a continuous Σ-algebra is a dcppo (D, v, ⊥)
such that for any function symbol σ in Σ there is an associated continuous
function σD : Dα(σ) → D.
Example 1. Let X be a set: the following are examples of dcppo (see [6] for
further examples).
1. The flat lifting Xundef of X, defined as X + {undef}, ordered as follows: x v y
iff x = undef or x = y.
2. The set (X +E)undef (think to E as a set of exceptions), ordered as in previous
example. We can consider the signature Σ = {raise(e) | e ∈ E}, where each
operation symbol raise(e) is interpreted as the constant inl (inr (e)).
3. The powerset PX, ordered by inclusion. The least upper bound of a chain of
sets is their union, whereas the bottom is the empty set. We can consider the
signature Σ = {⊕} containing a binary operation symbol for nondetermin-
istic choice. The latter can be interpreted as (binary) union, which is indeed
continuous. P
4. The set of discrete subdistributions DX = {µ : X → [0, 1] | x∈X µ(x) ≤ 1}
over X, ordered pointwise: µ v ν iff ∀x ∈ X. µ(x) ≤ ν(x). The dcppo
structure is pointwise induced by the one of [0, 1] with the natural ordering.
The least element is the always zero distribution x 7→ 0 (note that the latter
is a subdistribution, and not a distribution). We can consider the signature
Σ = {⊕p | p ∈ [0, 1]} with a family of probabilistic choice operations indexed
by real numbers in [0, 1]. We can interpret ⊕p as the binary operation (x, y) 7→
p · x + (1 − p) · y, which is indeed continuous.
Since we are interested in effectul calculi, we rely on monads hT, η, µi [15]
(on the category of sets and functions) to model the kind of effects we are
interested in. For a function f : X → T Y we denote by f † its Kleisli lifting
µY ◦ T f : T X → T Y . We are interested in monads carrying a continuous Σ-
algebra structure. That is, for a fixed signature Σ, we require a monad T to
come with a map associating to any set X an order vX on T X and an element
⊥X ∈ T X such that (T X, vX , ⊥X ) is a continuous Σ-algebra wrt the order
vX . We also require Kleisli lifting to satisfy specific continuity conditions4 . The
reader can consult [6] for details.
Example 2. It is easy to see that all the constructions in Example 1 carry a
monad structure.
4
For all sets X, Y we require (notice that T Y being a dcppo, so is X → T Y ) both
sup F † = supf ∈F f † and f † (sup T ) = supt∈T f † (t) to hold, where F ⊆ X → T Y
and T ⊆ T X are directed.
Finally, following [19] we require monads to properly interact with algebraic
operations.
Definition 2. Let T be a monad carrying a continuous Σ-algebra structure.
We say that T is algebraic if for any function f : X → T Y , f † is Σ-algebra
homomorphism. That is,
f † (σX (t1 , . . . , tn )) = σY (f † (t1 ), . . . , f † (tn )).
We treat ⊥X as an algebraic constant, so that the above definition implies
f † (⊥X ) = ⊥Y , for any f : X → T Y .
3 Syntax and Operational Semantics
In this section we introduce a computational λ-calculus and give it call-by-name
monadic operational semantics following [19]. We fix a signature Σ and a monad
hT, η, µi satisfying the conditions of previous section.
Definition 3. For a fixed signature Σ the sets Λ◦ and V ◦ of terms and values
are defined as follows:
M, N ::= V | M N | σ(M, . . . , M ) V ::= x | λx.M.
We let letters M, N . . . and V, W, . . . to range over terms and values, respectively.
We denote by Λ(x̄) the set of terms with free variables from x̄ and write Λ for
the set Λ(∅). Similar conventions apply to the set of values.
We give operational semantics to our calculus as in [19] (which we refer to
for details). An indexed function symbol σi consists of a function symbol σ ∈ Σ
together with an index i ∈ {0, . . . , α(σ) − 1}. Evaluation contexts are defined
by the simple grammar: E ::= [·] | EM . Small-step semantics is defined by
·
means of a binary relation → on closed terms and of a ternary relation → on
closed terms and indexed function symbols, according to the rules in Figure 1.
σ
(λx.M )N → M [N/x] M →N M →i N
σ σ
σ(M0 , . . . , Mn−1 ) →i Mi E[M ] → E[N ] E[M ] →i E[N ]
Fig. 1. Small-step Semantics.
We now give a monadic multi-step operational semantics to the above calcu-
lus. Multi-step operational semantics relates a closed term M to a set of elements
in T V, representing finite approximations of its evaluation. We refer to elements
in T V as monadic values.
Definition 4. Define the relation ⇒ between closed terms and monadic values
by the rules in Figure 2, where ⊥ is the bottom element of T V and σV is the
interpretation of σ in T V.
σ
M ⇒⊥ M →N N ⇒t M →i Ni Ni ⇒ t i
V ⇒ η(V ) M ⇒t M ⇒ σV (t1 , . . . , tn )
Fig. 2. Big-step Semantics.
It is easy to prove that the set {t ∈ T V | M ⇒ t} of finite approximations of
(the execution of) M is directed, meaning that it has a least upper bound.
Definition 5. Define the evaluation function J·K : Λ0 → T (V) by JM K =
supM ⇒t t.
4 Observational Equivalence
In this section we give a general notion of observation on top of which we define
several behavioural preorders. We rely on the basic assumption that we can only
observe side effects.
Intuitively, an observation is a function that takes an element in T V repre-
senting the computation of a term and returns what we can observe about it.
Since we assume that the observable part of a computation consists only of the
side effects that could occur during such computation, such observable part is
uniquely determined by the semantics of the operations considered.
Since we are working with an untyped calculus, it is customary not to observe
values5 .
Definition 6. Let 1 = {∗} be the one element set and !X : X → 1 be the
unique function mapping each element in X to ∗. Define the observation function
Obs : T V → T 1 as T (!V ). Observations trivially extends to terms by defining
Obs(M ) as Obs(JM K).
Note that by very definition of monad we have T (!V ) = (η1 ◦ !)† . As a conse-
quence, since T is algebraic an easy calculation shows that we have the following
equalities:
Obs(⊥) = ⊥T (1) ;
Obs(ηV (V )) = η1 (∗);
Obs(σV (t1 , . . . , tn ) = σ1 (Obs(t1 ), . . . , Obs(tn )).
5
One is usually more concerned with different notions of convergence, such as may
convergence or the probability of convergence.
Remark 1. Notice that the function Obs is uniquely determined by the effect
signature. That is because of our choice of not distinguishing between values.
Nevertheless, it is easy to see that our definition of Obs can be extended to
any function f : V → X, where the set X represents a set of observables and
f encodes a ground observation on values. In fact, we would have Obs(V ) =
(η ◦ f )(V ).
We can now give a general notion of contextual preorder.
Definition 7. Define contexts by the following two grammars
C ::= · | M C | CM | λx.C
The contextual proerder ≤ctx is defined as follows:
M ≤ctx N ⇐⇒ ∀C. Obs(JC[M ]K) v Obs(JC[N ]K)
Example 3. Referring to Example 1:
1. For pure λ-calculus we consider the monad T X = Xundef thus obtaining
Obs : Vundef → 1undef satisfying: Obs(η(V )) = ∗ and Obs(⊥) = undef. We
thus have Obs(M ) = undef iff M ↑. As a consequence, M ≤ctx N iff for
any context C, C[M ] ↑ =⇒ C[N ] ↑, which is the usual notion of contextual
preorder.
2. For the nondeterministic calculus of Example 1 we have P(1) = {∅, ∗} so
that: Obs(⊥) = ∅, Obs(V ) = {∗} and Obs(M ⊕ N ) = Obs(M ) ∪ Obs(N ).
We thus have Obs(M ) = {∗} iff M may converge. Again, we have recovered
the usual notion of contextual preorder.
3. For the probabilistic calculus of Example 1 we first observe that D(1) ∼
= [0, 1].
It is then easy to see that we obtain Obs(⊥) = 0, Obs(V ) = 1 and Obs(M ⊕p
N ) = p · Obs(M ) + (1 − p) · Obs(N ). We have Obs(M ) = P r(M ⇓), meaning
that M ≤ctx N holds iff for any context C, P r(C[M ] ⇓) ≤ P r(C[N ] ⇓) holds.
5 Applicative Similarity
In this section we define the notion of applicative simulation and prove full
abstraction of applicative similarity wrt the CIU preorder. First of all, we lift
the notion of application from terms to monadic values.
Definition 8. For t ∈ T V and M ∈ Λ define the application t ◦ M ∈ T V of M
to t as6 : ((λx.L) 7→ JL[M/x]K)† (t).
It is easy to see that we have:
⊥ ◦ M = ⊥;
η(λx.N ) ◦ M = JN [M/x]K;
σV (t1 , . . . , tn ) ◦ M = σV (t1 ◦ M, . . . , tn ◦ M );
and that for terms M, N we have JM N K = JM K ◦ N.
6
Note that with a similar strategy it is possible to extend application to T V ◦ .
Definition 9. A relation R ⊆ T V ×T V is an applicative simulation if whenever
(t, u) ∈ R we have
1. Obs(t) v Obs(u);
2. For any term M , (t ◦ M, u ◦ M ) ∈ R.
Applicative similarity . is defined as the largest applicative simulation. We ex-
tend applicative similarity to terms as follows (we overload the notation): M . N
iff JM K . JN K.
Our main result is a full abstraction theorem stating that applicative simi-
larity and the contextual preorder coincide. The proof of such result relies on a
CIU Theorem [18].
Definition 10. The CIU preorder ≤ciu is defined by
M ≤ciu N ⇐⇒ ∀E. Obs(JE[M ]K) v Obs(JE[N ]K)
where E ranges over the set of evaluation contexts.
Theorem 1 (CIU Equivalence). The following holds: ≤ciu = ≤ctx .
We postpone the proof of Theorem 1 to the next section. We spend the rest
of this section showing that applicative similarity is fully abstract with respect
to the CIU preorder.
Proposition 1 (Soundness). The following holds: . ⊆ ≤ciu .
Proof. Clearly M . N implies M L . N L, for any term L. It is then straightfor-
ward to prove that for any evaluation context E, M . N implies E[M ] . E[N ],
meaning, in particular, Obs(E[M ]) v Obs(E[N ]). t
u
To prove that . is fully abstract wrt ≤ciu we have to prove ≤ciu ⊆ .. To do
so we define a grammar for monadic values as follows:
T ::= t | T • M.
We refer to terms generated by the above grammar as monadic terms. We can
give semantics to monadic terms as monadic values via the mapping:
HtI = t;
HT • M I = HT I ◦ M.
Monadic term contexts (mt-contexts, for shorts) are defined by:
C ::= · | C • M.
Therefore a mt-context is an expression of the form · • M1 • · · · • Mn (where we
assume • to be left associative). The lifting 4ciu of the CIU preorder to monadic
terms is then defined by
T 4ciu U ⇐⇒ ∀C. Obs(HC[T ]I) v Obs(HC[U ]I).
It is easy to see that there is a bijective correspondence between evaluation
contexts and mt-contexts from which it follows the equation ≤ciu = 4ciu .
Proposition 2. The following holds: 4ciu ⊆ . .
Proof. We prove that 4ciu is an applicative simulation. Suppose t 4ciu u. Obvi-
ously Obs(t) v Obs(u) since HtI = t (and similarly for u). Let now M be a term.
We have to prove that t ◦ M 4ciu u ◦ M holds. Let C = · • M1 • · · · • Mn be a
mt-context. Then we have to prove: Obs(HC[t◦M ]I) = Obs(HC[u◦M ]I). That im-
mediatly follows from t 4ciu u once one observes that H(·•M1 •· · ·•Mn )[t◦M ]I =
H(· • M • M1 • · · · • Mn )[t]I holds. t
u
Corollary 1. The following holds: ≤ciu ⊆ . .
Together with Proposition 1, the above corollary gives a proof of the follow-
ing:
Proposition 3. Applicative similarity is fully abstract wrt the CIU preorder.
That is: . = ≤ciu .
What remains to be done in order to prove that applicative similarity is fully
abstract wrt to the contextual preorder is to prove Theorem 1.
6 A CIU Theorem
In this section we prove Theorem 1. The proof closely follows [18], and the reader
can consult the latter for further details.
We use the notion of frame stack.
Definition 11. The set of frame stacks is defined by the following grammar:
s ::= nil | [·]M :: s.
A configuration is a pair of the form (s, M ), where s is a stack and M a
term. To a stack s = [·]N1 :: · · · :: [·]Nn , we can associate the evaluation context
Es = ·N1 · · · Nn (where to nil we associate the empty context). Vice versa, we
can associate to any evaluation context E a stack sE such that E = EsE .
We now give operational semantics to configurations. Small step semantics is
defined via a relation 7→ between configurations, whereas multi-step semantics is
defined via a relation Z⇒ between configurations and monadic values. Both these
relations are described in Figure 3.
Notice that the set {t ∈ T V | (s, M ) Z⇒ t} is directed. As a consequence, we
can define the (operational) semantics L(s, M )M of a configuration (s, M ) as
L(s, M )M = sup t.
(s,M )Z⇒t
Proposition 4. For any term M , evaluation context E and stack s, we have:
JE[M ]K = L(sE , M )M;
L(s, M )M = JEs (M )K.
In particular, we have L(nil, M )M = JM K.
(s, M ) Z⇒ ⊥
(nil, V ) Z⇒ V
(s, M N ) 7→ ([·]N :: s, M )
(s, M ) 7→ (r, N ) (r, N ) Z⇒ t
([·]N :: s, λx.M ) 7→ (s, M [N/x])
(s, M ) Z⇒ t
σ
(s, σ(M1 , . . . , Mn )) 7→i (s, Mi )
σ
(s, M ) 7→i (si , Mi ) (si , Mi ) Z⇒ ti
(s, M ) Z⇒ σV (t1 , . . . , tn )
Fig. 3. Stack Semantics.
We can now build up a proof of Theorem 1. The proof is based on an adap-
tation oh Howe’s technique for pure λ-calculus and thus we only sketch its main
part. The reader can consult [18] for details. First of all, in light of previous
proposition let us characterise the CIU preorder in terms of stacks and configu-
rations.
Definition 12. Define the CIU order ciu on terms:
M ciu N ⇐⇒ ∀s. Obs(L(s, M )M) v Obs(L(s, N )M).
Proposition 5. The following hold: ≤ciu = ciu .
Dealing with Howe’s technique, it is convenient to work with generalisations
of relations on closed terms called λ-term relations.
Definition 13. An open relation over terms is a set R of triples (x̄, M, N )
where M, N ∈ Λ(x̄). A closed λ-term relation is closed if R ⊆ Λ × Λ.
We will use infix notation and write x̄ ` M R N to indicate that (x̄, M, N ) ∈
R. Finally, we will use the notations ∅ ` M R N and M R N interchangeably.
There is a canonical way to extend a closed relation to an open one.
Definition 14. Define the open extension operator mapping a closed relation
over terms R to the open relation R◦ over terms as follows: (x̄, M, N ) ∈ R◦ iff
M, N ∈ Λ(x̄), and for all L̄, M [L̄/x̄] R N [L̄/x̄] holds.
The notions of reflexivity, symmetry and transitivity straightforwardly ex-
tend to open λ-term relation (see e.g. [18]).
We say that a relation is compatible if it is closed under the term constructors
of the language. The idea of Howe’s technique is to extend a relation R to a
relation RH that is compatible by construction. As a consequence, if M RH N
holds, then C[M ]RH C[N ] holds as well. That means that in order to prove
that a relation R is compatible it is sufficient to prove that R = RH holds.
Proving the inclusion R ⊆ RH is often immediate (provided that R satisfies
minimal properties, e.g. reflexivity and transitivity in our case), whereas the
other inclusion requires more effort.
Definition 15. Given a λ-term relation R the Howe’s lifting RH of R is in-
ductively defined by the rules in Figure 4.
x̄ ` xRM x̄ ∪ {x} ` M RH L x̄ ` λx.LRN x 6∈ x̄
How1 How2
x̄ ` xRH M x̄ ` λx.M RH N
x̄ ` M RH P x̄ ` LRH x̄ ` P RN
How3
x̄ ` M LRH N
x̄ ` Mi RH Ni x̄ ` σ(N1 , . . . , Nn )RL
How4
x̄ ` σ(M1 , . . . , Mn )RH L
Fig. 4. Howe’s Lifting.
The following lemma states some useful properties of Howe’s lifting of pre-
order relations. The proof is standard and can be found in, e.g., [7].
Lemma 1. Let R be a preorder. The following hold
1. R ◦ RH ⊆ RH .
2. RH is reflexive.
3. For any context C, x̄ ` M RH N =⇒ x̄ ` C[M ]RH C[N ].
4. R ⊆ RH .
It is easy to see that ciu is a preorder7 and thus (ciu )H is a compatible
preorder containing ciu . We extend Howe’s construction to frame stacks as
described in Figure 5.
HowStk1 ∅ ` M RH N sRH r
nilRH nil H
HowStk2
[·]M :: sR [·]N :: r
Fig. 5. Howe’s Lifting for Frame Stacks.
The main techincal part of the Howe’s method is the so-called Key Lemma,
which basically states that the Howe’s extension of a relation is contained in the
relation itself.
Lemma 2 (Key Lemma). For all closed stacks s, r and closed terms M, N , if
s(ciu )H r, M (ciu )H N , then Obs(L(s, M )M) v Obs(L(r, N )M).
Proof (Sketch.). Since Obs is continuous and L(s, M )M) = sup(s,M )Z⇒t t it is suffi-
cient to prove that for every monadic value t, if (s, M ) Z⇒ t the Obs(t) v L(r, N )M.
The latter statement can be proved by induction on the derivation of (s, M ) Z⇒ t
as in [18]. t
u
7
We are actually working with (ciu )◦ .
Corollary 2. The following holds: (ciu )H = ciu .
Proof. We already know that ciu ⊆ (ciu )H holds. To prove the other inclusion
we have to prove M (ciu )H N =⇒ M ciu N , for all terms M, N . Suppose
M (ciu )H N . Then, for any stack s, we have s(ciu )H s. By previous lemma we
have Obs(L(s, M )M) v Obs(L(s, N )M), meaning that M ciu N . t
u
We can finally prove Theorem 1.
Theorem 1 (CIU Equivalence). The following holds: ≤ctx = ≤ciu .
Proof. It is immediate to see that ≤ctx ⊆ ≤ciu . For the other inclusion, suppose
M ≤ciu N and let C be a context. We prove that C[M ] ≤ciu C[N ] (this will
give the thesis simply aplying the definition of ≤ciu with the empty context).
Since ≤ciu = ciu = (ciu )H , we have M ciu N and thus C[M ] ciu C[N ]. It
follows C[M ] ≤ciu C[N ]. t
u
7 Conclusions
We have shown how a notion of applicative similarity on call-by-name effectful
lambda-calculi can be defined and proved fully-abstract. This is very much in line
with logical relations as introduced in [13], but simpler and applicable to untyped
λ-calculi. The underlying transition system has monadic values as states, and
is essentially deterministic. This is indeed the reason the framework is only
applicable to call-by-name (and not to call-by-value) calculi, in contrast with [6].
In fact, in the probabilistic call-by-value case our notion of applicative similarity
on monadic values is unsound for the contextual preorder, as witnessed by the
terms λx.(x ⊕p Ω), (λx.x) ⊕p (λx.Ω), and the context (λx.x(x(λy.y)))[·].
References
1. Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research
Topics in Functional Programming, pages 65–117. Addison Wesley, 1990.
2. Andrew W. Appel and David A. McAllester. An indexed model of recursive
types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst.,
23(5):657–683, 2001.
3. Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. Rela-
tional semantics for effect-based program transformations: higher-order store. In
Proc. of PPDP 2009, pages 301–312, 2009.
4. Ales Bizjak and Lars Birkedal. Step-indexed logical relations for probability. In
Proc. of FOSSACS 2015, pages 279–294, 2015.
5. Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation
and call-by-value λ-calculi. In Proc. of ESOP 2014, volume 8410 of LNCS, pages
209–228. Springer, 2014.
6. Ugo Dal Lago, Francesco Gavazzo, and Paul Levy. Effectful applicative bisimilarity:
Monads, relators, and Howe’s method (long version). Available at https://arxiv.
org/abs/1704.04647, 2017.
7. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences
for higher-order probabilistic functional programs. In Proc. of POPL 2014, pages
297–308, 2014.
8. Vincent Danos and Russell Harmer. Probabilistic game semantics. ACM Transac-
tions on Computational Logic, 3(3):359–382, 2002.
9. Ugo de’Liguoro and Adolfo Piperno. Non deterministic extensions of untyped
lambda-calculus. Inf. Comput., 122(2):149–177, 1995.
10. Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright.
Initial algebra semantics and continuous algebras. J. ACM, 24(1):68–95, 1977.
11. Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for
monadic types. Mathematical Structures in Computer Science, 18(6):1169–1217,
2008.
12. Douglas J. Howe. Proving congruence of bisimulation in functional programming
languages. Inf. Comput., 124(2):103–112, 1996.
13. Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational
metatheory for algebraic effects. In Proc. of LICS 2010, pages 209–218. IEEE
Computer Society, 2010.
14. Søren B. Lassen. Relational Reasoning about Functions and Nondeterminism. PhD
thesis, Dept. of Computer Science, University of Aarhus, May 1998.
15. Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag,
1971.
16. Eugenio Moggi. Computational lambda-calculus and monads. In Proc. of (LICS
1989, pages 14–23. IEEE Computer Society, 1989.
17. A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer
and A. M. Pitts, editors, Semantics and Logics of Computation, Publications of
the Newton Institute, pages 241–298. Cambridge University Press, 1997.
18. Andrew M. Pitts. Howe’s method for higher-order languages. In D. Sangiorgi and
J. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, volume 52
of Cambridge Tracts in Theoretical Computer Science, chapter 5, pages 197–232.
Cambridge University Press, November 2011.
19. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Proc. of
FOSSACS 2001, pages 1–24, 2001.
20. Gordon D. Plotkin and John Power. Algebraic operations and generic effects.
Applied Categorical Structures, 11(1):69–94, 2003.