Behavioural equivalence via modalities for algebraic effects

DOI10.1007/978-3-319-89884-1_11MaRDI QIDQ2323978zbMATH OpenOpenAlexFDO

Authors Niels Voorneveld, Alex Simpson

Publication date 13 September 2019

Full work available at URL https://arxiv.org/abs/1904.08843, https://repozitorij.uni-lj.si/Dokument.php?id=118446&dn=

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Abstract: The paper investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability, are satisfied by the modalities then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe's method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store and input/output.

Recommendations

• scientific article; zbMATH DE number 3852428
• A sound and complete logic for algebraic effects
• Recent Trends in Algebraic Development Techniques
• Behavioral algebraization of logics
• Behavioral equivalence of hidden k-logics: an abstract algebraic approach
• Modal Logic and Equality for Process Algebra
• Representations of effect algebras
• Behaviour algebras
• The logic induced by effect algebras
• Compatibility support mappings in effect algebras

Cited in

(12)

• scientific article; zbMATH DE number 7453165 (Why is no real title available?)
• Runners for interleaving algebraic effects
• Streams of approximations, equivalence of recursive effectful programs
• On bisimilarity in lambda calculi with continuous probabilistic choice
• Combining algebraic effect descriptions using the tensor of complete lattices
• Quantitative logics for equivalence of effectful programs
• A sound and complete logic for algebraic effects
• Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
• Stable families of behavioural equivalences
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Behavioural satisfaction and equivalence in concrete model categories
• Preorder-constrained simulations for program refinement with effects

This page was built for publication: Behavioural equivalence via modalities for algebraic effects

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