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

  • Extended Abstract (.pdf)<\li>
  • A slightly longer version (.pdf).<\li>
  • Slides from the conference presentation.
  • Bibtex entry:

    author = "J. Laird",
    title = "A Game Semantics of Higher-Order Concurrency",
    booktitle = "Proceedings of the 26th International Conference on Foundations of Software Technology and Computer Science (FSTTCS)",
    publisher = "Springer",
    series = "LNCS",
    number = 4337,
    pages = "17--428",
    year = 2006}