Write a Blog >>

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

POPL-2020-tutorialfest
14:00 - 15:05: TutorialFest - Proving Semantic Type Soundness in Iris (I) at TutorialFest-A
POPL-2020-tutorialfest14:00 - 15:05
Tutorial
Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven
POPL-2020-tutorialfest
15:35 - 17:35: TutorialFest - Proving Semantic Type Soundness in Iris (II) at TutorialFest-A
POPL-2020-tutorialfest15:35 - 17:35
Tutorial
Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven