Semantical analysis of higher-order abstract syntax
Martin O. Hofmann · 2003
A functor category semantics for higher-order abstract syntax is proposed with the following aims: relating higher order and first order syntax, justifying induction principles, suggesting new logical principles to reason about higher-order syntax.