In this tutorial we demonstrate how the Iris framework for concurrent separation logic can be used to prove type soundness of feature-rich, realistic languages, using the "semantic approach'' to type soundness. Contrary to the traditional “syntactic approach” of progress and preservation, the semantic approach has several advantages in terms of reasoning about data abstraction and unsafe features. We show that the semantic approach leads to clear and concise proofs that can be effectively mechanized using the implementation of Iris in the Coq proof assistant.

The tutorial will consist of the following parts:

1. Introduction to logical relations in Iris
2. Mechanization of logical relations in Iris in Coq
3. Hands-on session

For the hands-on session it is recommended to come with Coq and Iris pre-installed on your machine so that you can play with Iris yourself. For this you need the latest version of Iris master, which can be obtained from https://gitlab.mpi-sws.org/iris/iris/tree/446bc64428ce0c7bce4b82b53d93546a0e60f114

The tutorial material can be downloaded from https://gitlab.mpi-sws.org/iris/tutorial-popl20