Lecture 10: Classical Logic and Continuations
Channel: Neelakantan Krishnaswami
Date: 2020-10-26

This lecture continues the development of the proof term assignment for classical logic, and explores how it can be embedded into intuitionistic logic via double-negation translations. It also shows how to extend the STLC with first-class continuations, and how to embed that into the STLC without continuations.