# Overview

Atlassian Sourcetree is a free Git and Mercurial client for Windows.

Atlassian Sourcetree is a free Git and Mercurial client for Mac.

# Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
This is the Coq formalisation that accompanies the "[Handle with Care](https://bitbucket.org/pl-uwr/aleff-logrel/downloads/popl18e.pdf)"
paper.
## Compilation instructions
The development has been tested under Coq version 8.6.1. To compile,
simply issue `make` in the top-level directory of the project.
## Structure of the development
Here, we briefly discuss the mapping between the paper and the
development, noting which modules of the development correspond to
which sections of the paper. We also make note of the parts of the
development that are elided in the paper.
### Libraries
The development uses Biernacki and Polesiuk's
[IxFree](https://bitbucket.org/ppolesiuk/ixfree) library, which is a
shallow embedding in Coq of a step-indexed logic proposed in "Logical
Step-indexed Logical Relations" (LSLR) by Dreyer et al. For ease of
use, we package the library with the development. It is contained in
the `IxFree` subdirectory.
### The calculus of algebraic effects (Section 2 of the paper)
This part of the paper discusses the syntax and semantics of the
calculus, as well as the type system we use for the language. It is
mapped to the `Lang` subdirectory of the development. More precisely:
* The syntax of the calculus (Section 2.1) is formalised in module
[Syntax](Lang/Syntax.v). The documentation within the file discusses
the representation issues, particularly the treatment of open terms
and open types. Note that the notion of "freedom" defined in Fig. 2
of the paper is generalised in the development for technical
reasons.
* The operational semantics (Section 2.2) is defined in module
[Reduction](Lang/Reduction.v). The reduction definition follows the
version presented in Fig. 3 almost to the letter.
* The type system (Section 2.3) is defined in module
[Typing](Lang/Typing.v). Note that since the openness of types is
tracked through (dependent) indexing, the well-formedness judgments
are not necessary in their paper forms; instead, typing of
operations in the context of effects is used explicitly.
* The two modules [SyntaxProperties](Lang/SyntaxProperties.v) and
[ReductionProperties](Lang/ReductionProperties.v) contain additional
lemmas (respectively, about weakening and substitution, and about
reduction) that are not explicitly presented in the paper.
* The standard notion of contextual approximation, that immediately
gives rise to the notion of contextual equivalence briefly invoked
in Section 3.4, is formally developed in module
[CtxApprox](Lang/CtxApprox.v). As it is a fully syntactic,
reduction-based property, it is more appropriate to develop it
within this package, rather than as part of `BinaryRelation`.
### The logical relation (Section 3 of the paper)
This is the crucial technical section of the paper, where we develop a
relational model for the calculus of the previous
section. Consequently, the corresponding part of the development is
also quite mathematical. This part of the development can be found in
the `BinaryRelation` subdirectory; we give the overview of the modules
and their relation to the paper below.
* Module [ProgramObs](BinaryRelation/ProgramObs.v) defines the
observation relation (step-indexed cotermination at unit values) and
some of its simple properties. This is (informally defined) in
Section 3.2 (Section 3.1 briefly introduces step-indexing, which is
provided by `IxFree`).
* Module [Core](BinaryRelation/Core.v) gives the base definitions of
the logical relation, which correspond to the remainder of Section
3.2. Note that the recursion in the definitions is to a
large extent disentangled, since the crucial step-indexed relations
are defined as unique fixed-points of contractive maps�so we need to
define the maps and prove that they are contractive.
* Modules [Properties](BinaryRelation/Properties.v),
[EffectSubst](BinaryRelation/EffectSubst.v) and
[DefUnroll](BinaryRelation/DefUnroll.v) provide useful properties
about, respectively, expression reduction, effect row weakening and
substitution, and rolling/unrolling the logical relation
definitions.
* Module [HandlerRel](BinaryRelation/HandlerRel.v) defines the logical
relation for effect handlers and proves some helper lemmas about it.
* Module [ContextRel](BinaryRelation/ContextRel.v) defines the logical
relation for *partial* evaluation contexts (cf. Section 3.3), and
proves useful properties about it, in particular Lemma 2, and a
general lemma that subsumes Lemmas 3 & 4.
* Module [Subsumption](BinaryRelation/Subsumption.v) proves
compatibility of the logical relation wrt. the subtyping and effect
subsumption.
* Module [Compatibility](BinaryRelation/Compatibility.v) proves
compatibility of the logical relation wrt. the typing rules of the
calculus.
* Module [Soundness](BinaryRelation/Soundness.v) proves the soundness
of the logical relation wrt. contextual equivalence (as a corollary
of its adequacy and a precongruence).
* Module [TypeSoundness](BinaryRelation/TypeSoundness.v) shows the
type-soundness theorem (i.e., well-typed programs do not go wrong),
as a corollary of the relation's adequacy and the fundamental
property.
### Reasoning about algebraic effects and handlers (Section 4 of the paper)
This part of the paper shows how the logical relation can be used to
prove both equivalences of concrete programs and general type-based
equations. We present one example of each of these types of proofs in
the `Examples` subdirectory. These exhibit the usual characteristics:
the more general equivalences are easier to handle, since there is
less concrete code that needs to be reduced, etc. On the other hand,
the concrete equivalence requires performing actual reduction steps,
which tends to be fiddly without highly-engineered tactic support that
provides some symbolic execution capabilities. However, these still
serve as representative examples of how the proofs of Section 4 would
proceed.
* The module [PureEffectful](Examples/PureEffectful.v) corresponds to
Section 4.1 of the paper (pure vs effectful computations), and shows
how one may use the relation to show that a pure computation is
equivalent to a computation that uses effects. Note that while the
complete example only uses the effects internally, we also show in
the lemmas how pure code can be shown equivalent to externally
effectful one�and under what conditions.
* The module [ReturnClause](Examples/ReturnClause.v) corresponds to
Section 4.3 of the paper, where we show that the traditional
"return" clauses of effect handlers can be desugared away in our
calculus.