Sciweavers

ICALP
2001
Springer

An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS

14 years 2 months ago
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.
Furio Honsell, Marino Miculan, Ivan Scagnetto
Added 29 Jul 2010
Updated 29 Jul 2010
Type Conference
Year 2001
Where ICALP
Authors Furio Honsell, Marino Miculan, Ivan Scagnetto
Comments (0)