The Curry-Howard isomorphism: A study of the computational content of intuitionistic and classical logic

Abstract

The Curry-Howard isomorphism relates systems of formal logic to models of computation. It broadly states that proofs correspond to programs and formulae to types. For a long time it was believed the correspondence merely applied to intuitionistic logic. This changed when the axioms of classical logic were found to correspond to control operators. The correspondence is an important theoretical result connecting logic and computer science, but also has practical implications in e.g. program verification. This thesis will discuss the isomorphism with respect to both intuitionistic and classical logic. First, a language for the intuitionistic part of the correspondence will be constructed and assigned meaning by an operational semantics. These constructs will be used for exploring various aspects of the isomorphism, such as continuations and the relation between normalization and reduction. Subsequently, the language will be extended for a correspondence with classical logic by adding a control operator based on Peirce's law. The computational effects of this operator will be analysed and compared with other possible control operators, which arise from different classical axioms --i.e. a generalised version of Peirce's law, double negation elimination and the law of excluded middle. The correspondence will be shown to relate double negation embeddings of classical logic into intuitionistic logic to CPS translations. Finally, the complete language and semantics will be proven to have the properties of determinism, progress, preservation and termination.