20.500.12556/RUL-107596 Behavioural equivalence via modalities for algebraic effects 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. computer science behavioural equivalence call-by-value functional language openness decomposability true false false Angleški jezik Angleški jezik Neznano 2019-04-29 12:57:58 2019-04-29 12:58:01 2022-08-19 03:50:10 0000-00-00 00:00:00 2018 0 0 Str. 300-326 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 004.43 10.1007/978-3-319-89884-1_11 18420569 18419801 RAZ_Simpson_Alex_i2018.pdf RAZ_Simpson_Alex_i2018.pdf 1 7898B6C3504E5AE295FECC87D238B9FE 971b1752b72ed1672d12b95185d3361ab94ec7a2e559432abbb3e97bd14186a6 773eb1f3-a1b6-11eb-a523-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=118447 https://doi.org/10.1007/978-3-319-89884-1_11 1 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=118446 Fakulteta za matematiko in fiziko 0 0 0