Skip to main content
SpringerLink
Log in

A Games Model of Bunched Implications

  • Conference paper
Computer Science Logic (CSL 2007)

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

Included in the following conference series:

  • 779 Accesses

Abstract

A game semantics of the ( − − *, →)-fragment of the logic of bunched implications, BI, is presented. To date, categorical models of BI have been restricted to two kinds: functor category models; and the category Cat itself. The game model is not of this kind. Rather, it is based on Hyland-Ong-Nickau-style games and embodies a careful analysis of the notions of resource sharing and separation inherent in BI. The key to distinguishing between the additive and multiplicative connectives of BI is a semantic notion of separation. The main result of the paper is that the model is fully complete: every finite, total strategy in the model is the denotation of a term of the αλ-calculus, the term language for the fragment of BI under consideration.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 162(2), 409–470 (2000)

    Article  MathSciNet  Google Scholar 

  2. Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In: Proceedings of 1996 Workshop on Linear Logic. Electronic notes in Theoretical Computer Science, vol. 3, Elsevier, Amsterdam (1996)

    Google Scholar 

  3. Atkey, R.: A λ-calculus for resource separation. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 158–170. Springer, Heidelberg (2004)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  5. Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  6. McCusker, G.: Games and Full Abstraction for a Functional Metalanguage with Recursive Types. Distinguished Dissertations in Computer Science. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  7. Nickau, H.: Hereditarily sequential functionals. In: Proceedings of the Symposium on Logical Foundations of Computer Science, Logic at St. Petersburg. Lecture notes in Computer Science, Springer, Heidelberg (1994)

    Google Scholar 

  8. O’Hearn, P.W.: Resource interpretations, bunched implications and the α − λ-calculus. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 258–279. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  10. O’Hearn, P.W.: On bunched typing. Journal of Functional Programming 13(4), 747–796 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  11. Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic, Dordrecht (2002), Errata available at http://www.cs.bath.ac.uk/~pym/BI-monograph-errata.pdf

    MATH  Google Scholar 

  12. Pym, D.J., Tofts, C.: Systems modelling via resources and processes: Philosophy, calculus, semantics, and logic. Electronic Notes in Theoretical Computer Science, vol. 172, pp. 545–587 (2007), Errata available at http://www.cs.bath.ac.uk/~pym/pym-tofts-fac-errata.pdf

  13. Reynolds, J.C.: Syntactic control of interference. In: Conf. Record 5th ACM Symposium on Principles of Programming Languages, pp. 39–46 (1978)

    Google Scholar 

  14. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002), IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  15. Wall, M.: Games for Syntactic Control of Interference. PhD thesis, University of Sussex (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Bath, Bath BA2 7AY, United Kingdom

    Guy McCusker

  2. Hewlett-Packard Laboratories, Bristol BS34 8QZ, United Kingdom

    David Pym

Authors
  1. Guy McCusker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Pym
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jacques Duparc Thomas A. Henzinger

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

McCusker, G., Pym, D. (2007). A Games Model of Bunched Implications. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74915-8_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74914-1

  • Online ISBN: 978-3-540-74915-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation