A Two-Level Logic Approach to Reasoning about Typed Specification Languages

Mary Southern 1 Kaustuv Chaudhuri 2
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 : The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.
Type de document :
Communication dans un congrès
Venkatesh Raman and S. P. Suresh. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), Dec 2014, New Delhi, India. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 29, 2014, 〈http://www.fsttcs.org/〉. 〈10.4230/LIPIcs.FSTTCS.2014.557〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01091544
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 5 décembre 2014 - 15:52:46
Dernière modification le : jeudi 10 mai 2018 - 02:06:53
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:04:14

Fichiers

abella-lf-hal.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Collections

Citation

Mary Southern, Kaustuv Chaudhuri. A Two-Level Logic Approach to Reasoning about Typed Specification Languages. Venkatesh Raman and S. P. Suresh. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), Dec 2014, New Delhi, India. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 29, 2014, 〈http://www.fsttcs.org/〉. 〈10.4230/LIPIcs.FSTTCS.2014.557〉. 〈hal-01091544〉

Partager

Métriques

Consultations de la notice

386

Téléchargements de fichiers

76