  Safe, shared-memory interoperability between languages with different type
systems and memory-safety guarantees is an intricate problem as crossing
language boundaries may result in memory-safety violations. In this paper, we
present RichWasm, a novel richly typed intermediate language designed to serve
as a compilation target for typed high-level languages with different
memory-safety guarantees. RichWasm is based on WebAssembly and enables safe
shared-memory interoperability by incorporating a variety of type features that
support fine-grained memory ownership and sharing. RichWasm is rich enough to
serve as a typed compilation target for both typed garbage-collected languages
and languages with an ownership-based type system and manually managed memory.
We demonstrate this by providing compilers from core ML and L3, a type-safe
language with strong updates, to RichWasm. RichWasm is compiled to regular
Wasm, allowing for use in existing environments. We formalize RichWasm in Coq
and prove type safety.
