An axiomatic approach to metareasoning on nominal algebras in HOAS

Abstract

We present a logical framework for reasoning on a very general class of languages featuring binding operators, called nominal algebras, presented in higher-order abstract syntax (HOAS). is based on an axiomatic syntactic standpoint and it consists of a simple types theory a 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. © 2011 Springer-Verlag Berlin Heidelberg.