All the Languages Together
summary
Proposes a proof technique that builds a semantic intermediate representation (logical relations of source types as sets of target terms) to verify FFI glue code: compilers erase types to a lambda-like IR, glue implements conversion wrappers (thunks plus flag ref cells for affine resources), and each conversion lemma is machine-checked using step‑indexed logical relations. Delivers three case studies (ML↔affine, pairwise conversions, GC↔manual memory L3/Rust), proves conversion soundness, notes runtime thunking cost and a static analysis to remove checks, and prototypes a Rich Wasm typed IR for practical use.
AI-written summary · about
chapters (21)
- 0:00Introduction
- 1:49Language interoperability matters
- 3:13Type soundness with FFIs
- 5:41Multilanguage semantics
- 8:47FFI implementations today
- 9:52Verifying FFIs
- 15:29Framework case studies
- 17:41ML and affine language example
- 25:17Semantic models for types
- 33:04Proving FFI soundness
- 34:27Future work and language pairs
- 36:13Types in interoperability
- 41:09Safe encapsulation at boundaries
- 43:13Libraries across languages
- 45:41Linking types for encapsulation
- 46:03Secure compilation with IRs
- 48:12Lightweight safe interop
- 50:59WebAssembly for typed interop
- 52:44Unsafe languages like C
- 54:30Shared-nothing WebAssembly interop
- 55:11Takeaways and research
related talks
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
40mFormal semantics for multi-language programs- 40mFormal semantics for multi-language programs
01h 02mPolyglot Programming through Foreign Function Interfaces
17mOvercoming Restraint: Composing Verification of Foreign Functions with Cogent
01h 02mLanguage Design meets Verifying Compilers
45mLogic Meta Programming for Functional Languages