Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Descriptional Complexity of Formal Systems

DCFS 2012: Descriptional Complexity of Formal Systems pp 1–19Cite as

Computing with Capsules

  • Conference paper

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

Abstract

Capsules provide an algebraic representation of the state of a computation in higher-order functional and imperative languages. A capsule is essentially a finite coalgebraic representation of a regular closed λ-coterm. One can give an operational semantics based on capsules for a higher-order programming language with functional and imperative features, including mutable bindings. Static (lexical) scoping is captured purely algebraically without stacks, heaps, or closures. All operations of interest are typable with simple types, yet the language is Turing complete. Recursive functions are represented directly as capsules without the need for fixpoint combinators.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Springer (1996)

    Google Scholar 

  2. Aboul-Hosn, K.: Programming with Private State. Honors Thesis, The Pennsylvania State University (December 2001), http://www.cs.cornell.edu/%7Ekamal/thesis.pdf

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

    Chapter  Google Scholar 

  4. Aboul-Hosn, K., Kozen, D.: Local variable scoping and Kleene algebra with tests. J. Log. Algebr. Program. (2007), doi:10.1016/j.jlap.2007.10.007

    Google Scholar 

  5. 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, USA (1998)

    Google Scholar 

  6. 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 

  7. Barendregt, H.P., Klop, J.W.: Applications of infinitary lambda calculus. Inf. and Comput. 207(5), 559–582 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  8. 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 

  9. 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 

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

    Google Scholar 

  11. Jeannin, J.B.: Capsules and Closures: A Small-Step Approach. In: Constable, R.L., Silva, A. (eds.) Kozen Festschrift. LNCS, vol. 7230, pp. 106–123. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  12. Jeannin, J.B., Kozen, D.: Capsules and separation. Tech. Rep., Computing and Information Science, Cornell University (January 2012), http://hdl.handle.net/1813/28284 ; Conf. Logic in Computer Science (LICS 2012), Dubrovnik, Croatia (to appear, June 2012)

  13. Klop, J.W., de Vrijer, R.C.: Infinitary normalization. In: Artemov, S., Barringer, H., d’Avila Garcez, A.S., Lamb, L.C., Woods, J. (eds.) We Will Show Them: Essays in Honour of Dov Gabbay, vol. 2, pp. 169–192. College Publications (2005)

    Google Scholar 

  14. Kozen, D.: New. Tech. Rep., Computing and Information Science, Cornell University (March 2012), http://hdl.handle.net/1813/28632 ; Conf. Mathematical Foundations of Programming Semantics (MFPS XXVIII), Bath, UK (to appear, June 2012)

  15. 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 

  16. Landin, P.J.: The mechanical evaluation of expressions. Computer Journal 6(4), 308–320 (1964)

    MATH  Google Scholar 

  17. 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

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

    Google Scholar 

  19. 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 

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

    Google Scholar 

  21. McCarthy, J.: History of LISP. In: Wexelblat, R.L. (ed.) History of Programming Languages I, pp. 173–185. ACM (1981)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  24. 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

  25. Pitts, A.M.: Operational semantics and program equivalence. Tech. rep., INRIA Sophia Antipolis (2000), http://www.springerlink.com/media/1f99vvygyh3ygrykklby/contributions/l/w/f/6/lwf6r3jxn7a2lkq0.pdf ; lectures at the International Summer School On Applied Semantics, APPSEM 2000, Caminha, Minho, Portugal (September 2000)

  26. 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

  27. 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)

    Google Scholar 

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

    Google Scholar 

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

    MATH  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 & Dexter Kozen

Authors
  1. Jean-Baptiste Jeannin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dexter Kozen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Giessen, Arndtstraße 2, 35392, Giessen, Germany

    Martin Kutrib

  2. Departamento de Ciência de Computadores, Universidade do Porto, Faculdade de Ciências, Rua do Campo Alegre 1021-1055, 4169-007, Porto, Portugal

    Nelma Moreira  & Rogério Reis  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jeannin, JB., Kozen, D. (2012). Computing with Capsules. In: Kutrib, M., Moreira, N., Reis, R. (eds) Descriptional Complexity of Formal Systems. DCFS 2012. Lecture Notes in Computer Science, vol 7386. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31623-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31623-4_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31622-7

  • Online ISBN: 978-3-642-31623-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation