Home » forums » LtU Forum

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

By Matthieu Sozeau at 2008-01-23 15:05 | LtU Forum | previous forum topic | next forum topic | other blogs | 13187 reads

Comment viewing options

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

Nice!

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

By Paul Snively at Wed, 2008-01-23 18:22 | login or register to post comments

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.

By Matthieu Sozeau at Wed, 2008-01-23 19:27 | login or register to post comments

Great!

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

By Paul Snively at Wed, 2008-01-23 23:43 | login or register to post comments

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.

By Matthieu Sozeau at Thu, 2008-01-24 00:33 | login or register to post comments

Coq 8.2

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

By Paul Snively at Thu, 2008-01-24 14:01 | login or register to post comments

soon is...

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

By Matthieu Sozeau at Thu, 2008-01-24 14:36 | login or register to post comments

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...

By Gavin Mendel-Gleason at Thu, 2008-01-24 11:44 | login or register to post comments

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.

By Paul Snively at Thu, 2008-01-24 13:35 | login or register to post comments