Game Semantics for Higher-Order Concurrency

Abstract. We describe a denotational (game) semantics for a call-byvalue 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 . 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.

• Type: Conference
• Year: 2006
• Where: FSTTCS
• Authors: James Laird
• Keywords: Call-byvalue Functional Language, Closed Freyd Category, FSTTCS 2006, Natural Number Automorphisms, Software Engineering