Mechanized metatheory revisited

Proof assistants and the programming languages that implement them need to deal with a range of expressions that involve bindings. Many mature proof assistants have been extended with various packages and libraries so that bindings are addressed using various techniques (e.g., de Bruijn numerals and nominal logic). I argue here, however, that bindings are such an intimate aspect of the structure of expressions that they should be accounted for directly in the under-lying programming language support for proof assistants. High-level and semantically elegant programming language support can be found in rather old and familiar concepts. In particular, Church’s Simple Theory of Types has long ago provided answers to how bindings interact with logical connectives and quantifiers. Similarly, the proof search interpretation of Gentzen’s proof theory provides a rich model of computation that supports bindings. I outline several principles for dealing computationally with bindings that follow from their treatments in quantificational logic and sequent calculus. I also briefly describe some implementations of these principles that have helped to validate their effectiveness as computational principles. 1 Mechanization of meta theor