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
-
De caractériser syntaxiquement les réductions valides du système
mu-mu-tilde avec union non-déterministe.
- D'unifier si possible les présentations catégoriques de Selinger et de
Došen et Petric de telle sorte que, comme dans le cadre
syntaxique du calcul lambda-bar, le choix entre non-déterminisme,
appel par nom et appel par valeur, se caractérise par la présence ou
non d'un axiome particulier au dessus d'un ensemble commun d'axiomes.
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.