Skip to main content
SpringerLink
Log in

Resource Interpretations, Bunched Implications and the αλ-Calculus (Preliminary Version)

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1581))

Included in the following conference series:

Abstract

We introduce the αλ-calculus, a typed calculus that includes a multiplicative function type -* alongside an additive function type →. It arises proof-theoretically as a calculus of proof terms for the logic of bunched implications of O’Hearn and Pym, and semantically from doubly closed categories, where a single category possesses two closed structures. Typing contexts in αλ are bunches, i.e., trees built from two combining operations, one that admits the structural rules of Weakening and Contraction and another that does not. To illuminate the consequences of αλ’s approach to the structural rules we define two resource interpretations, extracted from Reynolds’s “sharing reading” of affine λ-calculus. Based on this we show how αλ enables syntactic control of interference and Idealized Algol, imperative languages based on affine and simply-typed λ-calculi, to be smoothly combined in one system.

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. S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1–2):3–57, April 12 1993.

    Article  MATH  MathSciNet  Google Scholar 

  2. A.R. Anderson and N.D. Belnap. Entailment: the Logic of Relevance and Necessity, volume I. Princeton University Press, 1975.

    Google Scholar 

  3. A. Barber and G.D. Plotkin. Dual intuitionistic linear logic. Submitted, October 1997.

    Google Scholar 

  4. P. N. Benton. A mixed linear and non-linear logic: proofs, terms and models. Proceedings of Computer Science Logic’ 94, Kazimierz, Poland. Springer-Verlag LNCS 933, 1995.

    Google Scholar 

  5. P.N. Benton, G.M. Bierman, V.C.V. de Paiva, and J.M.E. Hyland. Linear λ-calculus and categorical models revisited. In E. Börger et al., editors, Proceedings of the Sixth Workshop on Computer Science Logic, volume 702 of Lecture Notes in Computer Science, pages 61–84. Springer-Verlag, Berlin, 1992.

    Google Scholar 

  6. S. Brookes, M. Main, A. Melton, and M. Mislove, editors. Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, volume 1 of Electronic Notes in Theoretical Computer Science, Tulane University, New Orleans, Louisiana, March 29—April 1 1995. Elsevier Science.

    Google Scholar 

  7. B. J. Day. On closed categories of functors. In S. Mac Lane, editor, Reports of the Midwest Category Seminar, volume 137 of Lecture Notes in Mathematics, pages 1–38. Springer-Verlag, Berlin-New York, 1970.

    Chapter  Google Scholar 

  8. B. J. Day. An embedding theorem for closed categories. In G.M. Kelly, editor, Category Seminar, Sydney, volume 420 of Lecture Notes in Mathematics, pages 55–64. Springer-Verlag, Berlin-New York, 1974.

    Chapter  Google Scholar 

  9. J.M. Dunn. Consecution formulation of positive R with co-tenability and t. In [2], pp381–391.

    Google Scholar 

  10. J.-Y. Girard. Linear logic. Theoretical Computer Science, pages 1–102, 1987. 260

    Google Scholar 

  11. J.-Y Girard. Towards a geometry of interaction. Contemporary Mathematics 92: Categories in Computer Science and Logic, 69–108, 1989.

    Google Scholar 

  12. P. W. O’Hearn. A model for syntactic control of interference. Mathematical Structures in Computer Science, 3(4):435–465, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  13. P. W. O’Hearn, A. J. Power, M. Takeyama, and R. D. Tennent. Syntactic control of interference revisited. Theoretical Computer Science, 1999. To appear. Earlier version in [6] and in [17].

    Google Scholar 

  14. P. W. O’Hearn and U. S. Reddy. Objects, interference and the Yoneda embedding. Theoretical Computer Science, to appear. Preliminary version in [6], 1999.

    Google Scholar 

  15. P. W. O’Hearn and J. C. Reynolds. From Algol to polymorphic linear lambda-calculus. J.ACM, to appear, 1999.

    Google Scholar 

  16. P. W. O’Hearn and R. D. Tennent. Semantics of local variables. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 217–238. Cambridge University Press, Cambridge, England, 1992.

    Google Scholar 

  17. P. W. O’Hearn and R. D. Tennent, editors. Algol-like Languages. Birkhauser, Boston, 1997. Two volumes.

    Google Scholar 

  18. P.W. O’Hearn and D.J. Pym. The logic of bunched implications. 1998. Submitted.

    Google Scholar 

  19. F. J. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. Ph.D. thesis, Syracuse University, Syracuse, N.Y., 1982.

    Google Scholar 

  20. D.J. Pym. The semantics and proof theory of the logic of bunched implications, I: Propositional BI. 1998. Available on the web at http://www.dcs.qmw.ac.uk/~pym.

  21. J. C. Reynolds. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 39–46, Tucson, Arizona, January 1978. ACM, New York. Also in [17], vol 1.

    Google Scholar 

  22. J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372, Amsterdam, October 1981. North-Holland, Amsterdam. Also in [17], vol 1.

    Google Scholar 

  23. J. C. Reynolds. Syntactic control of interference, part 2. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming, 16th International Colloquium, volume 372 of Lecture Notes in Computer Science, pages 704–722, Stresa, Italy, July 1989. Springer-Verlag, Berlin.

    Chapter  Google Scholar 

  24. P. Wadler. A syntax for linear logic. In S. Brookes et al., editors, Mathematical Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 513–529, New Orleans, 1993. Springer-Verlag, Berlin.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Queen Mary & Westfield College, Westfield, UK

    Peter W. O’Hearn

Authors
  1. Peter W. O’Hearn
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS - UPR9016, Institut de Mathématiques de Luminy, 163 Avenue de Luminy, case 907, F-13288, Marseille cedex 9, France

    Jean-Yves Girard

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

O’Hearn, P.W. (1999). Resource Interpretations, Bunched Implications and the αλ-Calculus (Preliminary Version). In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-48959-2_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65763-7

  • Online ISBN: 978-3-540-48959-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation