(eng) Higher order abstract syntax is a natural way to formalize programming languages with binders, like the pi-calculus, because alpha-conversion and beta-reduction are delegated to the meta level of the provers, making ...