[Pl-seminar] Today: Formalizing an ABI with Semantic Typing and Separation Logic

[Luna Phipps-Costin]

Hi everyone:
We postponed Andrew Wagner's talk due to weather ❄️ last week.   So we'll get to hear him speak today, Feb 20th!   Here's the details one more time

When: Tuesday, 12:30-1:30. Lunch will be served 12-12:30
Where: WVH 366
Speaker: Andrew Wagner
Title: Formalizing an ABI with Semantic Typing and Separation Logic
Abstract:

Nearly all modern systems critically depend on interoperability between languages and libraries, but reasoning formally about this interaction has proven to be a serious challenge, as different components maintain drastically different invariants. Recent efforts to tackle the interoperability problem make use of advanced type systems or program logics that relate types or behaviors in one language to those in another.

But as we descend down toward the binary layer, the sophisticated type machinery slowly disappears, and all that remains is an unspoken promise between components. This promise is the application binary interface (ABI), which specifies data layouts, calling conventions, and other low-level details required for interaction. But while type systems have grown richer, ABIs have largely remained the same, lacking analogous advances in expressivity and safety guarantees.

We outline a vision for richer, semantic ABIs that would facilitate safer interoperability and library integrations. Building on recent work, we suggest a way forward using realizability models, which formally relate abstract, high-level types to unwieldy, but well-behaved, low-level code. We motivate the approach with a case study that uses separation logic to formalize the ABI of a functional source language in terms of a reference counting target implementation. We begin with a tutorial on separation logic, fictional separation, and semantic typing.

-------------- next part --------------
HTML attachment scrubbed and removed