Skip to main content
SpringerLink
Log in

Intensionality, Definability and Computation

  • Chapter
  • First Online:
Johan van Benthem on Logic and Information Dynamics

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 5))

Abstract

We look at intensionality from the perspective of computation. In particular, we review how game semantics has been used to characterize the sequential functional processes, leading to powerful and flexible methods for constructing fully abstract models of programming languages, with applications in program analysis and verification. In a broader context, we can regard game semantics as a first step towards developing a positive theory of intensional structures with a robust mathematical structure, and finding the right notions of invariance for these structures.

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 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    See e.g. https://sites.google.com/site/galopws/ for a workshop series devoted to this topic.

  2. 2.

    Cf. Henry James on the Russian masters.

  3. 3.

    This argument is due to Gordon Plotkin (personal communication).

References

  1. Abramsky S (1997) Semantics of interaction: an introduction to game semantics. In: Dybjer P, Pitts A (eds) Semantics and logics of computation. Publications of the Newton Institute, Cambridge University Press, pp 1–31

    Google Scholar 

  2. Abramsky S (1999) Axioms for definability and full completeness. In: Plotkin G, Tofte M, Stirling C (eds) Proof, language and interaction: essays in honour of Robin Milner. MIT Press, Cambridge, pp 55–75

    Google Scholar 

  3. Abramsky S (2001) Algorithmic game semantics. In: Schwichtenberg H, Steinbrüggen R (eds) Proof and system-reliability: proceedings of the NATO advanced study institute. Kluwer Academic Publishers, Marktoberdorf, pp 21–47 (24 July–5 Aug 2001)

    Google Scholar 

  4. Abramsky S (2006) What are the fundamental structures of concurrency?: we still don’t know!. Electron Notes Theoret Comput Sci 162:37–41

    Article  Google Scholar 

  5. Abramsky S (2007) Temperley-Lieb algebra: from knot theory to logic and computation via quantum mechanics. In: Chen G, Kauffman L, Lomonaco S (eds) Mathematics of quantum computing and technology, Taylor and Francis, New York, pp 415–458

    Google Scholar 

  6. Abramsky S, Ghica DR, Murawski AS, Ong CHL, Stark IDB (2004) Nominal games and full abstraction for the nu-calculus. In: Proceedings of the 19th annual IEEE symposium on logic in computer science, pp 150–159

    Google Scholar 

  7. Abramsky S, Ghica DR, Murawski AS, Ong CHL (2003) Algorithmic game semantics and component-based verification. In: SAVCBS 2003, specification and verification of component-based systems, p 66

    Google Scholar 

  8. Abramsky S, Ghica D, Murawski A, Ong CHL (2004) Applying game semantics to compositional software modeling and verification. In: Conference on tools and algorithms for the construction and analysis of systems. Lecture Notes in Computer Science, vol 2988. Springer, pp 421–435

    Google Scholar 

  9. Abramsky S, Honda K, McCusker G (1998) A fully abstract game semantics for general references. In: Proceedings of 13th annual IEEE symposium on logic in computer science, pp 334–344

    Google Scholar 

  10. Abramsky S, Jagadeesan R (1994) Games and full completeness for multiplicative linear logic. J Symb Log 59(2):543–574

    Article  Google Scholar 

  11. Abramsky S, Jagadeesan R, Malacaria P (2000) Full abstraction for PCF. Inf Comput 163(2):409–470

    Article  Google Scholar 

  12. Abramsky S, McCusker G (1997) Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. In: O’Hearn P, Tennent RD (eds) Algol-like languages, Birkhauser, pp 317–348

    Google Scholar 

  13. Abramsky S, McCusker G (1998) Call-by-value games. In: Proceedings of computer science logic, Springer, pp 1–17

    Google Scholar 

  14. Abramsky S, McCusker G (1999) Game semantics. In: Schwichtenberg H, Berger U (eds) Computational logic: proceedings of the 1997 Marktoberdorf summer school, Springer, pp 1–55

    Google Scholar 

  15. Abramsky S, Mellies PA (1999) Concurrent games and full completeness. In: Proceedings of 14th symposium on logic in computer science, pp 431–442

    Google Scholar 

  16. Awodey S, Warren MA (2009) Homotopy theoretic models of identity types. Math Proc Camb Phil Soc 146(1):45–55

    Article  Google Scholar 

  17. Barendregt HP (1984) The lambda calculus: its syntax and semantics, vol 103. Studies in Logic and the Foundations of Mathematics, North Holland

    Google Scholar 

  18. Berry G, Curien PL (1982) Sequential algorithms on concrete data structures. Theoret Comput Sci 20(3):265–321

    Article  Google Scholar 

  19. Church A (1941) The calculi of lambda-conversion, vol 6. Princeton University Press, Princeton

    Google Scholar 

  20. Curien PL, Faggian C (2012) An approach to innocent strategies as graphs. Inf Comput 214:119–155

    Article  Google Scholar 

  21. Cutland N (1980) Computability: an introduction to recursive function theory. Cambridge University Press, Cambridge

    Google Scholar 

  22. Danos V, Harmer RS (2002) Probabilistic game semantics. ACM Trans Comput Log 3(3):359–382

    Article  Google Scholar 

  23. Gandy R (1980) Church’s thesis and principles for mechanisms. In: Barwise J, Keisler HJ, Kunen K (eds) The kleene symposium of studies in logic and the foundations of mathematics, vol 101. Elsevier, Amsterdam, pp 123–148

    Google Scholar 

  24. Ghica DR (2009) Applications of game semantics: from program analysis to hardware synthesis. In: Proceedings of 24th Annual IEEE Symposium on logic in computer science, pp 17–26

    Google Scholar 

  25. Ghica DR, McCusker G (2003) The regular-language semantics of second-order idealized ALGOL. Theoret Comput Sci 309(1):469–502

    Article  Google Scholar 

  26. Ghica DR, Murawski AS (2008) Angelic semantics of fine-grained concurrency. Ann Pure Appl Log 151(2):89–114

    Article  Google Scholar 

  27. Gunter CA (1992) Semantics of programming languages: structures and techniques. MIT press, Cambridge

    Google Scholar 

  28. Harmer R, Hyland H, Mellies PA (2007) Categorical combinatorics for innocent strategies. In: 22nd annual IEEE symposium on logic in computer science, pp 379–388

    Google Scholar 

  29. Harmer R, McCusker G (1999) A fully abstract game semantics for finite nondeterminism. In: 14th annual IEEE symposium on logic in computer science, pp 422–430

    Google Scholar 

  30. Hintikka J, Sandu G (1997) Game-theoretical semantics. In: van Benthem J, ter Meulen A (eds) Handbook of logic and language, Elsevier, Amsterdam, pp 361–410

    Google Scholar 

  31. Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666–677

    Article  Google Scholar 

  32. Honda K, Yoshida N (1997) Game theoretic analysis of call-by-value computation: automata, languages and programming, Springer, Berlin, pp 225–236

    Google Scholar 

  33. Hopcroft JE, Ullman JD (1979) Introduction to automata theory, languages, and computation. Addison-Wesley, Cambridge

    Google Scholar 

  34. Hughes J (1989) Why functional programming matters. Comput J 32(2):98–107

    Article  Google Scholar 

  35. Hyland JME, Ong CHL (2000) On full abstraction for PCF: I, II, and III. Inf Comput 163(2):285–408

    Article  Google Scholar 

  36. Kleene SC (1938) On notation for ordinal numbers. J Symb Log 3(4):150–155

    Article  Google Scholar 

  37. Kleene SC (1978) Recursive functionals and quantifiers of finite types revisited I. In: Fenstad JE, Gandy RO, Sacks GE (eds) Generalized recursion theory II: proceedings of the 1977 Oslo symposium of studies in logic and the foundations of mathematics, vol 94. Amsterdam, pp 185–222

    Google Scholar 

  38. Kleene SC (1980) Recursive functionals and quantifiers of finite types revisited II. In: Barwise J, Keisler HJ, Kunen K (eds) The Kleene symposium of studies in logic and the foundations of mathematics, vol 101. Elsevier, pp 1–29

    Google Scholar 

  39. Kleene SC (1982) Recursive functionals and quantifiers of finite types revisited III. In: Metakides G (ed) Patras logic symposion: proceedings of studies in logic and the foundations of mathematics, logic symposion held at Patras, Greece, vol 109. Elsevier, pp 1–40, Aug 18–22 1982

    Google Scholar 

  40. Kleene SC (1985) Unimonotone functions of finite types (recursive functionals and quantifiers of finite types revisited IV). Recur Theory 42:119–138

    Article  Google Scholar 

  41. Kleene SC (1991) Recursive functionals and quantifiers of finite types revisited V. Trans Am Math Soc 325:593–630

    Google Scholar 

  42. Kripke S (1965) Semantical analysis of intuitionistic logic I. In: Formal systems and recursive functions, studies in logic and foundations of mathematics, North Holland, pp 92–130

    Google Scholar 

  43. Laird J (2001) A game semantics of idealized CSP. Electron Notes Theor Comput Sci 45:232–257

    Article  Google Scholar 

  44. Laird J (2001) A fully abstract game semantics of local exceptions. In: 16th annual IEEE symposium on logic in computer science, pp 105–114

    Google Scholar 

  45. Laird J (2003) A game semantics of linearly used continuations. In: Foundations of software science and computation structures, Springer, pp 313–327

    Google Scholar 

  46. Laird J (2005) A game semantics of the asynchronous \(\pi \)-calculus. CONCUR 2005-concurrency theory, pp 51–65

    Google Scholar 

  47. Landin PJ (1966) The next 700 programming languages. Commun ACM 9(3):157–166

    Article  Google Scholar 

  48. Legay A, Murawski A, Ouaknine J, Worrell J (2008) On automated verification of probabilistic programs: tools and algorithms for the construction and analysis of Systems, pp 173–187

    Google Scholar 

  49. Lassez JL, Nguyen VL, Sonenberg E (1982) Fixed point theorems and semantics: a folk tale. Inf Process Lett 14(3):112–116

    Article  Google Scholar 

  50. Loader R (2001) Finitary PCF is not decidable. Theor Comput Sci 266(1):341–364

    Article  Google Scholar 

  51. Lorenzen P (1960) Logik und agon. Atti Congr Int di Filosofia 4:187–194

    Google Scholar 

  52. Melliès PA (2006) Asynchronous games 2: the true concurrency of innocence. Theor Comput Sci 358(2):200–228

    Article  Google Scholar 

  53. Mellies PA (2012) Game semantics in string diagrams. In: 27th annual IEEE symposium on logic in computer science, pp 481–490

    Google Scholar 

  54. Milner R (1977) Fully abstract models of typed \(\lambda \)-calculi. Theor Comput Sci 4(1):1–22

    Article  Google Scholar 

  55. Milner R (1989) Communication and concurrency. Prentice-Hall, Upper Saddle River

    Google Scholar 

  56. Milner R (1999) Communicating and mobile systems: the pi calculus. Cambridge University Press, Cambridge

    Google Scholar 

  57. Moschovakis YN (2010) Kleene’s amazing second recursion theorem. Bull Symb Log 16(2):189–239

    Article  Google Scholar 

  58. Murawski A, Tzevelekos T (2009) Full abstraction for reduced ML: foundations of software science and computational structures, pp 32–47

    Google Scholar 

  59. Murawski A, Tzevelekos T (2011) Algorithmic nominal game semantics. In: Proceedings of the 20th European symposium on programming, Lecture Notes in Computer Science, vol 6602. Springer, pp 419–438

    Google Scholar 

  60. Murawski AS, Tzevelekos N (2011) Game semantics for good general references. In: 26th annual IEEE symposium on logic in computer science, pp 75–84

    Google Scholar 

  61. Murawski AS, Tzevelekos N (2012) Algorithmic games for full ground references. In: Proceedings of the 39th international colloquium on automata, languages and programming, Lecture Notes in Computer Science, vol 7392. pp 312–324

    Google Scholar 

  62. Myhill J, Shepherdson JC (1955) Effective operations on partial recursive functions. Math Log Quart 1(4):310–317

    Article  Google Scholar 

  63. Myhill JR (1957) Finite automata and the representation of events. Technical Report WADD TR-57-624, Wright Patterson AFB

    Google Scholar 

  64. Nerode A (1958) Linear automaton transformations. Proc Am Math Soc 9(4):541–544

    Article  Google Scholar 

  65. Petri CA (1962) Fundamentals of a theory of asynchronous information flow. In: IFIP Congress 1962, Amsterdam, pp 386–390

    Google Scholar 

  66. Petri CA (1966) Communication with automata, New York: Griffiss Air Force Base. vol. 1, suppl. no. 1. Tech Rep RADC-TR-65-377

    Google Scholar 

  67. Plotkin GD (1977) LCF considered as a programming language. Theor Comput Sci 5(3):223–255

    Article  Google Scholar 

  68. Rogers H (1967) Theory of recursive functions and effective computability. McGraw Hill, New York

    Google Scholar 

  69. Sieg W (2002) Calculations by man and machine: mathematical presentation. In: Gärdenfors P, Wolenski J, Kijania-Placek K (eds) Proceedings of the 11th international conference on logic, methodology and philsophy of science, Vol 1. Kluwer Academic Publishers, pp 247–262

    Google Scholar 

  70. Turing AM (1937) On computable numbers, with an application to the entscheidungs problem. Proc Lond Math Soc 42(2):230–265

    Article  Google Scholar 

  71. Turner D (1995) Elementary strong functional programming. In: Functional programming languages in education, Springer, pp 1–13

    Google Scholar 

  72. Tzevelekos N (2007) Full abstraction for nominal general references. In: 22nd annual IEEE symposium on logic in computer science, pp 399–410

    Google Scholar 

  73. Voevodsky V (2010) Univalent foundations project, NSF grant application

    Google Scholar 

  74. Wadler P (1992) The essence of functional programming. In: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 1–14

    Google Scholar 

  75. Winskel G (1987) Event structures. In: Brauer W, Reisig W, Rozenberg G (eds) Proceedings of an advanced course on Petri nets: Applications and relationships to other models of concurrency, advances in Petri nets 1986, Part II, LNCS, Bad Honnef, September 1986, vol 255. Springer, pp 325–392

    Google Scholar 

  76. Winskel G (1993) The formal semantics of programming languages: an introduction. MIT press, Cambridge

    Google Scholar 

  77. Winskel G (2012) Bicategories of concurrent games. In Foundations of Software Science and Computational Structures, Springer Berlin Heidelberg, pp 26–41

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Samson Abramsky

Authors
  1. Samson Abramsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Samson Abramsky .

Editor information

Editors and Affiliations

  1. University of Amsterdam Inst Logic,Language & Computation, Amsterdam, The Netherlands

    Alexandru Baltag

  2. Amsterdam, The Netherlands

    Sonja Smets

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Abramsky, S. (2014). Intensionality, Definability and Computation. In: Baltag, A., Smets, S. (eds) Johan van Benthem on Logic and Information Dynamics. Outstanding Contributions to Logic, vol 5. Springer, Cham. https://doi.org/10.1007/978-3-319-06025-5_5

Download citation

Publish with us

Policies and ethics

Search

Navigation