[Prev][Next][Index][Thread]
New paper: an intuitionistic lambda-calculus with exceptions
I am pleased to announce my PhD thesis, (Universite de Savoie, France,
19 fevrier 19999) available (in french) at the author :
mounier@univ-savoie.fr
Regards,
Georges Mounier
------------------------------------------------------------------------
AN INTUITIONISTIC LAMBDA-CALCULUS WITH EXCEPTIONS
Georges Mounier
Abstract:
The thesis describes a typed lambda-calculus extended with a mechanism
for exceptions.
Typed lambda-calculus is a good theoretical model for the functional
aspects of programming languages, but not for exceptions.
We first examine typed lambda-calculi recently proposed to give a
logical interpretation of control mechanisms, and we show that no one
of them is a satisfying description of exceptions - as they are
implemented, for example, in the Caml language.
Then, we describe a new typed lambda-calculus, named Ex2, which
allows to declare, raise and handle exceptions.
The main properties of Ex2 are proved :
confluence of the calculus, strong normalization of typed terms, subject
reduction for a parallel notion of reduction and preservation of data
types (e.g. the Church numerals are the only normal terms of type N).
Some examples are given. They use exceptions either to interrupt or to
speed up a computation.
Finally we prove that Ex2 is an intuitionistic proof system, a result
which is to compare with the link usually made between control
operators and classical logic.
=========================================================================
Georges MOUNIER
***************** Tel (perso) 04.78.69.31.01 ***************
***************** Email georges.mounier@ac-lyon.fr ****************
=========================================================================