No CrossRef data available.
Published online by Cambridge University Press: 01 November 1999
We derive a confluent λ-calculus with a catch/throw mechanism (called λct-calculus) from Parigot's λμ-calculus. We also present several translations from one calculus into the other which are morphisms for the reduction. We use them to show that the λct-calculus is a retract of λμ-calculus (these calculi are isomorphic if we consider only convertibility). As a by-product, we obtain the subject reduction property for the λct-calculus, as well as the strong normalization for λct-terms typable in the second order classical natural deduction.
Discussions
No Discussions have been published for this article.