Coinductive Big-Step Semantics for Concurrency

Tarmo Uustalu

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.

In Nobuko Yoshida and Wim Vanderbauwhede: Proceedings 5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2013), Rome, Italy, 23rd March 2013, Electronic Proceedings in Theoretical Computer Science 137, pp. 63–78.
Published: 8th December 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: