Session 10B

Chair: Amr Sabry

• 13:00: Dariusz Biernacki, Mateusz Pyzik, Filip Sieczkowski. A Reflection on Continuation-Composing Style.     See abstract ...
  ABSTRACT. We present a study of the continuation-composing style (CCS) that describes the image of the CPS translation of Danvy and Filinski’s shift and reset delimited-control operators. In CCS continuations are composable rather than abortive as in the traditional CPS, and, therefore, the structure of terms is considerably more complex. We show that the CPS translation from Moggi’s computational lambda calculus extended with shift and reset has a right inverse and that the two translations form a reflection i.e., a Galois connection in which the target is isomorphic to a subset of the source (the orders are given by the reduction relations). Furthermore, we use this result to show that Plotkin’s call-by-value lambda calculus extended with shift and reset is isomorphic to the image of the CPS translation. This result, in particular, provides a first direct-style transformation for delimited continuations that is an inverse of the CPS transformation up to syntactic identity.
• 13:30: Andrej Ivaskovic, Alan Mycroft, Dominic Orchard. Data-flow analyses as effects and graded monads.     See abstract ...
  ABSTRACT. In static analysis, two general frameworks have been studied extensively: monotone data-flow analysis and type-and-effect systems. Recent developments in effect systems have pursued different axiomatisations of the effect algebras used, separating alternation (if-then-else) from sequencing, capturing control-flow more precisely. Whilst effect systems have been described as a general framework for static analysis, their relationship to data-flow analysis has remained unclear. This paper shows that monotone data-flow analyses can indeed be encoded as effect systems, via algebras of transfer functions. This helps to answer questions about the appropriate structure for general effect algebras; for non-distributive constant propagation analysis, we show that recent suggestions of using "effect quantales" are not general enough. Via a recasting of the McCarthy transformation, we then model data-flow effects using graded monads. This gives a model of data-flow analyses which can be used for reasoning about compiler correctness or embedding data-flow analyses into types.
• 14:00: Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers.     See abstract ...
  ABSTRACT. We present a complete coinductive syntactic theory for an untyped calculus of algebraic operations and handlers, a relatively recent concept that augments a programming language with unprecedented flexibility to define, combine and interpret computational effects. Our theory takes the form of a normal-form bisimilarity and its soundness w.r.t. contextual equivalence hinges on using so-called context variables to test evaluation contexts comprising normal forms other than values. The theory is formulated in purely syntactic elementary terms and its completeness demonstrates the discriminating power of handlers. It crucially takes advantage of the clean separation of effect handling code from effect raising construct, a distinctive feature of algebraic effects, not present in other closely related control structures such as delimited-control operators.