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.