We present a logical framework Upsilon for reasoning on a very general class of languages featuring binding operators, called nominal algebras, presented in higher-order abstract syntax (HOAS). Upsilon is based on an axiomatic syntactic standpoint and it consists of a simple types theory à la Church extended with a set of axioms called the Theory of Contexts, recursion operators and induction principles. This framework is rather expressive and, most notably, the axioms of the Theory of Contexts allow for a smooth reasoning of schemata in HOAS. An advantage of this framework is that it requires a very low mathematical and logical overhead. Some case studies and comparison with related work are briefly discussed.

Keywords: higher-order abstract syntax, induction, logical frameworks.

The article is available as a PDF file.