A two-level logic approach to reasoning about computations

Andrew Gacek Dale Miller 1, 2 Gopalan Nadathur 3
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called G which represents relations over lambda-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in G. We also describe an interactive theorem prover called Abella that implements G and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2012, 49 (2), pp.241-273. 〈10.1007/s10817-011-9218-1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776208
Contributeur : Dale Miller <>
Soumis le : mardi 15 janvier 2013 - 11:25:53
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Identifiants

Collections

Citation

Andrew Gacek, Dale Miller, Gopalan Nadathur. A two-level logic approach to reasoning about computations. Journal of Automated Reasoning, Springer Verlag, 2012, 49 (2), pp.241-273. 〈10.1007/s10817-011-9218-1〉. 〈hal-00776208〉

Partager

Métriques

Consultations de la notice

276