present a logical framework Upsilon for reasoning on a very
general class of languages featuring binding operators, called
algebras, presented in higher-order abstract syntax (HOAS).
Upsilon is based on an axiomatic syntactic standpoint and it
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
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