Semantic Intermediate Representations for Sound Language Interoperability
summary
Claim: build semantic IRs — logical relations that map each source type to a set of target terms — to prove interoperability after compilation. Implementation: compilers to an untyped lambda VM, three PLDI 2022 case studies (shared mutable refs, affine vs unrestricted via thunked affine wrappers and flag cells, ML↔low-level Rust-like memory), and runtime conversion soundness proofs showing no runtime type errors (conversion errors allowed). Result: conversions are proved sound, checks impose runtime cost, and optimizations save checks for statically safe values.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:04Sound language interoperability proofs
- 3:27Multi-language semantics limits
- 7:42Semantic intermediate representations
- 10:48Convertibility rules and conversions
- 13:57PLDI 22 case studies
- 18:00Mini ML and Affy interoperability
- 27:32Function type conversions
- 35:32Logical relations and semantic IR
- 45:04Conversion soundness and type safety
- 45:45Runtime checks for affine functions
- 47:30Future work and cases
- 48:11Type meaning across languages
- 53:13Stateful behavior in pure code
- 58:13Secure compilation soundness
- 1:01:27Building semantic IR challenges
- 1:03:33Conclusion
related talks
01h 05mAll the Languages Together
20mMimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
40mFormal semantics for multi-language programs
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
27mR Melts Brains -- An IR for First-Class Environments and Lazy Effectful Arguments- 40mFormal semantics for multi-language programs