License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.23
URN: urn:nbn:de:0030-drops-142618
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14261/
Go to the corresponding LIPIcs Volume Portal

Dal Lago, Ugo ; Gavazzo, Francesco

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

pdf-format:
LIPIcs-FSCD-2021-23.pdf (0.9 MB)

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.

BibTeX - Entry

@InProceedings{dallago_et_al:LIPIcs.FSCD.2021.23,
  author =	{Dal Lago, Ugo and Gavazzo, Francesco},
  title =	{{Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14261},
  URN =		{urn:nbn:de:0030-drops-142618},
  doi =		{10.4230/LIPIcs.FSCD.2021.23},
  annote =	{Keywords: algebraic effects, linearity, program equivalence, full abstraction}
}

Keywords: algebraic effects, linearity, program equivalence, full abstraction
Collection: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Issue Date: 2021
Date of publication: 06.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI