Higher-order abstract syntax in classical higher-order logic

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.