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

Fingerprint

Game Semantics
Concurrency
Semantics
Higher Order
Asynchronous Communication
Denotational Semantics
Lambda Calculus
Natural number
Thread
Automorphisms
Correspondence
Game
Closed
Testing
Dependent
Communication
Interaction
Language
Model
Strategy

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Laird, J. (2006). Game semantics for higher-order concurrency. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science - 26th International Conference, Proceedings (pp. 417-428). (Lecture Notes in Computer Science; Vol. 4337 LNCS). Springer Verlag.

Game semantics for higher-order concurrency. / Laird, J.

FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science - 26th International Conference, Proceedings. Springer Verlag, 2006. p. 417-428 (Lecture Notes in Computer Science; Vol. 4337 LNCS).

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

Laird, J 2006, Game semantics for higher-order concurrency. in FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science - 26th International Conference, Proceedings. Lecture Notes in Computer Science, vol. 4337 LNCS, Springer Verlag, pp. 417-428, 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, Kolkata, India, 13/12/06.
Laird J. Game semantics for higher-order concurrency. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science - 26th International Conference, Proceedings. Springer Verlag. 2006. p. 417-428. (Lecture Notes in Computer Science).
Laird, J. / Game semantics for higher-order concurrency. FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science - 26th International Conference, Proceedings. Springer Verlag, 2006. pp. 417-428 (Lecture Notes in Computer Science).
@inproceedings{5be184e08c5747e98d8ecd5f7f5e405f,
title = "Game semantics for higher-order concurrency",
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.",
author = "J. Laird",
year = "2006",
month = "1",
day = "1",
language = "English",
isbn = "9783540499947",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "417--428",
booktitle = "FSTTCS 2006",
address = "Germany",

}

TY - GEN

T1 - Game semantics for higher-order concurrency

AU - Laird, J.

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80052145215&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783540499947

T3 - Lecture Notes in Computer Science

SP - 417

EP - 428

BT - FSTTCS 2006

PB - Springer Verlag

ER -