Proofs in continuation-passing style
Danko Ilik · 2014
While writing programs in continuation-passing style (CPS) is a common technique from Programming Languages research, writing mathematical proofs in CPS is much less common. Although such proofs open new possibilities for writing constructive proofs (for cases where more direct CPS-less proofs are not known, like in this tutorial), working with them is delicate (instead of data, we manipulate functionals). Proof assistants come to our rescue.