Semantic Encapsulation Using Linking Types

Explore a 26-minute video presentation from the TyDe 2023 conference on Semantic Encapsulation using Linking Types. Delve into the challenges of language interoperability and the preservation of safety invariants when linking different programming languages. Learn about a novel approach that encapsulates foreign code soundly, introducing linking types to characterize behaviors inexpressible in the core language. Discover how realizability models can be used to prove the soundness of linking and how compiler-inserted wrappers can automatically ensure encapsulation. Examine case studies extending a pure functional language with state and exceptions, demonstrating the implementation of mutable references and try-catch mechanisms as library functions. Gain insights into type soundness, semantics, and logical relations in the context of language interoperability.

[TyDe'23] Semantic Encapsulation using Linking Types