Freddie Agestam: Interpretations of Classical Logic Using λ-calculus

Lambda calculus was introduced in the 1930s as a computation model. It was later shown that the simply typed lambda-calculus has a strong connection to intuitionistic logic, via the Curry-Howard correspondence. When the type of a lambda-term is seen as a proposition, the term itself corresponds to a proof, or construction, of the object the proposition describes.

In the 1990s, it was discovered that the correspondence can be extended to classical logic, by enriching the lambda-calculus with control operators found in some functional programming languages such as Scheme. These control operators operate on abstractions of the evaluation context, so called continuations. These extensions of the lambda-calculus allow us to find computational content in non-constructive proofs.

Most studied is the lambda-mu-calculus, which we will focus on, having several interesting properties. Here it is possible to define catch and throw operators. The type constructors AND and OR are definable from only IMPLIES and FALSE. Terms in lambda-mu-calculus can be translated to lambda-calculus using continuations.

In addition to presenting the main results, we go to depth in understanding control operators and continuations and how they set limitations on the evaluation strategies. We look at the control operator C, as well as call/cc from Scheme. We find lambda-mu-calculus and C equivalents in Racket, a Scheme implementation, and implement the operators AND and OR in Racket. Finally, we find and discuss terms for some classical propositional tautologies.

Supervisor: Erik Palmgren