Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics
Electronic Notes in Theoretical Computer Science
MetadataShow full item record
Kammar, O., & McDermott, D. (2018). Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics. Electronic Notes in Theoretical Computer Science, 341 239-260. https://doi.org/10.1016/j.entcs.2018.11.012
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.
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’.
External DOI: https://doi.org/10.1016/j.entcs.2018.11.012
This record's URL: https://www.repository.cam.ac.uk/handle/1810/287501
Attribution-NonCommercial-NoDerivatives 4.0 International
Licence URL: https://creativecommons.org/licenses/by-nc-nd/4.0/