Combining effects and coeffects via grading

DOI10.1145/2951913.2951939MaRDI QIDQ2985796zbMATH OpenOpenAlexWikidataFDO

Authors Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu

Publication date 10 May 2017

Published in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://kar.kent.ac.uk/57480/1/bieffects.pdf

zbMATH Keywords

effectstypescategorical semanticsmonadscomonadsdistributive lawsgradingcoeffects

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18)

Recommendations

• Coeffects: a calculus of context-dependent computation
• Coeffects: unified static analysis of context-dependence
• Effect systems revisited -- control-flow algebra and semantics
• A core quantitative coeffect calculus
• Unifying graded and parameterised monads

Cited in

(24)

• Unifying graded and parameterised monads
• Formalizing Soundness of Contextual Effects
• When programs have to watch paint dry
• Diagrammatic algebra of first order logic
• Coeffects: unified static analysis of context-dependence
• Effect systems revisited -- control-flow algebra and semantics
• Resourceful program synthesis from graded linear types
• A Java-like calculus with heterogeneous coeffects
• Deciding Equations in the Time Warp Algebra
• Generalized bounded linear logic and its categorical semantics
• Graded Hoare logic and its categorical semantics
• Graded modal dependent type theory
• The syntactic side of autonomous categories enriched over generalised metric spaces
• Quantitative equality in substructural logic via Lipschitz doctrines
• Graded differential categories and graded differential linear logic
• A complete \(\mathcal{V}\)-equational system for graded \(\lambda\)-calculus
• Relating structure and power: comonadic semantics for computational resources
• Non-linear communication via graded modal session types
• Logical foundations of quantitative equality
• Deriving distributive laws for graded linear types
• A core quantitative coeffect calculus
• A mixed linear and graded logic: proofs, terms, and models
• Back to futures
• Time warps, from algebra to algorithms

This page was built for publication: Combining effects and coeffects via grading

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985796)