Institut de Mathématiques de Marseille, UMR 7373




Rechercher


Accueil >

Logical by-need

Jeudi 19 avril 11:00-12:30 - Alexis SAURIN - IRIF, Université Paris-Diderot

Logical by-need

Résumé : L’analyse de l’appel par nécessité (aussi appelé évaluation paresseuse) est complexe, d’autant plus lorsqu’on considère des opérateurs de contrôle. Ceci suggère de faire appel à la logique, par nécessité, plutôt qu’à chercher à trouver une solution fondée sur de pures considérations opérationnelles. Dans ce séminaire, je présenterai deux telles approches du logical by-need : le premier inspiré par le système L de Curien et Herbelin et le second de la réduction linéaire de tête de Danos et Regnier.
La première approche ne sera qu’évoquée : l’exposé se visera surtout à construire un calcul paresseux à partir de la réduction linéaire de tête en trois étapes, de le comparer aux calculs de la littérature et de montrer que cette construction s’étend naturellement aux opérateurs de contrôle fournissant un λμ-calcul paresseux. Selon le temps restant, je discuterai de variantes de l’appel par nécessité (notamment la pleine paresse). Cet exposé s’appuie sur des travaux conduits avec Pédrot ainsi qu’Ariola, Downen, Herbelin et Nakata.

JPEG - 7 ko
Alexis SAURIN

Lieu : Salle des séminaires 304-306 (3ème étage) - Institut de Mathématiques de Marseille (UMR 7373)
Site Sud - Bâtiment TPR2
Campus de Luminy, Case 907
13288 MARSEILLE Cedex 9

Exporter cet événement

Pour en savoir plus sur cet événement, consultez l'article Séminaire Logique et Interactions