Proving Semantic Type Soundness in Iris

Robbert Krebbers

Date: Wed, April 08, 2020
Time: 12:00
Room: Eelco's Zoom Room

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 is joint work with Amin Timany, Derek Dreyer, and Lars Birkedal.

Previous: Arjen Rouvoet |
Next: Jasper Denkers |