Skip to main content
SpringerLink
Log in

Capsules and Closures: A Small-Step Approach

  • Chapter
Logic and Program Semantics

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7230))

Abstract

We present a side by side comparison of Capsules and Closures, including a proof of bisimilarity, using small-step semantics. A similar proof was presented in [8], using big-step semantics. However, while big-step semantics only allow to talk about final results of terminating computations, the use of small-step semantics allows to prove a stronger bisimilarity involving every step of the computation and thus also applicable to infinite computations.

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. Aboul-Hosn, K.: Programming with private state. Honors Thesis, The Pennsylvania State University (December 2001), http://www.cs.cornell.edu/%7Ekamal/thesis.pdf

  2. Aboul-Hosn, K., Kozen, D.: Relational semantics of local variable scoping. Tech. Rep. 2005-2000, Cornell University (2005), http://www.cs.cornell.edu/%7Ekamal/local.pdf

  3. Aboul-Hosn, K., Kozen, D.: Relational Semantics for Higher-Order Programs. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 29–48. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: LICS 1998: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pp. 334–344. IEEE Computer Society, Washington, DC (1998)

    Google Scholar 

  5. Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for idealized ALGOL with active expressions. Electr. Notes Theor. Comput. Sci. 3 (1996)

    Google Scholar 

  6. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science 103, 235–271 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Halpern, J.Y., Meyer, A.R., Trakhtenbrot, B.A.: The semantics of local storage, or what makes the free-list free? In: Proc. 11th ACM Symp. Principles of Programming Languages (POPL 1984), New York, NY, USA, pp. 245–257 (1984)

    Google Scholar 

  8. Jeannin, J.B.: Capsules and closures. In: Mislove, M., Ouaknine, J. (eds.) Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXVII). Elsevier Electronic Notes in Theoretical Computer Science, Pittsburgh, PA (2011)

    Google Scholar 

  9. Jeannin, J.B., Kozen, D.: Computing with capsules. Tech. Rep., Computing and Information Science, Cornell University (January 2011), http://hdl.handle.net/1813/22082

  10. Laird, J.: A Game Semantics of Local Names and Good Variables. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 289–303. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Mason, I.A., Talcott, C.L.: References, local variables and operational reasoning. In: Seventh Annual Symposium on Logic in Computer Science, pp. 186–197. IEEE (1992), http://www-formal.stanford.edu/MT/92lics.ps.Z

  12. Mason, I., Talcott, C.: Programming, transforming, and proving with function abstractions and memories

    Google Scholar 

  13. Mason, I., Talcott, C.: Axiomatizing operational equivalence in the presence of side effects. In: IEEE Fourth Annual Symposium on Logic in Computer Science, pp. 284–293. IEEE Computer Society Press (1989)

    Google Scholar 

  14. Mason, I., Talcott, C.: Equivalence in functional languages with effects (1991)

    Google Scholar 

  15. Milne, R., Strachey, C.: A Theory of Programming Language Semantics. Halsted Press, New York (1977)

    Google Scholar 

  16. Moggi, E.: Notions of computation and monads. Information and Computation 93(1) (1991)

    Google Scholar 

  17. Pitts, A.M.: Operationally-based theories of program equivalence. In: Dybjer, P., Pitts, A.M. (eds.) Semantics and Logics of Computation, pp. 241–298. Publications of the Newton Institute, Cambridge University Press (1997), http://www.cs.tau.ac.il/~nachumd/formal/exam/pitts.pdf

  18. Pitts, A.M., Stark, I.D.B.: Operational reasoning in functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 227–273. Cambridge University Press (1998), http://homepages.inf.ed.ac.uk/stark/operfl.pdf

  19. Pitts, A.M., Stark, I.D.B.: 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)

    Chapter  Google Scholar 

  20. Scott, D.S.: Mathematical concepts in programmng language semantics. In: Proc. 1972 Spring Joint Computer Conferences, pp. 225–234. AFIPS Press, Montvale (1972)

    Google Scholar 

  21. Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1981)

    MATH  Google Scholar 

  22. Sussman, G.J., Steele, G.L.: Scheme: A interpreter for extended lambda calculus. Higher-Order and Symbolic Computation 11, 405–439 (1998), http://dx.doi.org/10.1023/A:1010035624696 , 10.1023/A:1010035624696

    Article  MATH  Google Scholar 

  23. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, Ithaca, New York, 14853-7501, USA

    Jean-Baptiste Jeannin

Authors
  1. Jean-Baptiste Jeannin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, Cornell University, 4149 Upson Hall, 14853, Ithaca, NY, USA

    Robert L. Constable

  2. Intelligent Systems Faculty of Science, Institute for Computing and Information Sciences, Radboud University Nijmegen, Postbus 9010, 6500 GL, Nijmegen, The Netherlands

    Alexandra Silva

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Jeannin, JB. (2012). Capsules and Closures: A Small-Step Approach. In: Constable, R.L., Silva, A. (eds) Logic and Program Semantics. Lecture Notes in Computer Science, vol 7230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29485-3_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-29485-3_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-29484-6

  • Online ISBN: 978-3-642-29485-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation