Unmaintained repository. An extension of the Iris program logic to support linearity and fair refinement reasoning.