Article ID Journal Published Year Pages File Type
423738 Electronic Notes in Theoretical Computer Science 2008 9 Pages PDF
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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics