Game semantics for higher-order concurrency

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)

Abstract

We describe a denotational (game) semantics for a call-by-value functional language with multiple threads of control, which may communicate values of general type on locally declared channels. This develops previous work which interpreted freshly generated names in a category of games acted upon by the group of natural number automorphisms, by showing how names may be associated with “dependent arenas” in which interaction between strategies, corresponding to asynchronous communication on named channels, may occur. We describe a model of the call-by-value λ-calculus (a closed Freyd category) based on these arenas, and use this as the basis for interpreting our language. We prove that the semantics is fully abstract with respect to may-testing using a correspondence between channel and function types based on the “triggering” representation of procedure-passing in terms of name-passing.

Original languageEnglish
Title of host publicationFSTTCS 2006
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 26th International Conference, Proceedings
PublisherSpringer Verlag
Pages417-428
Number of pages12
ISBN (Print)9783540499947
Publication statusPublished - 1 Jan 2006
Event26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006 - Kolkata, India
Duration: 13 Dec 200615 Dec 2006

Publication series

NameLecture Notes in Computer Science
Volume4337 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006
CountryIndia
CityKolkata
Period13/12/0615/12/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Game semantics for higher-order concurrency'. Together they form a unique fingerprint.

Cite this