Hostname: page-component-745bb68f8f-f46jp Total loading time: 0 Render date: 2025-01-12T04:14:42.041Z Has data issue: false hasContentIssue false
  • English
  • Français

An intuitionistic λ-calculus with exceptions

Published online by Cambridge University Press:  08 December 2004

R. DAVID  and
G. MOUNIER
R. DAVID
Affiliation:
Laboratoire de Mathématiques, Université de Savoie Campus Scientifique, 73376 Le Bourget du Lac cedex, France (e-mail: [email protected], [email protected])
G. MOUNIER
Affiliation:
Laboratoire de Mathématiques, Université de Savoie Campus Scientifique, 73376 Le Bourget du Lac cedex, France (e-mail: [email protected], [email protected])
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 introduce a typed λ-calculus which allows the use of exceptions in the ML style. It is an extension of the system $AF_2$ of Krivine & Leivant (Krivine, 1990; Leivant, 1983). We show its main properties: confluence, strong normalization and weak subject reduction. The system satisfies the “the proof as program” paradigm as in $AF_2$. Moreover, the underlined logic of our system is intuitionistic logic.

Type
Article
Information
Journal of Functional Programming , Volume 15 , Issue 1 , January 2005 , pp. 33 - 52
Copyright
© 2004 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.