Développement d'un lambda-calcul dual non-déterministe pour la logique classique



Encadrant: Hugo Herbelin (INRIA-Futurs -- LIX) et ?



Lieu: École Polytechnique à Palaiseau ou PPS ?




Curien et Herbelin ont montré que la structure du lambda-calcul pouvait être finement analysée au travers d'un calcul symétrique avec opérateurs de contrôle (c'est-à-dire lié à la logique classique). Ce calcul, le calcul lambda-bar, est non-déterministe à la base mais il admet deux sous-calculs duaux, l'un implémentant l'appel par valeur et l'autre l'appel par nom.

De son côté, Selinger a exhibé deux structures catégoriques duales pour modéliser les versions appel par nom et appel par valeur du lambda-mu-calcul de Parigot (un calcul classique). Ces modèles sont applicables au cas du calcul lambda-bar.

D'un autre côté, Došen et Petric ont mis au point une structure catégorique caractérisant ce qui semble être l'extension du système mu-mu-tilde avec une opération d'union non-déterministe.

Le but du stage est

Références

- Pierre-Louis Curien et Hugo Herbelin. The duality of computation. International Conference on Functional Programming 2000 (ICFP '00).

- Kosta Došen et Zoran Petric. Proof-Theoretical Coherence. Studies in Logic 1, King's College Publications, London, 2004.

- Peter Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science 11(2), 2001.
This document was translated from LATEX by HEVEA.