Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs - Archive ouverte HAL Access content directly
Conference Papers Year :

Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs

(1, 2) , (1, 2)
1
2

Abstract

We investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.
Fichier principal
Vignette du fichier
main.pdf (606.38 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03520742 , version 1 (11-01-2022)

Identifiers

  • HAL Id : hal-03520742 , version 1

Cite

Ugo Dal Lago, Francesco Gavazzo. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires, Argentina. ⟨hal-03520742⟩
12 View
71 Download

Share

Gmail Facebook Twitter LinkedIn More