Skip to main content
SpringerLink
Log in

From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple

  • Conference paper
  • First Online:
FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002)

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

Abstract

We give a first-principles description of the context semantics of Gonthier, Abadi, and Lévy, a computer-science analogue of Girard’s geometry of interaction. We explain how this denotational semantics models λ-calculus, and more generally multiplicative-exponential linear logic (MELL), by explaining the call-by-name (CBN) coding of the λ- calculus, and proving the correctness of readback, where the normal form of a λ-term is recovered from its semantics. This analysis yields the correctness of Lamping’s optimal reduction algorithm. We relate the context semantics to linear logic types and to ideas from game semantics, used to prove full abstraction theorems for PCF and other λ-calculus variants.

Supported by NSF Grants CCR-0228951 and EIA-9806718, and also by the Tyson Foundation.

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, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409–470, Dec. 2000.

    Article  MATH  MathSciNet  Google Scholar 

  2. S. Abramsky and G. McCusker. Game semantics. In H. Schwichtenberg and U. Berger, editors, Theoretical Foundations of Computer Graphics and CAD, volume 165 of NATO ASI, pages 307–325. Springer-Verlag, 1999.

    Google Scholar 

  3. A. Asperti. Linear logic, comonads and optimal reductions. Fundamentae Informaticae, 22:3–22, 1995.

    MATH  MathSciNet  Google Scholar 

  4. A. Asperti and S. Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge University Press, 1998.

    Google Scholar 

  5. A. Asperti and C. Laneve. Paths, computations and labels in the λ-calculus. Theoretical Computer Science, 142(2):277–297, 15 May 1995.

    Article  MATH  MathSciNet  Google Scholar 

  6. A. Asperti and H. G. Mairson. Parallel beta reduction is not elementary recursive. Information and Computation, 170:49–80, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  7. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.

    Google Scholar 

  8. J.-Y. Girard. Geometry of interaction I: Interpretation of system F. In C. Bonotto, R. Ferro, S. Valentini, and A. Zanardo, editors, Logic Colloquium’ 88, pages 221–260. North-Holland, 1989.

    Google Scholar 

  9. G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In Conference record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: papers presented at the symposium, Albuquerque, New Mexico, January 19–22, 1992, pages 15–26, New York, NY, USA, 1992. ACM Press.

    Google Scholar 

  10. G. Gonthier, M. Abadi, and J.-J. Lévy. Linear logic without boxes. In Proceedings 7th Annual IEEE Symp. on Logic in Computer Science, LICS’92, Santa Cruz, CA, USA, 22–25 June 1992, pages 223–34. IEEE Computer Society Press, Los Alamitos, CA, 1992.

    Google Scholar 

  11. J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285–408, Dec. 2000.

    Article  MATH  MathSciNet  Google Scholar 

  12. J. Lamping. An algorithm for optimal lambda calculus reduction. In POPL’ 90. Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, January 17–19, 1990, San Francisco, CA, pages 16–30, New York, NY, USA, 1990. ACM Press.

    Google Scholar 

  13. J.-J. Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université Paris 7, 1978. Thèse d’Etat.

    Google Scholar 

  14. P. Wadler. The essence of functional programming. In Conference record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: papers presented at the symposium, Albuquerque, New Mexico, January 19–22, 1992, pages 1–14, New York, NY, USA, 1992. ACM Press.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Brandeis University, Waltham, 02454, Massachusetts

    Harry G. Mairson

Authors
  1. Harry G. Mairson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, 208016, Kanpur, India

    Manindra Agrawal  & Anil Seth  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mairson, H.G. (2002). From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation