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.
This program is tentative and subject to change.
Mon 20 Jan
|14:00 - 15:05|