Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-irisPOPL · 2015