Behavioural equivalence via modalities for algebraic effects

Simpson, Alex (author), Voorneveld, Niels (author)

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.

• Language: English
• Keywords: computer science, behavioural equivalence, call-by-value functional language, openness, decomposability
• Typology: 1.08 - Published Scientific Conference Contribution
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2018
• Number of pages: Str. 300-326
• PID: 20.500.12556/RUL-107596
• UDC: 004.43
• DOI: 10.1007/978-3-319-89884-1_11
• COBISS.SI-ID: 18420569
• Publication date in RUL: 29.04.2019

Record is a part of a monograph

• Title: Programming languages and systems : 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018
• Editors: Amal Ahmed
• Place of publishing: Cham
• Publisher: Springer
• ISBN: 978-3-319-89883-4
• COBISS.SI-ID: 18419801
• Collection title: Lecture notes in computer science
• Collection numbering: 10801
• Collection ISSN: 0302-9743

Projects

• Funder: EC - European Commission
• Funding programme: H2020
• Project number: 731143
• Name: Computing with Infinite Data
• Acronym: CID