Higher-order abstract syntax; Induction; Logical Frameworks; Abstract syntax; Axiomatic approach; Induction principles; Recursion operators

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 algebras, presented in higher-order abstract syntax (HOAS). is based on an axiomatic syntactic standpoint and it consists of …