Formal semantics for multi-language programs by Amal Ahmed @StrangeLoopConf
Formal semantics for multi-language programs by Amal Ahmed  @StrangeLoopConf
Uploaded October 2023 | Updated September 2026, 3 weeks ago
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.

Amal Ahmed
Professor, Northeastern University

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.

----
Recorded on Sept 21, 2023 in the PWLConf track at Strange Loop 2023 in St. Louis, MO.
thestrangeloop.com
https://pwlconf
Formal semantics for multi-language programs by Amal AhmedSymbolic Numeric Programming in Julia by Shashi Gowda (Strange Loop 2022)The Vera C. Rubin Observatory Legacy Survey of Space and Time by Andrés Plazas MalagónWhy is a Monad Like a Writing Desk? by Carin Meier (2012)Exploring deep space and deep ocean with AI guidance by Daniel Van HoesenCat Hicks: Fostering a learning culture in coding teamsFelienne Hermans: How patterns in variable names can make code easier to readPlayable Quotes for Game Boy Games by Joël Franušić and Adam SmithStrange Loop Chat with Felienne Hermans about The Programmers BrainStrange Loop Language Panel - Hickey, Sussman, Wirfs-Brock, Pamer, Alexandrescu, Ashkenas (2011)Igor Steinmacher: Negotiation and padding in software project estimates
Strange Loop Conference |

"Formal semantics for multi-language programs" by Amal Ahmed

SHARE TO X SHARE TO REDDIT SHARE TO FACEBOOK WALLPAPER