Programming and Proving with Classical Types

摘要

The propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed λ-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 λμ-calculus. In this work, we use the λμ-calculus as the foundation for a system of proof terms for classical first-order logic. In particular, we define an extended call-by-value λμ-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 /iML- using Isabelle's code generation mechanism. Atop our proof terms, we build a prototype LCF-style interactive theorem prover—called /xTP- for classical first-order logic, capable of synthesising μML programs from completed tactic-driven proofs. We present example closed /xML programs with classical tautologies for types, including some inexpressible as closed programs in the original λμ-calculus, and some example tactic-driven μTP proofs of classical tautologies.