Formal Continuations and Classical Logic

by Karl Crary
1996-1997

I will be discussing formalized continuations in type theory and how they can be used to interpret classical proofs as programs and to construct "psuedo-constructive" oracles. As time permits, I will show how a CPS (continuation passing style) translation can be used in some cases to convert these classical proofs to constructive proofs.

The results to be presented are largely the work of Griffin, Murthy, Felleisen and Friedman.

Formal Continuations and Classical Logic

by Karl Crary 1996-1997

by Karl Crary
1996-1997