[ 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:


They build with Coq 8.3pl1 and OCaml 3.12.0.    Any comments would be
very welcome.

Jaroslav, Viktor, Francesco, Suresh, and Peter

Reply via email to