Nominal Abstraction

Gacek Andrew 1 Dale Miller 2, 3 Gopalan Nadathur 4
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation between terms called nominal abstraction as a means for overcoming this deficiency. We incorporate nominal abstraction into a rich logic also including definitions, generic quantification, induction, and co-induction that we then prove to be consistent. We present examples to show that this logic can provide elegant treatments of binding contexts that appear in many proofs, such as those establishing properties of typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.
Type de document :
Article dans une revue
Journal of Information and Computation, Elsevier, 2011, 209 (1), pp.48-73
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00772606
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 18:04:16
Dernière modification le : mercredi 25 avril 2018 - 10:45:27
Document(s) archivé(s) le : jeudi 11 avril 2013 - 04:08:38

Fichier

nominal-abstraction.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00772606, version 1

Collections

Citation

Gacek Andrew, Dale Miller, Gopalan Nadathur. Nominal Abstraction. Journal of Information and Computation, Elsevier, 2011, 209 (1), pp.48-73. 〈hal-00772606〉

Partager

Métriques

Consultations de la notice

270

Téléchargements de fichiers

83