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

Journal article

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.

Authors: Kammar, O; McDermott, D

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Electronic Notes in Theoretical Computer Science
• Volume: 341
• Pages: 239-260
• Publication date: 2018-12-11
• DOI: 10.1016/j.entcs.2018.11.012
• EISSN: 1571-0661
• ISSN: 1571-0661
• Keywords: monads; computational effects; fibrations; denotational semantics; logical relations; type-and-effect systems; factorisation systems