Logical by-need

Carte non disponible

Date/heure
Date(s) - 19/04/2018
11 h 00 min - 12 h 30 min

Catégories


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.

http://www.irif.fr/~saurin/

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange