User loginNavigation |
Programming a compiler with a proof assistant
Xavier Leroy's contribution to POPL'06 is Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, which describes a fairly realistic mini-compiler from a subset of C, called Cminor, to PPC assembler.
So what? It's written entirely in Coq, which pretty much makes a certified compiler for free, and all done in a particularly easy way to leverage if you want to show particular implementations correct. He's got a resource page up with the implementation (which he calls CompCert), and some further notes. |
Browse archives
Active forum topics |
Recent comments
13 weeks 6 days ago
13 weeks 6 days ago
13 weeks 6 days ago
36 weeks 20 hours ago
40 weeks 2 days ago
41 weeks 6 days ago
41 weeks 6 days ago
44 weeks 4 days ago
49 weeks 2 days ago
49 weeks 2 days ago