Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A proof-theoretic foundation of abortive continuations

  • Published:
Higher-Order and Symbolic Computation

Abstract

We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s law without enforcing Ex Falso Quodlibet. We show that a “natural” implementation of this logic is Parigot’s classical natural deduction. We then move on to the computational side and emphasize that Parigot’s λ μ corresponds to minimal classical logic. A continuation constant must be added to λ μ to get full classical logic. The extended calculus is isomorphic to a syntactical restriction of Felleisen’s theory of control that offers a more expressive reduction semantics. This isomorphic calculus is in correspondence with a refined version of Prawitz’s natural deduction.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Thirtieth International Colloquium on Automata, Languages and Programming, ICALP’03, Eindhoven, The Netherlands, June 30–July 4, 2003. Lecture Notes in Computer Science, vol. 2719, pp. 871–885. Springer, New York (2003)

    Google Scholar 

  2. Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of continuations and prompts. In: ACM SIGPLAN International Conference on Functional Programming, pp. 40–53. ACM Press, New York (2004)

    Google Scholar 

  3. Ariola, Z.M., Herbelin, H., Sabry, A.: A proof-theoretic foundation of abortive continuations (extended version). Technical Report TR608, Computer Science Department, Indiana University (2005)

  4. Avron, A.: Natural 3-valued logics—characterization and proof theory. J. Symb. Log. 56(1), 276–294 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  5. Barbanera, F., Berardi, S.: Extracting constructive content from classical logic via control-like reductions. In: Bezem, M., Groote, J.F. (eds.) Proceedings 1st Intl. Conf. on Typed Lambda Calculi and Applications, TLCA’93, Utrecht, The Netherlands, 16–18 March 1993. Lecture Notes in Computer Science, vol. 664, pp. 45–59. Springer, Berlin (1993)

    Google Scholar 

  6. Barendregt, H.P.: Lambda calculi with types. In: Maibaum, A.G. (ed.) Handbook of Logic in Computer Science, vol. 2, pp. 117–309. Oxford University Press, Oxford (1992)

    Google Scholar 

  7. Bierman, G.: A computational interpretation of the lambda-mu calculus. In: Brim, L., Gruska, J., Zlatuska, J. (eds.) Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 1450, pp. 336–345. Springer, New York (1998)

    Chapter  Google Scholar 

  8. Crolard, T.: A confluent lambda-calculus with a catch/throw mechanism. J. Funct. Program. 9(6), 625–647 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  9. de Groote, P.: On the relation between the lambda-mu calculus and the syntactic theory of sequential control. In: Pfennig, F. (ed.) Logic Programming and Automated Reasoning, Proc. of the 5th International Conference, LPAR’94, pp. 31–43. Springer, Berlin (1994)

    Google Scholar 

  10. de Groote, P.: An environment machine for the lambda-mu-calculus. Math. Struct. Comput. Sci. 8(6), 637–669 (1998)

    Article  MATH  Google Scholar 

  11. Felleisen, M.: The theory and practice of first-class prompts. In: Proceedings of the 15th ACM Symposium on Principles of Programming Languages (POPL’88), pp. 180–190. ACM Press, New York (1988)

    Chapter  Google Scholar 

  12. Felleisen, M.: On the expressive power of programming languages. In: Jones, N. (ed.) ESOP’90 3rd European Symposium on Programming, Copenhagen, Denmark. Lecture Notes in Computer Science, vol. 432, pp. 134–151. Springer, New York (1990)

    Google Scholar 

  13. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  14. Gentzen, G.: Investigations into logical deduction. In: Szabo, M. (ed.) Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1969)

    Google Scholar 

  15. Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comput. Sci. 1(3), 255–296 (1991)

    MATH  MathSciNet  Google Scholar 

  16. Goubault-Larrecq, J., Mackie, I.: Proof Theory and Automated Deduction. Kluwer Academic, Dordrecht (2001)

    Google Scholar 

  17. Griffin, T.G.: The formulae-as-types notion of control. In: Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL’90, San Francisco, CA, USA, 17–19 Jan. 1990, pp. 47–57. ACM Press, New York (1990)

    Google Scholar 

  18. Hofmann, M.: Sound and complete axiomatisations of call-by-balue control operators. Math. Struct. Comput. Sci. 5(4), 461–482 (1995)

    Article  MATH  Google Scholar 

  19. Johansson, I.: Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compos. Math. 4, 119–136 (1937)

    MathSciNet  Google Scholar 

  20. Kameyama, Y., Hasegawa, M.: A sound and complete axiomatization of delimited continuations. In: Proc. of 8th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP’03, Uppsala, Sweden, 25–29 Aug. 2003. SIGPLAN Notices, vol. 38(9), pp. 177–188. ACM Press, New York (2003)

    Google Scholar 

  21. Lalement, R.: Computation as Logic. Prentice Hall International Series in Computer Science, Amsterdam (1993)

    MATH  Google Scholar 

  22. Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Conf. Record 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL’97, Paris, France, 15–17 Jan. 1997, pp. 215–227. ACM Press, New York (1997)

    Chapter  Google Scholar 

  23. Parigot, M.: Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In: Logic Programming and Automated Reasoning: International Conference LPAR’92 Proceedings, St. Petersburg, Russia, pp. 190–201. Springer, New York (1992)

    Google Scholar 

  24. Parigot, M.: Classical proofs as programs. Comput. Log. Theory 713, 263–276 (1993)

    Article  MathSciNet  Google Scholar 

  25. Parigot, M.: Strong normalization for second order classical natural deduction. In: Proceedings 8th Annual IEEE Symp. on Logic in Computer Science, LICS’93, pp. 39–47. IEEE Computer Society Press (1993)

  26. Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. J. Symb. Log. 62(4), 1461–1479 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  27. Prawitz, D.: Natural Deduction, a Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965)

    MATH  Google Scholar 

  28. Py, W.: Confluence en λ μ-calcul. Ph.D. thesis, Université de Savoie (1998)

  29. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symb. Comput. 6(3–4), 289–360 (1993)

    Article  Google Scholar 

  30. Selinger, P.: Control categories and duality: on the categorical semantics of the lambda-mu calculus. Math. Struct. Comput. Sci. 11(2), 207–260 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  31. Streicher, T., Reus, B.: Classical logic: continuation semantics and abstract machines. J. Funct. Program. 8(6), 543–572 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  32. van Dalen, D.: Logic and Structure. Springer, New York (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oregon, Eugene, USA

    Zena M. Ariola

  2. INRIA-Futurs, Orsay, France

    Hugo Herbelin

  3. Indiana University, Bloomington, USA

    Amr Sabry

Authors
  1. Zena M. Ariola
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hugo Herbelin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Amr Sabry
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zena M. Ariola.

Additional information

This article is an extended version of the conference article “Minimal Classical Logic and Control Operators” (Ariola and Herbelin, Lecture Notes in Computer Science, vol. 2719, pp. 871–885, 2003). A longer version is available as a technical report (Ariola et al., Technical Report TR608, Indiana University, 2005).

Z.M. Ariola supported by National Science Foundation grant number CCR-0204389.

A. Sabry supported by National Science Foundation grant number CCR-0204389, by a Visiting Researcher position at Microsoft Research, Cambridge, U.K., and by a Visiting Professor position at the University of Genova, Italy.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ariola, Z.M., Herbelin, H. & Sabry, A. A proof-theoretic foundation of abortive continuations. Higher-Order Symb Comput 20, 403–429 (2007). https://doi.org/10.1007/s10990-007-9007-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10990-007-9007-z

Keywords

Search

Navigation