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

Ohad Kammar, Dylan McDermott

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)239 - 260
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Volume341
DOIs
Publication statusPublished - 1 Dec 2018
Event34th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2018) - Dalhousie University, Halifax, Canada
Duration: 6 Jun 20189 Jun 2018
https://www.mathstat.dal.ca/mfps2018/

Keywords

  • computational effects
  • denotational semantics
  • logical relations
  • fibrations
  • factorisation systems
  • monads
  • type-and-effect systems

Fingerprint Dive into the research topics of 'Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics'. Together they form a unique fingerprint.

Cite this