View: session overviewtalk overview
13:00 | Semi-Axiomatic Sequent Calculus ABSTRACT. We present the semi-axiomatic sequent calculus (SAX) that blends features of Gentzen's sequent calculus with an axiomatic formulation of intuitionistic logic. We develop and prove a suitable analogue to cut elimination and then show that a natural computational interpretation of SAX provides a simple form of shared memory concurrency. |
13:30 | A Gentzen-style monadic translation of Goedel's System T ABSTRACT. We introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen's negative translation of classical logic. By instantiating the monad and the base case of the logical relation, we reveal various properties and structures of T-definable functionals such as majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant. |
14:00 | The difference lambda-calculus: a language for difference categories. PRESENTER: Mario Alvarez-Picallo ABSTRACT. Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of infinitesimal arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only up to an infinitesimal perturbation. In this work, we construct a simply-typed calculus in the spirit of the differential lambda-calculus equipped with syntactic infinitesimals and show how its models correspond to difference lambda-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials. |
13:00 | A Reflection on Continuation-Composing Style PRESENTER: Mateusz Pyzik 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 | Data-flow analyses as effects and graded monads PRESENTER: Andrej Ivaskovic 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 | A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers PRESENTER: Piotr Polesiuk 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. |