Skip to main content
SpringerLink
Log in

Calculus of classical proofs I

  • Session 8
  • Conference paper
  • First Online:
Advances in Computing Science — ASIAN'97 (ASIAN 1997)

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

Included in the following conference series:

Abstract

We introduce a simple natural deduction system of classical propositional logic called λ vexc , and prove the computational properties of the system based on a call-by-value strategy. We show (1) a strict fragment of gl vexc that is complete with respect to classical provability, and the computational meaning of the existence of such a fragment; (2) a simple exit mechanism by the use of a proof of Peirce's law, and some examples using classical proofs as programs; (3) the Church-Rosser property; (4) the CPS-translation from λ vexc to λ→ and its correctness with respect to conversions; (5) a computational use of the logical inconsistency in λ vexc , extended with a certain signature.

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. Andou, Y.: A Normalization-Procedure for the First Order Classical Natural Deduction with Full Logical Symbols. Tsukuba Journal of Mathematics 19 1 (1995) 153–162

    Google Scholar 

  2. Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics (revised edition). North-Holland (1984)

    Google Scholar 

  3. Barendregt, H.P.: Lambda Calculi with Types. Handbook of Logic in Computer Science Vol. II. Oxford University Press (1992) 1–189

    Google Scholar 

  4. Barbanera, F. and Berardi, S.: Extracting Constructive Context from Classical Logic via Control-like Reductions. LNCS 664 (1993) 45–59

    Google Scholar 

  5. Coquand, T.: An Analysis of Girard's Paradox. Proc. 1st Logic in Computer Science (1986) 227–236

    Google Scholar 

  6. De Groote, P.: On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control. LNAI 822 (1994) 31–43

    Google Scholar 

  7. De Groote, P.: A Simple Calculus of Exception Handling. LNCS 902 (1995) 201–215

    Google Scholar 

  8. Felleisen, M., Friedman, D.P., Kohlbecker, E. and Duba, B.: Reasoning with Continuations. Proc. Annual IEEE Symposium on Logic in Computer Science (1986) 131–141

    Google Scholar 

  9. Felleisen, M. and Hieb, R.: The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science 103 (1992) 131–141

    Article  Google Scholar 

  10. Fujita, K.: On Embedding of Classical Substructural Logics. Proc. Theory of Rewriting Systems and Its Applications Kyoto University RIMS 918 (1995) 178–195

    Google Scholar 

  11. Fujita, K.: μ,-Head Form Proofs and its Application to Programming. Computer Software 14 2 (1997) 71–75

    Google Scholar 

  12. Fujita, K.: μ-Head Form Proofs with at Most Two Formulas in the Succedent. Transactions of Information Processing Society of Japan 38 6 (1997) 1073–1082

    Google Scholar 

  13. Fujita, K.: Calculus of Classical Proofs from Programming Viewpoint. Kyoto University RIMS 1010 (1997) 7–34

    Google Scholar 

  14. Griffin, T.G.: A Formulae-as-Types Notion of Control. Proc. 17th Annual ACM Symposium on Principles of Programming Languages (1990) 47–58

    Google Scholar 

  15. Harper, R., Duba, B.F. and MacQueen, D.: Typing First-Class Continuations in ML. J. Functional Programming 3 (4) (1993) 465–484

    Google Scholar 

  16. Hayashi, S. and Nakano, H.: PX A Computational Logic. The MIT Press (1988)

    Google Scholar 

  17. Howard, W.: The Formulae-as-Types Notion of Constructions. To H.B.Curry: Essays on combinatory logic, lambda-calculus, and formalism. Academic Press (1980) 479–490

    Google Scholar 

  18. Howe, D.J.: The Computational Behaviour of Girard's Paradox. Proc. 2nd Logic in Computer Science (1987) 205-214

    Google Scholar 

  19. Kobayashi, S.: Monads, Modality and Curry-Howard Principle. Proc. 10th Japan Society for Software Science and Technology (1993) 225–228

    Google Scholar 

  20. Lillibridge, M.: Exceptions Are Strictly More Powerful Than Call/CC. Carnegie Mellon University CMU-CS-95-178 (1995)

    Google Scholar 

  21. Milner, R., Tofte, M. and Harper, R.: The Definition of Standard ML. The MIT Press (1990)

    Google Scholar 

  22. Murthy, C.R.: An Evaluation Semantics for Classical Proofs. Proc. 6th Annual IEEE Symposium on Logic in Computer Science (1991) 96–107

    Google Scholar 

  23. Nakano, H.: Logical Structures of the Catch and Throw Mechanism. PhD thesis University of Tokyo (1995)

    Google Scholar 

  24. Nordstr6m, B., Petersson, K. and Smith, J.M.: Programming in Martin-Löf's Type Theory An Introduction. Clarendon Press (1990)

    Google Scholar 

  25. Ong, C.-H.L.: A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations. Linear Logic '96 Tokyo Meeting (1996)

    Google Scholar 

  26. Ong, C.-H.L. and Stewart, C.A.: A Curry-Howard Foundation for Functional Computation with Control. Proc. 24th Annual ACM SIGPLAN-SIGACT Symposium of Principles of Programming Languages (1997)

    Google Scholar 

  27. Parigot, M.: μ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. LNCS 624 (1992) 190–201

    Google Scholar 

  28. Parigot, M.: Classical Proofs as Programs. LNCS 713 (1993) 263–276

    Google Scholar 

  29. Parigot, M.: Strong Normalization for Second Order Classical Natural deduction. Proc. 8th Annual IEEE Symposium on Logic in Computer Science (1993)

    Google Scholar 

  30. Plotkin, G.: Call-by-Name, Call-by-Value and the λ-Calculus. Theoretical Computer Science 1 (1975) 125–159

    Article  Google Scholar 

  31. Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almgvist&Wiksell (1965)

    Google Scholar 

  32. Rehof, N.J. and Sorensen, M.H.: The λΔ-Calculus. LNCS 789 (1994) 516–542

    Google Scholar 

  33. Seldin, J.P.: Normalization and Excluded Middle I. Studia Logica XLVIII 2 (1989) 193–217

    Google Scholar 

  34. Szabo, M.E.: The Collected Papers of Gerhard Gentzen. North-Holland (1969)

    Google Scholar 

  35. Takahashi, M.: Parallel Reductions in λ-Calculus. J. Symbolic Computation 7 (1989) 113–123

    Google Scholar 

  36. Takeuti, G.: Proof Theory (second edition). North-Holland (1987)

    Google Scholar 

  37. Tonino, H. and Fujita, K.: On the adequacy of representing higher order intuitionistic logic as a pure type system. Annals of Pure and Applied Logic 57 (1992) 251–276

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Kyushu Institute of Technology, 820, Iizuka, Japan

    Ken-etsu Fujita

Authors
  1. Ken-etsu Fujita
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

R. K. Shyamasundar K. Ueda

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fujita, Ke. (1997). Calculus of classical proofs I. In: Shyamasundar, R.K., Ueda, K. (eds) Advances in Computing Science — ASIAN'97. ASIAN 1997. Lecture Notes in Computer Science, vol 1345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63875-X_62

Download citation

  • DOI: https://doi.org/10.1007/3-540-63875-X_62

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63875-9

  • Online ISBN: 978-3-540-69658-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation