A confluence result for a typed λ-calculus of exception handling with fixed-point

  • Catherine Pilière
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


We prove the confluence of a λ-calculus of exception handling whose typing system and evaluation rules are initially based on classical logic through the Curry-Howard isomorphism and to which we have added a general fixed-point operator.


Classical Logic Reduction Rule Natural Deduction Evaluation Rule Exception Handling 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    H.P. Barendregt. The Lambda Calculus. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984.Google Scholar
  2. [2]
    R.V. Book and F. Otto. String-rewriting systems. Texts and Monographs in Computer Science. Springer-Verlag, 1993.Google Scholar
  3. [3]
    Ph. de Groote. A simple calculus of exception handling. Lectures Notes in Computer Science, 902:201–215, 1995.Google Scholar
  4. [4]
    K. Fujita. Calculus of classical proofs 1. Lectures Notes in Computer Science, 1345:321–335, 1997.Google Scholar
  5. [5]
    J.H. Gallier. On the correspondence between proofs and λ-terms. Cahiers du Centre de Logique (Universitè Catholique de Louvain), 8:55–138, 1995.MathSciNetGoogle Scholar
  6. [6]
    J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Computer Science. Cambridge University Press, 1989.Google Scholar
  7. [7]
    J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theorical Computer Science, 121:279–308, 1993.zbMATHCrossRefGoogle Scholar
  8. [8]
    D. Prawitz. Natural deduction: a proof-theoretical study. Almquist and Wiksell, Stockholm, 1965zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Catherine Pilière
    • 1
  1. 1.LORIAVandœuvre-lès-Nancy CedexFrance

Personalised recommendations