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.
Original language | English |
---|---|
Pages (from-to) | 239 - 260 |
Number of pages | 22 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 341 |
DOIs | |
Publication status | Published - 1 Dec 2018 |
Event | 34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) - Dalhousie University, Halifax, Canada Duration: 6 Jun 2018 → 9 Jun 2018 https://www.mathstat.dal.ca/mfps2018/ |
Keywords / Materials (for Non-textual outputs)
- computational effects
- denotational semantics
- logical relations
- fibrations
- factorisation systems
- monads
- type-and-effect systems