Relating nominal and higher-order abstract syntax specifications

Abstract : Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the N-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda-conversion, raising, and the nabla-quantifier. This paper aims to unify these communities and provide a concrete correspondence between their different devices. In particular, we develop a semantics-preserving translation from alpha Prolog, a nominal abstract syntax based logic programming language, to G−, a higher-order abstract syntax based logic programming language. We also discuss higher-order judgments, a common and powerful tool for specifications with higher-order abstract syntax, and we show how these can be incorporated into G−. This establishes G− as a language with the power of higher-order abstract syntax, the fine-grained variable control of nominal specifications, and the desirable properties of higher-order judgments.
Type de document :
Communication dans un congrès
Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming, Jul 2010, Hagenberg, Austria. 2010
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00772522
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 15:59:17
Dernière modification le : jeudi 10 mai 2018 - 02:06:01
Document(s) archivé(s) le : samedi 1 avril 2017 - 03:37:46

Fichier

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

Identifiants

  • HAL Id : hal-00772522, version 1

Collections

Citation

Gacek Andrew. Relating nominal and higher-order abstract syntax specifications. Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming, Jul 2010, Hagenberg, Austria. 2010. 〈hal-00772522〉

Partager

Métriques

Consultations de la notice

131

Téléchargements de fichiers

63