Hostname: page-component-8448b6f56d-c4f8m Total loading time: 0 Render date: 2024-04-23T17:21:12.415Z Has data issue: false hasContentIssue false

A confluent λ-calculus with a catch/throw mechanism

Published online by Cambridge University Press:  01 November 1999

TRISTAN CROLARD
Affiliation:
Laboratoire Preuves, Programmes et Systèmes Université Paris 7, France (e-mail: crolard@ufr-info-p7.jussieu.fr)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.