Coinductive Big-Step Semantics for Concurrency

Coinductive Big-Step Semantics for Concurrency

In a paper presented at SOS 2010, we developed a framework for big-step semantics for interactive input-output in combination with divergence, based on coinductive and mixed inductive-coinductive notions of resumptions, evaluation and termination-sensitive weak bisimilarity. In contrast to standard...

Full description

Bibliographic Details
Main Author: Tarmo Uustalu
Format: Article
Language:English
Published: Open Publishing Association 2013-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1312.2702v1
id doaj-254cc43eb0914c44a24c47582c230743
record_format Article
spelling doaj-254cc43eb0914c44a24c47582c2307432020-11-25T01:56:37ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-12-01137Proc. PLACES 2013637810.4204/EPTCS.137.6:18Coinductive Big-Step Semantics for ConcurrencyTarmo UustaluIn a paper presented at SOS 2010, we developed a framework for big-step semantics for interactive input-output in combination with divergence, based on coinductive and mixed inductive-coinductive notions of resumptions, evaluation and termination-sensitive weak bisimilarity. In contrast to standard inductively defined big-step semantics, this framework handles divergence properly; in particular, runs that produce some observable effects and then diverge, are not "lost". Here we scale this approach for shared-variable concurrency on a simple example language. We develop the metatheory of our semantics in a constructive logic.http://arxiv.org/pdf/1312.2702v1
collection DOAJ
language English
format Article
sources DOAJ
author Tarmo Uustalu
spellingShingle Tarmo Uustalu
Coinductive Big-Step Semantics for Concurrency
Electronic Proceedings in Theoretical Computer Science
author_facet Tarmo Uustalu
author_sort Tarmo Uustalu
title Coinductive Big-Step Semantics for Concurrency
title_short Coinductive Big-Step Semantics for Concurrency
title_full Coinductive Big-Step Semantics for Concurrency
title_fullStr Coinductive Big-Step Semantics for Concurrency
title_full_unstemmed Coinductive Big-Step Semantics for Concurrency
title_sort coinductive big-step semantics for concurrency
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2013-12-01
description In a paper presented at SOS 2010, we developed a framework for big-step semantics for interactive input-output in combination with divergence, based on coinductive and mixed inductive-coinductive notions of resumptions, evaluation and termination-sensitive weak bisimilarity. In contrast to standard inductively defined big-step semantics, this framework handles divergence properly; in particular, runs that produce some observable effects and then diverge, are not "lost". Here we scale this approach for shared-variable concurrency on a simple example language. We develop the metatheory of our semantics in a constructive logic.
url http://arxiv.org/pdf/1312.2702v1
work_keys_str_mv AT tarmouustalu coinductivebigstepsemanticsforconcurrency
_version_ 1724979008226983936

Similar Items