Series: Penn State Logic Seminar Date: Wednesday, August 11, 2004 Time: 11:10 AM - 12:25 PM Place: 317 Boucke Building Speaker: John J. Hannan, Penn State, Computer Science Title: An Introduction to Classical Logic as a Programming Language Abstract: Intuitionistic logics can be understood (via the Curry-Howard isomorphism) as type systems for functional programming languages. About 15 years ago this correspondence was been extended to classical logics and functional programming languages augmented with imperative control operators. Classical logic can be used as a total correctness type theory for such languages. One of the basic principles behind this work is the embedding of classical logic into intuitionistic logic. Although there exist formulas that are provable classically but not intuitionistically, there are several ways of embedding classical logic into intuitionistic logic. We present one such embedding, a double-negation translation, and present its correctness proof. We then briefly consider how this result relates to control operators and continuation passing style (CPS) translations.