Proving Semantic Type Soundness in Iris

Robbert Krebbers

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 | Demo of Intrinsically Typed Compilation of Imperative Code in Agda
Next: Jasper Denkers | Early Validation and Global Optimization for Parametric Manufacturing Systems