An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS

We present a logical framework Υ for reasoning on a very general class of languages featuring binding operators, called nominal , 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.

• Type: Conference
• Year: 2001
• Where: ICALP
• Authors: Furio Honsell, Marino Miculan, Ivan Scagnetto
• Keywords: Axiomatic Syntactic Standpoint, Binding Operators, ICALP 2001, Logical Framework, Programming Languages