Akademska digitalna zbirka SLovenije - logo
ALL libraries (COBIB.SI union bibliographic/catalogue database)
PDF
  • Behavioural equivalence via modalities for algebraic effects
    Simpson, Alex ; Voorneveld, Niels, 1991-
    The article 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.
    Source: ACM transactions on programming languages and systems. - ISSN 0164-0925 (Vol. 42, iss. 1, Jan. 2020, art. 4 [45 str.])
    Type of material - article, component part ; adult, serious
    Publish date - 2020
    Language - english
    COBISS.SI-ID - 18937433