Skip to main content
SpringerLink
Log in

λμ-Calculus: An algorithmic interpretation of classical natural deduction

  • Session 8: Logical Frameworks
  • Conference paper
  • First Online:
Book cover Logic Programming and Automated Reasoning (LPAR 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 624))

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. T. GRIFFIN, A formulae-as-types notion of control, Proc. POPL, 1990.

    Google Scholar 

  2. W.A. HOWARD, The formulae as types notion of construction. Manuscript 1969. In: To H.B. Curry: Essays on combinatory logic, λ-calculus and formalism; Seidin, Hindley (eds.), Academic Press 1980.

    Google Scholar 

  3. J.L. KRIVINE, Opérateurs de mise en mémoire et traduction de Gödel. Archive for Mathematical Logic, 30(1990).

    Google Scholar 

  4. G. MURTHY, Classical proofs as programs: how, when, and why. Manuscript, 1991.

    Google Scholar 

  5. M. PARIGOT & J.L. KRIVINE, Programming with proofs. Presented at SCT'87. In EIK 26 (1990).

    Google Scholar 

  6. M. PARIGOT, Free deduction: an analysis of “computations” in classical logic. 2nd Russian Conference on Logic Programming, 1991 (to appear in LNAI).

    Google Scholar 

  7. D. PRAWITZ, Natural deduction. Almqvist&Wiksell, 1965.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Equipe de logique - CNRS UA 753 45-55 5éme étage, Université Paris 7, 2 place jussieu, 75251, Paris Cedex 05, France

    Michel Parigot

Authors
  1. Michel Parigot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Parigot, M. (1992). λμ-Calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013061

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55727-2

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation