An Introduction to Iris: Higher-Order Concurrent Separation Logic (Version intégrée)