[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Dear all, we are pleased to announce a release of CompCertTSO, a certified compiler from a multithreaded C-like language with a TSO relaxed memory model to x86 assembly language with a realistic x86-TSO memory model; the development builds on CompCert. The code, documentation, and papers are available here: http://www.cl.cam.ac.uk/~pes20/CompCertTSO/ They build with Coq 8.3pl1 and OCaml 3.12.0. Any comments would be very welcome. Jaroslav, Viktor, Francesco, Suresh, and Peter