Using the Adelfa Proof Assistant to Construct Proofs of Programming Language Properties

Abstract

In this thesis, we demonstrate stating and proving properties of a programming language using a dependently typed lambda calculus called LF and a system called Adelfa which provides mechanized support for reasoning about statements concerning typing derivations in LF. Proving properties in this manner allows the proofs to be undertaken using a formal logic, and builds greater trust in the proofs because the details of the steps are checked mechanically. The property that we consider in our demonstration is subject reduction for the Simply Typed Lambda Calculus. The Simply Typed Lambda Calculus is the theoretical foundation for many important programming languages and more complex lambda calculi, and subject reduction is a nontrivial properties with important equivalents in these more complex systems. Therefore, this proof constitutes a nontrivial demonstration of the usefulness of LF and Adelfa for proving properties of programming languages.