Programming and Proving with Classical Types

Abstract

The propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed $\lambda$-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigot’s $\lambda \mu$-calculus. In this work, we use the $\lambda \mu$-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value $\lambda \mu$-calculus with a type system in correspondence with full classical logic. We extend the language with polymorphic types, add a host of data types in ‘direct style’, and prove several metatheoretical properties. All of our proofs and definitions are mechanised in Isabelle/HOL, and we automatically obtain an interpreter for a system of proof terms cum programming language—called $\mu$ML—using Isabelle’s code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover—called $\mu$TP—for classical first-order logic, capable of synthesising $\mu$ML programs from completed tactic-driven proofs. We present example closed $\mu$ML programs with classical tautologies for types, including some inexpressible as closed programs in the original $\lambda \mu$-calculus, and some example tactic-driven $\mu$TP proofs of classical tautologies.