The notes for a short talk given on Iris in a seminar on concurrent separation logic at Carnegie Mellon. - View it on GitHub