Combining algebraic effect descriptions using the tensor of complete lattices

DOI10.1016/j.entcs.2020.09.013OpenAlexW3093940109WikidataQ113317292 ScholiaQ113317292MaRDI QIDQ2133480

Niels Voorneveld

Publication date: 29 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2020.09.013

zbMATH Keywords

probabilitycomplete latticeEilenberg-Moore algebratensor productnondeterminismalgebraic effectsquantitative logicprogram equivalenceapplicative bisimilarityglobal storetree monad

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generic weakest precondition semantics from monads enriched with order
• Tensorial decomposition of concept lattices
• Semantics of weakening and contraction
• Tensor products and relation quantales
• Semigroups in complete lattices. Quantales, modules and related topics
• Quantitative logics for equivalence of effectful programs
• A sound and complete logic for algebraic effects
• Behavioural equivalence via modalities for algebraic effects
• Combining effects: sum and tensor
• Cancellative medial means are arithmetic
• Observationally-induced algebras in Domain Theory
• Substitution, jumps, and algebraic effects
• Quantitative Algebraic Reasoning
• Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Dijkstra monads for free
• On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi
• Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions