Logical frameworks supporting higher-order abstract syntax (HOAS) allow a direct and concise specification of a wide variety of languages and deductive systems. Reasoning about such systems within the same framework is well-known to be problematic. We describe the new version of the Hybrid system, implemented on top of Isabelle/HOL (as well as Coq), in which a de Bruijn representation of λ-terms provides a definitional layer that allows the user to represent object languages in HOAS style, while offering tools for reasoning about them at the higher level. We briefly describe how to carry out two-level reasoning in the style of frameworks such as Linc, and briefly discuss our system's capabilities for reasoning using tactical theorem proving and principles of induction and coinduction.
Two-level hybrid : a system for reasoning using higher-order abstract syntax / A. Momigliano, A.J. Martin, A.P. Felty. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 196:C(2008 Jan), pp. 85-93. [10.1016/j.entcs.2007.09.019]
Two-level hybrid : a system for reasoning using higher-order abstract syntax
A. MomiglianoPrimo
;
2008
Abstract
Logical frameworks supporting higher-order abstract syntax (HOAS) allow a direct and concise specification of a wide variety of languages and deductive systems. Reasoning about such systems within the same framework is well-known to be problematic. We describe the new version of the Hybrid system, implemented on top of Isabelle/HOL (as well as Coq), in which a de Bruijn representation of λ-terms provides a definitional layer that allows the user to represent object languages in HOAS style, while offering tools for reasoning about them at the higher level. We briefly describe how to carry out two-level reasoning in the style of frameworks such as Linc, and briefly discuss our system's capabilities for reasoning using tactical theorem proving and principles of induction and coinduction.File | Dimensione | Formato | |
---|---|---|---|
martin.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
162.9 kB
Formato
Adobe PDF
|
162.9 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.