Derek's Foundations of Programming group
A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.
Logically Atomic Triples in Iris
Coq development for the Semantics course taught at Saarland University