A confluence Result for a Typed lambda-Calculus of Exception Handling with Fixed-point

Catherine Pilière (1)

1 CALLIGRAMME - Linear logic, proof networks and categorial grammars

We prove the confluence of a lambda-calculus of exception handling whose typing system and evaluation rules are initially based on classical logic through the Curry-Howard isomorphism and to which we have added a general fixed-point operator.

Mots clés: lambda-calculus; confluence; exception handling; functional programming; fixed-point; traitement d'exception; programmation fonctionnelle; point fixe; lambda-calcul

Domaines: Autre [cs.OH]

Catherine Pilière. A confluence Result for a Typed lambda-Calculus of Exception Handling with Fixed-point. 12th International Symposium on Fundamentals of Computation Theory - FCT'99, 1999, Iasi, Romania, pp.421-432. ⟨inria-00098837⟩