Soundness of the simply typed lambda calculus in ACL2

To make it practical to mechanize proofs in programming language metatheory, several capabilities are required of the theorem proving framework. One must be able to represent and efficiently reason about complex recursively-defined expressions, define arbitrary induction schemes including mutual inductions over several objects and inductions over derivations, and reason about variable bindings with minimal overhead. We introduce a method for performing these proofs in ACL2, including a macro which automates the process of defining functions and theorems to facilitate reasoning about recursive data types. To illustrate this method, we present a proof in ACL2 of the soundness of the simply typed λ-calculus.

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Sol Swords, William R. Cook
• Keywords: ACL2 2006, Arbitrary Induction Schemes, Complex Recursively-defined Expressions, Computational Linguistics, Theorem Proving Framework