Skip to main content
SpringerLink
Log in

A computational interpretation of the λΜ-calculus

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1998 (MFCS 1998)

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

Abstract

This paper proposes a simple computational interpretation of Parigot's λΜ-calculus. The λΜ-calculus is an extension of the typed λ-calculus which corresponds via the Curry-Howard correspondence to classical logic. Whereas other work has given computational interpretations by translating the λΜ-calculus into other calculi, I wish to propose here a direct computational interpretation. This interpretation is best given as a single-step semantics which, in particular, leads to a relatively simple, but powerful, operational theory.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G.M. Bierman. A classical linear λ-calculus. Technical Report 401, Cambridge Computer Laboratory 1996.

    Google Scholar 

  2. M. Felleisen. The theory and practice of first-class prompts. POPL 1988.

    Google Scholar 

  3. A.D. Gordon. Bisimilarity as a theory of functional programming: Mini-course. Technical Report NS-95-2, BRICS, Department of Computer Science, University of århus, July 1995.

    Google Scholar 

  4. T.G. Griffin. A formulae-as-types notion of control. POPL 1990.

    Google Scholar 

  5. C.A. Gunter, D. Rémy, and J.G. Riecke. A generalisation of exceptions and control in ML-like languages. FPCA 1995.

    Google Scholar 

  6. R. Harper and C. Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, School of Computer Science, Carnegie Mellon University, June 1997.

    Google Scholar 

  7. M. Hofmann and T. Streicher. Continuation models are universal for λΜ-calculus. LICS 1997.

    Google Scholar 

  8. C.-H.L. Ong and C.A. Stewart. A Curry-Howard foundation for functional computation with control. POPL 1997.

    Google Scholar 

  9. M. Parigot. λΜ-calculus: an algorithmic interpretation of classical natural deduction. LPAR 1992. LNCS 624.

    Google Scholar 

  10. A.M. Pitts. Operational semantics for program equivalence. Slides from talk given at MFPS, 1997.

    Google Scholar 

  11. A.M. Pitts. Operationally-based theories of program equivalence. In Semantics and Logics of Computation, CUP, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Cambridge, USA

    G. M. Bierman

Authors
  1. G. M. Bierman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Luboš Brim Jozef Gruska Jiří Zlatuška

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bierman, G.M. (1998). A computational interpretation of the λΜ-calculus. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055783

Download citation

  • DOI: https://doi.org/10.1007/BFb0055783

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation