Normalization by realizability also evaluates

Résumé : Pour ceux d'entre nous qui vivent dans le monde de la syntaxe, les techniques de preuve sémantiques, comme la réalisabilité, les relations logiques ou la paramétricité ont parfois un arrière-goût de méthode magique. Pourquoi fonctionnent-elles ? Quel est le point clé de la preuve ? Bernardy et Lasson expriment la parametricité comme une construction de modèle syntaxique, par traduction bien typée, mais leurs théorèmes d'abstracion et adéquation restent des résultats au méta-niveau. Dans l'espoir de mieux comprendre ces résultats, nous étudiont leurs preuves comme des programmes. Les preuves de normalization par réalisabilité calculent-elles effectivement des formes normales, comment et à quel moment ? Ce travail de détective est encore à ses débuts, et nous proposons une première tentative dans un cadre très simple : au lieu de Pure Type Systems (PTS), nous utilisons le lambda-calcul simplement typé.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), <http://jfla.inria.fr/2015>
Liste complète des métadonnées


https://hal.inria.fr/hal-01099138
Contributeur : David Baelde <>
Soumis le : mercredi 31 décembre 2014 - 15:44:25
Dernière modification le : lundi 5 octobre 2015 - 17:01:53
Document(s) archivé(s) le : mercredi 1 avril 2015 - 10:26:26

Fichier

jfla15_submission_31.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01099138, version 1

Collections

Citation

Pierre-Évariste Dagand, Gabriel Scherer. Normalization by realizability also evaluates. David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), <http://jfla.inria.fr/2015>. <hal-01099138>

Partager

Métriques

Consultations de
la notice

157

Téléchargements du document

105