The purpose of this tutorial is to show how constructive proofs, that may seem to be not possible directly, can be carried out if one uses continuation passing style for writing the proofs. The case study will consist of three extensions of the simply typed lambda calculus: with sums, with delimited control, with higher-type primitive recursion.
To help us keep track of details, and still allow us to see the CPS structure of the proof, we will use the Agda proof assistant. Please install it and its standard library on your machine. If you prefer, you may download this ISO image of a Linux live CD containing Agda pre-installed, which you can than either copy on USB or DVD or run in a virtual machine using programs like Gnome Boxes, VirtualBox or VMWare.
Have a look at the slides from my presentation. The simplest example of NBE in Agda is KripkeCompleteness.agda.