A confluence result for a typed λ-calculus of exception handling with fixed-point
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.
KeywordsClassical Logic Reduction Rule Natural Deduction Evaluation Rule Exception Handling
Unable to display preview. Download preview PDF.
- H.P. Barendregt. The Lambda Calculus. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984.Google Scholar
- R.V. Book and F. Otto. String-rewriting systems. Texts and Monographs in Computer Science. Springer-Verlag, 1993.Google Scholar
- Ph. de Groote. A simple calculus of exception handling. Lectures Notes in Computer Science, 902:201–215, 1995.Google Scholar
- K. Fujita. Calculus of classical proofs 1. Lectures Notes in Computer Science, 1345:321–335, 1997.Google Scholar
- 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