Alexis Saurin
IRIF, Université de Paris
https://www.irif.fr/~saurin//
Date(s) : 19/04/2018 iCal
11 h 00 min - 12 h 30 min
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.
Catégories