Write a Blog >>
Mon 20 Jan 2020 14:00 - 15:05 at Muses - Proving Semantic Type Soundness in Iris (I)
Mon 20 Jan 2020 15:35 - 17:35 at Muses - Proving Semantic Type Soundness in Iris (II)

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

Talk Slides (talk-iristutorial20.pdf)19.34MiB

Mon 20 Jan

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