User loginNavigation |
Type-safe printf using delimited continuations, in CoqI 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 ! By Matthieu Sozeau at 2008-01-23 15:05 | LtU Forum | previous forum topic | next forum topic | other blogs | 12674 reads
|
Browse archives
Active forum topics
|
Recent comments
2 weeks 2 days ago
3 weeks 4 hours ago
3 weeks 1 day ago
3 weeks 1 day ago
3 weeks 6 days ago
4 weeks 2 days ago
4 weeks 2 days ago
4 weeks 2 days ago
5 weeks 4 days ago
5 weeks 6 days ago