Abstract FR:

La these decrit un systeme de -calcul type etendu par un traitement des exceptions. Le -calcul type est une bonne description abstraite des langages de programmation fonctionnels, mais les exceptions sortent de son cadre. Apres avoir examine trois -calculs types recemment proposes pour donner une interpretation logique des mecanismes de controle et verifie qu'aucun ne permet de decrire completement le mecanisme des exceptions, tel qu'il est, par exemple, mis en oeuvre dans la langage caml, la these decrit un systeme de -calcul type original ex2 integrant declaration, levee et capture des exceptions. Les proprietes du systeme ex2 sont ensuite prouvees : la reduction des termes est confluente ; tout terme typable est fortement normalisable ; le type se conserve non dans la reduction ordinaire, mais dans une forme parallelisee de la reduction qui produit les memes formes normales ; seuls les termes equivalents aux entiers de church ont le type entier. Le systeme ex2 permet d'utiliser les exceptions aussi bien pour abreger un calcul, que pour denoter une impossibilite a poursuivre : plusieurs exemples en sont fournis. Enfin nous prouvons que ex2 est un calcul de preuve intuitionniste, resultat qui amene a s'interroger sur l'opinion couramment admise qui relie operateurs de controle et logique classique.