Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics

Conference Object
Change log
Kammar, Ohad 

Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for type-and-effect systems involves a parameterised family of monads whose size is exponential in the number of effects. We derive such refined semantics from a single monad over a category, a choice of algebraic operations for this monad, and a suitable factorisation system over this category. We relate the derived semantics to the original semantics using fibrations for logical relations. Our proof uses a folklore technique for lifting monads with operations.

Journal Title
Electronic Notes in Theoretical Computer Science
Conference Name
34th Conference on the Mathematical Foundations of Programming Semantics: MFPS 2018
Journal ISSN
Volume Title
Elsevier BV
Engineering and Physical Sciences Research Council (EP/N509620/1)
This work has been supported by an Engineering and Physical Sciences Research Council (EPSRC) studentship, EPSRC grants EP/N007387/1 ‘Quantum computation as a programming language’, EPSRC Leadership Fellowship EP/H005633/1 ‘Semantic Foundations for Real-World Systems’, Institute for Information & Communications Technology Promotion (IITP) grant funded by the Korea government (MSIP) No. R0190-16-2011 ‘Development of Vulnerability Discovery Technologies for IoT Software Security’, a Balliol College Oxford Career Development Fellowship, European Research Council Grant ‘Events, Causality and Symmetry — the next generation semantics’, and Isaac Newton Trust grant ‘algebraic theories, computational effects, and concurrency’.