PRL Seminars

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.