# Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics

arXiv: https://arxiv.org/abs/1804.03460 · HTML: https://mlsanity.com/paper/1804.03460/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Apr 2018.

## Built on by (most cited first, 1 of 1)

- [ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs](https://mlsanity.com/paper/2302.10636/) (2023)

## Abstract (arXiv)

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.