Type-safe printf using delimited continuations, in Coq

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

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


By the way, what's the status of Russell? :-)

Russell status

It's now quite robust and can be used for all sorts of things. It's also pretty well integrated with the Coq environment. I use it to neatly define the Show instance for naturals in Show.v. It's used by quite a lot of people now, but I'm still reluctant to say it's not experimental because in some ways it really is.


That's excellent news. So, color me dense, but: how/where can I download, install, and play with it?

Coq version

You may have flavors of Russell since 8.1 along with Coq, but the real stuff is still in the trunk version, to appear as 8.2 soon. Beware: you need subversion, ocaml 3.9 or 3.10+camlp5 and GNU make 3.81 to compile the trunk these days.

Coq 8.2

Any idea how soon "soon" is? :-)

soon is...

mid-february most likely. I will push for a dev version release at this date at least.

Excellent, A double wammy!

Congratulations on explicating something like delimited continuations while producing a useful piece of software.

hmmm, I wouldn't mind a nice parsec style parser in Coq...

I don't know how "parsec-style" it is...

...but see here for a Coq development that includes a parser so that you can play with tiny programs written in a language whose semantics have been defined in Coq. It's quite painful in practice, but it exists.