Skip to main content
SpringerLink
Log in

Algorithmic Game Semantics

A Tutorial Introduction

  • Chapter
Proof and System-Reliability

Part of the book series: NATO Science Series ((NAII,volume 62))

Abstract

Game Semantics has emerged as a powerful paradigm for giving semantics to a variety of programming languages and logical systems. It has been used to construct the first syntax-independent fully abstract models for a spectrum of programming languages ranging from purely functional languages to languages with non-functional features such as control operators and locally-scoped references [4, 21, 5, 19, 2, 22, 17, 11]. A substantial survey of the state of the art of Game Semantics circa 1997 was given in a previous Marktoberdorf volume [6].

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky: Semantics of interaction: an introduction to game semantics. In Semantics and Logics of Computation, pages 1–32. Cambridge Univ. Press, 1997.

    Chapter  Google Scholar 

  2. S. Abramsky, K. Honda, and G. McCusker. Fully abstract game semantics for general references. In Proceedings of IEEE Symposium on Logic in Computer Science, 1998, pages 334–344. Computer Society Press, 1998.

    Google Scholar 

  3. S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symb. Logic, 59:543–574, 1994.

    Article  MathSciNet  MATH  Google Scholar 

  4. S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163:409–470, 2000.

    Article  MathSciNet  MATH  Google Scholar 

  5. S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In P. W. O’Hearn and R. D. Tennent, editors, Algol-like languages, pages 297–330. Birkhaüser, 1997.

    Google Scholar 

  6. S. Abramsky and G. McCusker. Call-by-value games. In Proceedings of CSL ’97, number 1414 in Lecture Notes in Computer Science, pages 1–17. Springer-Verlag, 1998.

    Google Scholar 

  7. S. Abramsky and G. McCusker. Game semantics. In H. Schwichtenberg and U. Berger, editors, Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School, pages 1–56. Springer-Verlag, 1998.

    Google Scholar 

  8. T. Ball and S. K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, MicroSoft Research, 2000.

    Google Scholar 

  9. J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971.

    MATH  Google Scholar 

  10. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of 4th ACM Symp. POPL, pages 238–252, 1977.

    Google Scholar 

  11. V. Danos and R. Harmer. Probabilistic game semantics. In Proc. IEEE Symposium on Logic in Computer Science, Santa Barbara, June, 2000. Computer Science Society, 2000.

    Google Scholar 

  12. J. Corbett et al. Bandera: Extracting finite-state models from java source code. In Proceedings of the 2000 International Conference on Software Engineering, 2000.

    Google Scholar 

  13. D. R. Ghica. A regular-language model for Hoare-style correctness statements. In Proc. 2nd Int. Workshop on Verification and Computational Logic VCL’2001, Florence, Italy, 2001. www.cs.queensu.ca/home/ghica/.

    Google Scholar 

  14. D. R. Ghica. Regular language semantics for a call-by-value programming language. In Proc. 17th Conf. Mathematical Foundations of Programming Semantics, Aarhus, Denmark, 2001. www.es . queensu. ca/home/ghica/.

    Google Scholar 

  15. D. R. Ghica and G. McCusker. Reasoning about Idealized Algol using regular languages. In Proceedings of 27th International Colloquium on Automata, Languages and Programming ICALP 2000, pages 103–116. Springer-Verlag, 2000. LNCS Vol. 1853.

    Google Scholar 

  16. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989. Cambridge Tracts in Theoretical Computer Science 7.

    MATH  Google Scholar 

  17. R. Harmer and G. McCusker. A fully abstract game semantics for finite nondeterminism. In Proceedings of Fourteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999.

    Google Scholar 

  18. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    MATH  Google Scholar 

  19. K. Honda and N. Yoshida. Game-theoretic analysis of call-by-value computation (extended abstract). In Proc. of ICALP’97, Borogna, Italy, July, 1997, LNCS. Springer-Verlag, 1997.

    Google Scholar 

  20. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.

    MATH  Google Scholar 

  21. J. M. E. Hyland and C.-H. L. Ong. On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Information and Computation, 163:285–408, 2000.

    Article  MathSciNet  MATH  Google Scholar 

  22. J. Laird. A semantic analysis of control. PhD thesis, University of Edinburgh, 1998.

    Google Scholar 

  23. R. Lazic and D. Nowak. A unifying approach to data-independence. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000). Springer-Verlag, 2000. LNCS.

    Google Scholar 

  24. R. S. Lazic, T. C. Newcomb, and A. W. Roscoe. On model checking data-independent systems with arrays without reset (abstract). In Proceedings of VCL 2001, 2001.

    Google Scholar 

  25. P. Malacaria and C. Hankin. Non-deterministic games and program analysis: an application to security. In Proceedings of 14th Annual IEEE Symp. Logic in Computer Science, pages 443–452. IEEE Computer Society, 1999.

    Google Scholar 

  26. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    MATH  Google Scholar 

  27. P. W. O’Hearn and R. D. Tennent. Algol-like Languages: Volumes I and II. Birkhäuser, 1997. Progress in Theoretical Computer Science.

    Google Scholar 

  28. C.-H. L. Ong. Equivalence of third order Idealized Algol is decidable. Technical report, Oxford University Computing Laboratory, 2001. In preparation.

    Google Scholar 

  29. T. Reps, S. Horowitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proc. ACM Symp. POPL, pages 49–61, 1995.

    Google Scholar 

  30. J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372. North Holland, 1978.

    Google Scholar 

  31. D. A. Schmidt. On the need for a popular formal semantics. ACM SIGPLAN Notices, 32:115–116, 1997.

    Article  MATH  Google Scholar 

  32. J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, 1979. The MIT Press Series in Computer Science.

    Google Scholar 

  33. C. Strachey. Fundamental concepts in programming languages. Lecture notes for the International Summer School in Computer Programming, Copenhagen, 1967.

    Google Scholar 

  34. R. D. Tennent. Denotational semantics. In S. Abramsky et al, editor, Handbook of Logic in Computer Science, pages 169–322. Oxford University Press, 1994.

    Google Scholar 

  35. G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. Foundations of Computing Series.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, UK

    Samson Abramsky

Authors
  1. Samson Abramsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematisches Institut, Ludwig-Maximilians-Universität, München, Germany

    Helmut Schwichtenberg

  2. Institut für Informatik, Technische Universität, München, Germany

    Ralf Steinbrüggen

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Abramsky, S. (2002). Algorithmic Game Semantics. In: Schwichtenberg, H., Steinbrüggen, R. (eds) Proof and System-Reliability. NATO Science Series, vol 62. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-0413-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-94-010-0413-8_2

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-0608-1

  • Online ISBN: 978-94-010-0413-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation