Skip to main content
SpringerLink
Log in

Interpreting Localized Computational Effects Using Operators of Higher Type

  • Conference paper
Logic and Theory of Algorithms (CiE 2008)

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

Included in the following conference series:

  • 1032 Accesses

Abstract

We outline a general approach to providing intensional models for languages with computational effects, whereby the problem of interpreting a given effect reduces to that of finding an operator of higher type satisfying certain equations. Our treatment consolidates and generalizes an idea that is already implicit in the literature on game semantics. As an example, we work out our approach in detail for the case of fresh name generation, and discuss some particular models to which it applies.

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.: Semantics of interaction: an introduction to game semantics. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, CUP, pp. 1–31 (1997)

    Google Scholar 

  2. Abramsky, S., Ghica, D., Murawski, A., Ong, C.-H., Stark, I.: Nominal games and full abstraction for the nu-Calculus. In: Proc. 19th LICS, pp. 150–159. IEEE Press, Los Alamitos (2004)

    Google Scholar 

  3. Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Proc. 13th LICS, pp. 334–344. IEEE Press, Los Alamitos (1998)

    Google Scholar 

  4. Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  5. Abramsky, S., McCusker, G.: Game semantics. In: Proc. 1997 Marktoberdorf Summer School, pp. 1–56. Springer, Heidelberg (1999)

    Google Scholar 

  6. Abramsky, S., McCusker, G.: Full Abstraction for Idealized Algol with passive expressions. Theor. Comp. Sci. 227, 3–42 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  7. Amadio, R.M., Curien, P.-L.: Domains and Lambda-Calculi, CUP (1998)

    Google Scholar 

  8. Berry, G., Curien, P.-L.: Sequential algorithms on concrete data structures. Theor. Comp. Sci. 20, 265–321 (1982)

    MathSciNet  MATH  Google Scholar 

  9. Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not enough points is enough. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 298–312. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Curien, P.-L.: On the symmetry of sequentiality. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 29–71. Springer, Heidelberg (1994)

    Google Scholar 

  11. Curien, P.-L.: Notes on game semantics. From the author’s web page (2006)

    Google Scholar 

  12. Hyland, J.M.E.: Game semantics. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, CUP, pp. 131–194 (1997)

    Google Scholar 

  13. Laird, J.: A game semantics of local names and good variables. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, Springer, Heidelberg (2004)

    Google Scholar 

  14. Lambek, J., Scott, P.: Introduction to Higher-Order Categorical Logic, CUP (1986)

    Google Scholar 

  15. Launchbury, J., Peyton Jones, S.: State in Haskell. Lisp Symb. Comp. 8, 193–341 (1995)

    Google Scholar 

  16. Longley, J.R.: Notions of computability at higher types I. In: Longley, J.R. (ed.) Proc. Logic Colloquium 2000. Lecture Notes in Logic, ASL, vol. 200, pp. 32–142 (2005)

    Google Scholar 

  17. Longley, J.R.: On the ubiquity of certain total type structures. Math. Struct. in Comp. Science 17, 841–953 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  18. Longley, J.R., Wolverson, N.: Eriskay: a programming language based on game semantics. GaLoP III, Budapest (to be presented) (2008)

    Google Scholar 

  19. Melliès, P.-A.: Comparing hierarchies of types in models of linear logic. Inf. Comp. 189(2), 202–234 (2004)

    Article  MATH  Google Scholar 

  20. Moggi, E.: Computational lambda-calculus and monads. In: LFCS report ECS-LFCS-88-66, University of Edinburgh (1988); A shorter version appeared. In: Proc. 4th LICS, pp.14-23. IEEE Press (1989)

    Google Scholar 

  21. Moggi, E.: An abstract view of programming languages. LFCS report ECS-LFCS-90-113, University of Edinburgh (1989)

    Google Scholar 

  22. Moggi, E.: Notions of computation and monads. Inf. and Comp. 93, 55–92 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  23. Moggi, E., Sabry, A.: Monadic encapsulation of effects: a revised approach. J. Funct. Prog. 11(6), 591–627 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  24. Peyton Jones, S., Wadler, P.: Imperative functional programming. In: Proc. 20th POPL, ACM Press, New York (1993)

    Google Scholar 

  25. Pitts, A., Stark, I.: Observable Properties of Higher Order Functions that Dynamically Create Local Names, or: What’s new? In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 122–141. Springer, Heidelberg (1993)

    Google Scholar 

  26. Plotkin, G.D.: LCF considered as a programming language. Theor. Comp. Sci. 5, 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  27. Plotkin, G.D., Power, A.J.: Algebraic operations and generic effects. Appl. Categ. Struct. 11(1), 69–94 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  28. Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theor. Comp. Sci. 342, 28–55 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  29. Stark, I.: Free-algebra models for the π-calculus. Theor. Comp. Sci. 390(2-3), 248–270 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  30. Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. LNM, vol. 344. Springer, Heidelberg (1973)

    MATH  Google Scholar 

  31. Tzevelekos, N.: Full abstraction for nominal general references. In: Proc. 22nd LICS, pp. 399–410. IEEE Press, Los Alamitos (2007)

    Google Scholar 

  32. Wolverson, N.: Game semantics for object-oriented languages. PhD thesis, University of Edinburgh (submitted, 2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science School of Informatics, University of Edinburgh, The King’s Buildings, Mayfield Road, Edinburgh, EH9 3JZ, UK

    John Longley

Authors
  1. John Longley
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Arnold Beckmann Costas Dimitracopoulos Benedikt Löwe

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Longley, J. (2008). Interpreting Localized Computational Effects Using Operators of Higher Type. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds) Logic and Theory of Algorithms. CiE 2008. Lecture Notes in Computer Science, vol 5028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69407-6_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69407-6_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69405-2

  • Online ISBN: 978-3-540-69407-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation