A unified treatment of syntax with binders

Abstract : Atoms and de Bruijn indices are two well-known representation techniques for data structures that involve names and binders. However, using either technique, it is all too easy to make a programming error that causes one name to be used where another was intended. We propose an abstract interface to names and binders that rules out many of these errors. This interface is implemented as a library in Agda. It allows defining and manipulating term representations in nominal style and in de Bruijn style. The programmer is not forced to choose between these styles: on the contrary, the library allows using both styles in the same program, if desired. Whereas indexing the types of names and terms with a natural number is a well-known technique to better control the use of de Bruijn indices, we index types with worlds. Worlds are at the same time more precise and more abstract than natural numbers. Via logical relations and parametricity, we are able to demonstrate in what sense our library is safe, and to obtain theorems for free about world-polymorphic functions. For instance, we prove that a world-polymorphic term transformation function must commute with any renaming of the free variables. The proof is entirely carried out in Agda.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (4--5), pp.614--704. 〈10.1017/S0956796812000251〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00772721
Contributeur : François Pottier <>
Soumis le : vendredi 11 janvier 2013 - 09:19:16
Dernière modification le : vendredi 11 janvier 2013 - 14:31:58
Document(s) archivé(s) le : samedi 1 avril 2017 - 03:41:35

Fichier

pouillard-pottier-unified.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Nicolas Pouillard, François Pottier. A unified treatment of syntax with binders. Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (4--5), pp.614--704. 〈10.1017/S0956796812000251〉. 〈hal-00772721〉

Partager

Métriques

Consultations de
la notice

125

Téléchargements du document

131