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

Ohad Kammar, Dylan McDermott

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 retur…