howe@scs.carleton.ca Higher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to classical higherorder logic that supports HOAS. The logic we work with is the core of the logics employed in the widely used systems HOL and Isabelle/HOL. The extension adds recursive types, and a new type constructor for parametric functions. Using these additions, we can solve, for example, the archetypal recursive type equation for a HOAS representation of the syntax of the untyped lambdacalculus: T = (T - T) + (T, ! T), where the function type is the new parametric one. The usual HOAS induction principles can be derived. The bulk of the technical development in the paper is a semantics of the new logic, extending the usual set-theoretic semantics of classical higher-order logic. Copyright

Additional Metadata
Keywords Higher-order abstract syntax, Induction, Interactive theorem proving, Logical frameworks, Namebinding
Persistent URL dx.doi.org/10.1145/1577824.1577826
Conference 4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009
Citation
Howe, D. (2009). Higher-order abstract syntax in classical higher-order logic. Presented at the 4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009. doi:10.1145/1577824.1577826