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

DOI10.1016/j.entcs.2018.11.012OpenAlexW2963951024WikidataQ113317485 ScholiaQ113317485MaRDI QIDQ2134832

Dylan McDermott, Ohad Kammar

Publication date: 3 May 2022

Full work available at URL: https://arxiv.org/abs/1804.03460

zbMATH Keywords

fibrationsdenotational semanticsmonadscomputational effectslogical relationstype-and-effect systemsfactorisation systems

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Deriving logical relations from interpretations of predicate logic ⋮ Canonical Gradings of Monads ⋮ An algebraic theory for shared-state concurrency

Uses Software

• Eff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming with algebraic effects and handlers
• Epis need not be dense
• Constructions of factorization systems in categories
• Categorical logic and type theory
• Algebraic operations and generic effects
• Relating computational effects by \(\top \top \)-lifting
• Strong functors and monoidal monads
• Factorization systems and fibrations
• Algebraic foundations for effect-dependent optimisations
• Handlers of Algebraic Effects
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Two addenda to the author's ‘Transfinite constructions’
• Axiomatic Domain Theory in Categories of Partial Maps
• Proof-Relevant Logical Relations for Name Generation
• A monad for full ground reference cells
• Compiling standard ML to Java bytecodes
• The marriage of effects and monads
• No value restriction is needed for algebraic effects and handlers
• Computer Science Logic
• Parametric effect monads and semantics of effect systems

This page was built for publication: Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics