Mechanized metatheory revisited

Proof assistants and the programming languages that imple-ment them need to deal with a range of linguistic expressions that involve bindings. Since most mature proof assistants do not have built-in methods to treat this aspect of syntax, they have been extended with various packages and libraries that allow them to encode such syntax using, for example, de Bruijn numerals and nominal logic features. I put forward the argument that bindings are such an intimate aspect of the structure of expressions that they should be accounted for di-rectly in the underlying programming language support for proof assistants and not as packages and libraries. One possi-ble approach to designing programming languages and proof assistants that directly supports such an approach to bindings in syntax is presented. The roots of such an approach can be found in the mobility of binders between the term-level bindings, formula-level bindings (quantifiers), and proof-level bindings (eigenvariables). In particular, by combining Church’s approach to terms and formulas (found in his Sim-ple Theory of Types) and Gentzen’s approach to sequent cal-culus proofs, we can learn how bindings can declaratively interact with the full range of logical connectives and quan-tifiers. I will also illustrate how that framework provides an intimate and semantically clean treatment of computation and reasoning with syntax containing bindings. Some im-plemented systems, which support this intimate and built-in treatment of bindings, will be briefly described