Combining Higher Order Abstract Syntax (HOAS) and (co)induction is well known to be problematic. In previous work [1] we have described the implementation of a tool called Hybrid, within Isabelle HOL, which allows object logics to be represented using HOAS, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such FOλΔNand Twelf. By explicitly referencing provability, we solve the problem of reasoning by (co)induction in presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications. We demonstrate the method by formally verifying the correctness of a compiler for (a fragment) of Mini-ML, following [10]. To further exhibit the flexibility of our system, we modify the target language with a notion of non-well-founded closure, inspired by Milner & Tofte [16] and formally verify via co-induction a subject reduction theorem for this modified language.
Multi-level Meta-reasoning with Higher-Order Abstract Syntax / A. Momigliano, S.J. Ambler (LECTURE NOTES IN COMPUTER SCIENCE). - In: Foundations of Software Science and Computation Structures / [a cura di] A.D. Gordon. - [s.l] : Springer, 2003. - ISBN 978-3-540-00897-2. - pp. 375-391 (( convegno International Conference, FOSSACS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 tenutosi a Warsaw nel 2003 [10.1007/3-540-36576-1_24].
Multi-level Meta-reasoning with Higher-Order Abstract Syntax
A. Momigliano
Primo
;
2003
Abstract
Combining Higher Order Abstract Syntax (HOAS) and (co)induction is well known to be problematic. In previous work [1] we have described the implementation of a tool called Hybrid, within Isabelle HOL, which allows object logics to be represented using HOAS, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such FOλΔNand Twelf. By explicitly referencing provability, we solve the problem of reasoning by (co)induction in presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications. We demonstrate the method by formally verifying the correctness of a compiler for (a fragment) of Mini-ML, following [10]. To further exhibit the flexibility of our system, we modify the target language with a notion of non-well-founded closure, inspired by Milner & Tofte [16] and formally verify via co-induction a subject reduction theorem for this modified language.File | Dimensione | Formato | |
---|---|---|---|
10.1.1.201.6792.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
237.67 kB
Formato
Adobe PDF
|
237.67 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Momigliano-Ambler2003_Chapter_Multi-levelMeta-reasoningWithH.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
253.45 kB
Formato
Adobe PDF
|
253.45 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.