[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    ****************
=========================================================================