Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 2006: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science pp 417–428Cite as

Game Semantics for Higher-Order Concurrency

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4337))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ferreira, W., Hennessy, M., Jeffrey, A.S.A.: A theory of weak bisimulation for core CML. J. Functional Programming 8(5), 447–491 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  2. Ghica, D., McCusker, G.: The regular language semantics of second-order Idealised Algol. Theoretical Computer Science 309, 469–502 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  3. Ghica, D.R., Murawski, A.S.: Angelic semantics of fine-grained concurrency. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 211–225. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Harmer, R., McCusker, G.: A fully abstract games semantics for finite non-determinism. In: Proceedings of LICS 1999. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  5. Honda, K., Yoshida, N.: Game theoretic analysis of call-by-value computation. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256. Springer, Heidelberg (1997)

    Google Scholar 

  6. Hughes, D.: Games and definability for System F. In: Proceedings of LICS 1997. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  7. Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II and III. Information and Computation 163, 285–408 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  8. Jeffrey, A.S.A., Rathke, J.: Contextual equivalence for higher-order pi-calculus revisited. Logical Methods in Computer Science 1(1:4) (2002)

    Google Scholar 

  9. Jeffrey, A.S.A., Rathke, J.: A fully abstract testing semantics for concurrent objects. In: Proceedings of LICS 2002, pp. 101–112 (2002)

    Google Scholar 

  10. Laird, J.: A game semantics of ICSP. In: Proceedings of MFPS XVII. Electronic notes in Theoretical Computer Science, vol. 45. Elsevier, Amsterdam (2001)

    Google Scholar 

  11. Laird, J.: A game semantics of names and pointers. Annals of Pure and Applied Logic (to appear, 2005), Available from: http://www.cogs.susx.ac.uk/users/jiml

  12. Laird, J.: A game semantics of the asynchronous p-calculus. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 51–65. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Laurent, O.: Polarized games. In: Proceedings of LICS 2002 (2002)

    Google Scholar 

  14. Malacaria, P., Hankin, C.: Generalised flowcharts and games. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 363. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  15. McCusker, G.: Games and full abstraction for a functional metalanguage with recursive types. PhD thesis, Imperial College London (1996)

    Google Scholar 

  16. Power, J., Robinson, E.: Premonoidal categories and notions of computation. Mathematical Structures in Computer Science (1997)

    Google Scholar 

  17. Reppy, J.: CML: A higher-order concurrent language. In: Proceedings of PLDI 1991, pp. 293–305. ACM Press, New York (1991)

    Google Scholar 

  18. Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, University of Sussex, UK

    J. Laird

Authors
  1. J. Laird
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology Delhi, P.O. Box, 110016, New Delhi, India

    S. Arun-Kumar

  2. Indian Institute of Technology, Delhi

    Naveen Garg

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Laird, J. (2006). Game Semantics for Higher-Order Concurrency. In: Arun-Kumar, S., Garg, N. (eds) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2006. Lecture Notes in Computer Science, vol 4337. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11944836_38

Download citation

  • DOI: https://doi.org/10.1007/11944836_38

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-49994-7

  • Online ISBN: 978-3-540-49995-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation