Formal semantics for multi-language programs

Multi-language programs are ubiquitous and language designers have long been designing programming languages to support interoperability. We've had platforms such as .NET, JVM, and COM that facilitate interoperability, and languages such as Scala, F#, SML.NET, and many more that treat it as a central design feature. In a 2007 paper, Matthews and Findler pointed out that most multi-language research was focused almost exclusively on how to implement interoperability efficiently and not on the quite subtle semantics of these features. They presented a multi-language semantics framework that gives language designers a methodology for taking two languages, adding interoperability boundaries between them, and giving an operational semantics to those boundaries. I'll describe the mechanics of multi-language semantics, how they support reasoning about the behavior of mixed-language programs, and discuss the impact that this tool has had in the last 15 years on research on compiler correctness, secure compilation, and the design and verification of safe FFIs.

References

• Operational semantics for multi-language programs Jacob Matthews, Robert Bruce Findler - POPL 2007
• Stateful Contracts for Affine Types Jesse A. Tov and Riccardo Pucella - ESOP 2010
• FunTAL: Reasonably Mixing a Functional Language with Assembly Daniel Patterson, Jamie Perconti, Christos Dimoulas and Amal Ahmed - PLDI 2017
• Semantic Soundness for Language Interoperability Daniel Patterson, Noble Mushtak, Andrew Wagner and Amal Ahmed - PLDI 2022

Amal Ahmed is a Professor at the Khoury College of Computer Sciences at Northeastern University. Her interests include type systems and semantics, compiler verification, language interoperability, and secure compilation. Her earlier work showed how to scale the logical relations proof method to realistic languages, leading to wide use of the technique, including for soundness of advanced type systems such as Rust's, correctness of compiler transformations, and verification of fine-grained concurrent data structures. Her current work includes design and verification of safe FFIs and richer ABIs, and development of RichWasm, a richly typed WebAssembly that supports safe, shared-memory, inter-language linking. Over the last decade, she has been a frequent speaker and less-frequent organizer of the Oregon Programming Languages Summer School (OPLSS) and the Programming Languages Mentoring Workshop (PLMW), which seek to broaden participation in PL research.

• Web Presence: https://www.ccs.neu.edu/home/amal/