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.