License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2018.21
URN: urn:nbn:de:0030-drops-92267
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9226/
Go to the corresponding LIPIcs Volume Portal

Ancona, Davide ; Dagnino, Francesco ; Zucca, Elena

Modeling Infinite Behaviour by Corules

pdf-format:
LIPIcs-ECOOP-2018-21.pdf (0.8 MB)

Abstract

Generalized inference systems have been recently introduced, and used, among other applications, to define semantic judgments which uniformly model terminating computations and divergence. We show that the approach can be successfully extended to more sophisticated notions of infinite behaviour, that is, to express that a diverging computation produces some possibly infinite result. This also provides a motivation to smoothly extend the theory of generalized inference systems to include, besides coaxioms, also corules, a more general notion for which significant examples were missing until now. We first illustrate the approach on a lambda-calculus with output effects, for which we also provide an alternative semantics based on standard notions, and a complete proof of the equivalence of the two semantics. Then, we consider a more involved example, that is, an imperative Java-like language with I/O primitives.

BibTeX - Entry

@InProceedings{ancona_et_al:LIPIcs:2018:9226,
  author =	{Davide Ancona and Francesco Dagnino and Elena Zucca},
  title =	{{Modeling Infinite Behaviour by Corules}},
  booktitle =	{32nd European Conference on Object-Oriented Programming  (ECOOP 2018)},
  pages =	{21:1--21:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Todd Millstein},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9226},
  URN =		{urn:nbn:de:0030-drops-92267},
  doi =		{10.4230/LIPIcs.ECOOP.2018.21},
  annote =	{Keywords: Operational semantics, coinduction, trace semantics}
}

Keywords: Operational semantics, coinduction, trace semantics
Collection: 32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Issue Date: 2018
Date of publication: 10.07.2018

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