Reasoning About Higher-Order Relational Specifications

Yuting Wang 1 Kaustuv Chaudhuri 2 Andrew Gacek 3 Gopalan Nadathur 1
1 Department of Computer Science and Engineering [Minneapolis]
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
3 Rockwell Collins
Abstract : The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dynamically changing sets of assumptions and that is key to encoding side conditions and contexts that occur frequently in structural operational semantics (SOS) style presentations. Specifications are often useful in reasoning about the systems they describe. The Abella theorem prover supports such reasoning by explicitly embedding the specification logic within a rich reasoning logic; specifications are then reasoned about through this embedding. However, realizing an induction principle in the face of dynamically changing assumption sets is nontrivial and the original Abella system uses only a subset of the HH specification logic for this reason. We develop a method here for supporting inductive reasoning over all of HH. Our approach takes advantage of a focusing property of HH to isolate the use of an assumption and the ability to finitely characterize the structure of any such assumption in the reasoning logic. We demonstrate the effectiveness of these ideas via several specification and meta-theoretic reasoning examples that have been implemented in an extended version of Abella.
Type de document :
Communication dans un congrès
Tom Schrijvers. International Symposium on Principles and Practice of Declarative Programming, Sep 2013, Madrid, Spain. ACM, 2013, 〈10.1145/2505879.2505889〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00787126
Contributeur : Kaustuv Chaudhuri <>
Soumis le : dimanche 4 août 2013 - 21:19:12
Dernière modification le : mercredi 23 janvier 2019 - 10:29:23
Document(s) archivé(s) le : mercredi 5 avril 2017 - 19:23:50

Fichiers

hhw-arxiv.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIX | X | PARISTECH | X-LIX | X-DEP-INFO

Citation

Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur. Reasoning About Higher-Order Relational Specifications. Tom Schrijvers. International Symposium on Principles and Practice of Declarative Programming, Sep 2013, Madrid, Spain. ACM, 2013, 〈10.1145/2505879.2505889〉. 〈hal-00787126v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

560

Téléchargements de fichiers

332

Contact


archive-ouverte@inria.fr