Type soundness is commonly proved using the syntactic approach, i.e. by proving progress and preservation. This problem session is about another approach to type soundness, semantic type soundness. I will explain the differences between syntactic typing and semantic typing, and show a high level idea of how to prove type soundness using the semantic approach, as well as how recent developments in Iris address the complexity of previous semantic type soundness proofs based on logical relations. In the end of the session, I will discuss how those results can be applied to our research, in particular the full iso-recursive type system I am working on. The contents of this problem session are mainly based on the paper “A Logical Approach to Type Soundness”.

Note: the problem session starts at 11am, not 10am as usual.