A relational model of types-and-effects in higher-order concurrent separation logic
Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal · 2016
Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating whole classes of bugs, statically tracking effects opens the door to advanced compiler optimizations.