Types for relaxed memory models
Matthew A. Goto, Radha Jagadeesan, Corin Ptcher, James Riely · 2012
Multicore computers implementing weak memory models are mainstream, yet type-based analyses of these models remain rare. We help fill this gap. We not only prove the soundness of a type system for a weak execution model, but we also show that interesting properties of that model can be embedded in the types themselves.