Alex Simpson (Avtor), Niels Voorneveld (Avtor)

Povzetek

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.

Ključne besede

computer science;behavioural equivalence;call-by-value functional language;openness;decomposability;

Podatki

Jezik: Angleški jezik
Leto izida:
Tipologija: 1.08 - Objavljeni znanstveni prispevek na konferenci
Organizacija: UL FMF - Fakulteta za matematiko in fiziko
UDK: 004.43
COBISS: 18420569 Povezava se bo odprla v novem oknu
Št. ogledov: 741
Št. prenosov: 569
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Strani: Str. 300-326
DOI: 10.1007/978-3-319-89884-1_11
ID: 11124613