Combining Higher Order Abstract Syntax (HOAS) and induction is well known to be problematic. We have implemented a tool called Hybrid, within Isabelle HOL, which does allow object logics to be represented using HOAS, and reasoned about using tactical theorem proving in general and principles of (co)induction in particular. In this paper we describe Hybrid, and illustrate its use with case studies. We also provide some theoretical adequacy results which underpin our practical work.
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction / S.J. Ambler, R.L. Crole, A. Momigliano (LECTURE NOTES IN COMPUTER SCIENCE). - In: Theorem Proving in Higher Order Logics / [a cura di] A. Carreño, A. Muñoz, S. Tahar. - [s.l] : Springer, 2002. - ISBN 978-3-540-44039-0. - pp. 13-30 (( Intervento presentato al 15. convegno TPHOLs tenutosi a Hampton nel 2002 [10.1007/3-540-45685-6_3].
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction
A. Momigliano
Ultimo
2002
Abstract
Combining Higher Order Abstract Syntax (HOAS) and induction is well known to be problematic. We have implemented a tool called Hybrid, within Isabelle HOL, which does allow object logics to be represented using HOAS, and reasoned about using tactical theorem proving in general and principles of (co)induction in particular. In this paper we describe Hybrid, and illustrate its use with case studies. We also provide some theoretical adequacy results which underpin our practical work.File | Dimensione | Formato | |
---|---|---|---|
choasttpci.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
281.54 kB
Formato
Adobe PDF
|
281.54 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Ambler2002_Chapter_CombiningHigherOrderAbstractSy.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
263.01 kB
Formato
Adobe PDF
|
263.01 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.