Semantic Soundness for Language Interoperability
summary
Proves that linking heterogeneous languages is sound by building realizability models over a common untyped target and reasoning about the actual glue code that runs. Defines a declarative convertibility judgment inhabited by pairwise target translators and proves correctness. Delivers three case studies (five source languages, two untyped targets): safe pointer exchange requires isomorphic pointee types, affine↔unrestricted conversions validate dynamic checks, and moving linear-owned memory into a GC heap is safe without copying.
AI-written summary · about
chapters (12)
- 0:00Start
- 0:01Programs are multi-lingual
- 0:29Type soundness is important
- 1:37Multi-language boundary rules
- 1:54Multi-language operational semantics
- 4:22Boundaries are glue code
- 4:55A new (old) approach to soundness
- 5:471st part: realizability logical relation
- 6:422nd part: index by types in both languages
- 7:16Our models enable important interop questions
- 9:15Conversions realized by glue code
- 12:45Key takeaways
related talks
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
01h 05mAll the Languages Together
40mFormal semantics for multi-language programs
26mSemantic Encapsulation using Linking Types- 40mFormal semantics for multi-language programs
25mA Semantic Approach to Robust Property Preservation
16mA metalanguage for multi-phase modularity
27mTaming Unsoundness with Gradual Abstract Interpretation