Lambda the Ultimate

I had a session with Oleg at POPL this year trying to understand the shift/reset control operators and particularly the printf examples of Danvy & Filinski and Asai & Kameyama. Late night thinkings ensued and now I can say I understand this thing a bit better. I've documented the whole development in Coq and Oleg reviewed it now so it should be mostly free of errors. I hope others could be enlightened by this development, it also shows some nice features of programming in dependently-typed languages like Coq, notably having proofs of the actual laws of your structures or writing functions at the type level. Enjoy this fine bit of type theory !

Genuine shift reset