Formal semantics for multi-language programs
summary
Claims that a 2007 recipe gives a practical operational semantics for linking two source languages by adding typed boundaries and two concrete mechanisms: the lump embedding that passes opaque handles and the natural embedding that generates wrappers to convert values and functions (higher‑order contract style). Paper proves type soundness, shows conversions for errors via richer conversion strategy labels, and enables later work on compiler correctness, secure compilation, FunEL (typed assembly interop) and RichWasm; verified FFIs for real languages remain unresolved.
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
26mSemantic Encapsulation using Linking Types
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
16mExtrinsically Typed Operational Semantics for Functional Languages
15mSemantics of Sets of Programs
31mProgramming Languages Must Have Formal Semantics. Period.
19mA Pure Demand Operational Semantics with Applications to Program Analysis