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.
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
Book Part (author)
File in questo prodotto:
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

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/212930
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 36
  • ???jsp.display-item.citation.isi??? ND
social impact