Behavioural equivalence via modalities for algebraic effects

Simpson, Alex (avtor), Voorneveld, Niels (avtor)

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.

• Jezik: Angleški jezik
• Ključne besede: computer science, behavioural equivalence, call-by-value functional language, openness, decomposability
• Tipologija: 1.08 - Objavljeni znanstveni prispevek na konferenci
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2018
• Št. strani: Str. 300-326
• PID: 20.500.12556/RUL-107596
• UDK: 004.43
• DOI: 10.1007/978-3-319-89884-1_11
• COBISS.SI-ID: 18420569
• Datum objave v RUL: 29.04.2019

Gradivo je del monografije

• Naslov: 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
• Uredniki: Amal Ahmed
• Kraj izida: Cham
• Založnik: Springer
• ISBN: 978-3-319-89883-4
• COBISS.SI-ID: 18419801
• Naslov zbirke: Lecture notes in computer science
• Številčenje v zbirki: 10801
• ISSN zbirke: 0302-9743

Projekti

• Financer: EC - European Commission
• Program financ.: H2020
• Številka projekta: 731143
• Naslov: Computing with Infinite Data
• Akronim: CID