Repository logo
 

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

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Kammar, Ohad 

Abstract

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.

Description

Keywords

Journal Title

Electronic Notes in Theoretical Computer Science

Conference Name

34th Conference on the Mathematical Foundations of Programming Semantics: MFPS 2018

Journal ISSN

1571-0661

Volume Title

341

Publisher

Elsevier BV
Sponsorship
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’.