Behavioural equivalence via modalities for algebraic effects

DOI10.1007/978-3-319-89884-1_11zbMATH Open1418.68066arXiv1904.08843OpenAlexW2797640271MaRDI QIDQ2323978FDOQ2323978

Authors: Niels Voorneveld, Alex Simpson 

Publication date: 13 September 2019

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.

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

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

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)

Cited In (11)

• Runners for interleaving algebraic effects
• Streams of approximations, equivalence of recursive effectful programs
• Stable families of behavioural equivalences
• 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
• Title not available (Why is that?)
• Preorder-constrained simulations for program refinement with effects
• Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
• Title not available (Why is that?)
• Behavioural satisfaction and equivalence in concrete model categories

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)