Tracking Data-Flow with Open Closure Types

Résumé : Les systèmes de types habituels pour le lambda-calcul cachent les variables capturées par une fermeture, et ce dès sa création. À un point donné du programme, il est en fait possible de mentionner certaines de ces variables, celles qui sont toujours présentes dans l'environnement lexical de typage. Ce raffinement des types de fermetures, plus ''ouverts'' car mentionnant le contexte qui les entoure, est désirable pour certaines applications des systèmes de types à l'analyse de programmes. Cet article introduit formellement de tels types ouverts de fermetures, pour mettre à plat leur traitement théorique recélant quelques difficultés techniques: le type d'une fermeture mentionne ses dépendances sur le contexte, et varie donc selon les différents point du programme. En guise d'exemple, ils sont utilisés pour garder trace des informations de typage de flots de données induits par la capture des valeurs de l'environnement dans les fermetures. Un prototype d'implémentation de ce système de types est publiquement disponible.
Type de document :
Communication dans un congrès
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR- 19th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, Dec 2013, Stellenbosch, South Africa. Springer Verlag, 8312, pp.710-726, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00911656
Contributeur : Scherer Gabriel <>
Soumis le : vendredi 29 novembre 2013 - 15:41:26
Dernière modification le : mercredi 29 juillet 2015 - 01:26:44
Document(s) archivé(s) le : lundi 3 mars 2014 - 20:01:11

Fichiers

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

Identifiants

  • HAL Id : hal-00911656, version 1
  • ARXIV : 1312.0018

Collections

Citation

Gabriel Scherer, Jan Hoffmann. Tracking Data-Flow with Open Closure Types. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR- 19th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, Dec 2013, Stellenbosch, South Africa. Springer Verlag, 8312, pp.710-726, 2013, Lecture Notes in Computer Science. 〈hal-00911656〉

Partager

Métriques

Consultations de
la notice

457

Téléchargements du document

331