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 archivesActive forum topics |
Recent comments
12 min 57 sec ago
54 min 8 sec ago
1 hour 17 min ago
2 hours 20 min ago
2 hours 31 min ago
7 hours 59 min ago
11 hours 23 min ago
15 hours 15 min ago
19 hours 34 min ago
22 hours 47 min ago