Behavioural equivalence via modalities for algebraic effects
Simpson, Alex (Author), Voorneveld, Niels (Author)

.pdfPDF - Presentation file, Download (640,49 KB)
URLURL - Source URL, Visit https://doi.org/10.1007/978-3-319-89884-1_11 This link opens in a new window

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.

Keywords:computer science, behavioural equivalence, call-by-value functional language, openness, decomposability
Tipology:1.08 - Published Scientific Conference Contribution
Organization:FMF - Faculty of Mathematics and Physics
Number of pages:Str. 300-326
DOI:10.1007/978-3-319-89884-1_11 Link is opened in a new window
COBISS.SI-ID:18420569 Link is opened in a new window
Average score:(0 votes)
Your score:Voting is allowed only to logged in users.
AddThis uses cookies that require your consent. Edit consent...

Record is a part of a monograph

Title:Programming languages and systems
Subtitle: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
COBISS.SI-ID:18419801 This link opens in a new window
Collection title:Lecture notes in computer science
Collection numbering:10801
Collection ISSN:0302-9743
Place of publishing:Cham
Editors:Amal Ahmed

Document is financed by a project

Funder:EC - European Commission
Funding Programme:H2020
Project no.:731143
Name:Computing with Infinite Data

Similar documents

Similar works from RUL:
Similar works from other Slovenian collections:


Leave comment

You have to log in to leave a comment.

Comments (0)
0 - 0 / 0
There are no comments!