Formal semantics for multi-language programs
summary
Presents a concrete recipe: add typed boundaries between two languages, run each fragment with its own operational semantics, and convert values at the boundary using either the lump embedding or the natural embedding (wrapper functions via higher‑order contracts); proves type soundness and shows conversion strategies for errors. Tools include formal operational semantics, logical relations and compiler‑level case studies (Funel, RichWasm); the method enables verified linking and compiler correctness but fully verified, practical FFIs remain an open problem.
AI-written summary · about
chapters (16)
- 0:00Multi-language semantics intro
- 1:50Formal semantics for interoperability
- 3:36Core recipe for multi-language semantics
- 6:04ML and Scheme mechanics demo
- 7:53Lump embedding: opaque values
- 11:22Natural embedding: value conversion
- 16:21Errors across language boundaries
- 18:51Verified FFI open problems
- 22:04Assembly and high-level semantics
- 24:30Compiler correctness with multi-language
- 28:04Source semantics to glue code
- 34:06Paper’s simplicity benefits
- 35:31Q&A: Integer conversions
- 36:34Q&A: Round-trip conversions
- 37:14Q&A: Memory models
- 38:59Q&A: WebAssembly future
related talks
40mFormal semantics for multi-language programs
01h 05mAll the Languages Together
20mOn Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
16mExtrinsically Typed Operational Semantics for Functional Languages
31mProgramming Languages Must Have Formal Semantics. Period.
19mA Pure Demand Operational Semantics with Applications to Program Analysis
15mSemantics of Sets of Programs
16mTowards formally secure compilation of verified F* programs against unverified ML(…)