HTTPS SSH
# 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.