Semantic Encapsulation using Linking Types
summary
Presents a concrete mechanism that lets a pure language safely link to foreign code by adding linking types that describe C‑like behaviors, proving soundness with a realizability model (logical relations that map source types to sets of untyped target terms), and automatically inserting encapsulation wrappers at compile time. Implements two case studies: mutable references via a library (memoized Fibonacci) and exceptions as library try/catch, compiles to an untyped target, and carries out formal proofs that the wrappers actually enforce the core language invariants.
AI-written summary · about
chapters (9)
- 0:00Semantic encapsulation intro
- 2:30FFI breaks type safety
- 5:41Linking types for foreign behavior
- 9:59Exception encapsulation
- 11:47Interoperability models
- 15:22Proving encapsulation
- 17:49Implementation steps
- 19:35Soundness with foreign code
- 21:27Q&A
related talks
40mFormal semantics for multi-language programs
01h 05mAll the Languages Together
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
50mA Type-Theoretic Framework for Certified Meta-programming- 40mFormal semantics for multi-language programs
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
16mA metalanguage for multi-phase modularity
19mExtensible Metatheory Mechanization via Family Polymorphism