Wed 23 Oct 2024 13:40 - 14:00 at San Gabriel - Formal Methods 1 Chair(s): Benjamin Delaware

The Application Binary Interface (ABI) for a language defines the interoperability rules for its target platforms, including data layout and calling conventions, such that compliance with the rules ensures “safe” execution and perhaps certain resource usage guarantees. These rules are relied upon by compilers, libraries, and foreign-function interfaces. Unfortunately, ABIs are typically specified in prose, and while type systems for source languages have evolved, ABIs have comparatively stalled, lacking advancements in expressivity and safety.

We propose a vision for richer, semantic ABIs to improve interoperability and library integration, supported by a methodology for formally specifying ABIs using realizability models. These semantic ABIs connect abstract, high-level types to unwieldy, but well-behaved, low-level code. We illustrate our approach with a case study formalizing the ABI of a functional source language in terms of a reference-counting implementation in a C-like target language. A key contribution supporting this case study is a graph-based model of separation logic that captures the ownership and accessibility of reference-counted resources using modalities inspired by hybrid logic. To highlight the flexibility of our methodology, we show how various design decisions can be interpreted into the semantic ABI. Finally, we provide the first formalization of library evolution, a distinguishing feature of Swift’s ABI.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:40 - 15:20
Formal Methods 1OOPSLA 2024 at San Gabriel
Chair(s): Benjamin Delaware Purdue University
13:40
20m
Talk
Realistic Realizability: Specifying ABIs You Can Count On
OOPSLA 2024
Andrew Wagner Northeastern University, Zachary Eisbach Northeastern University, Amal Ahmed Northeastern University, USA
DOI
14:00
20m
Talk
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
OOPSLA 2024
Robert Schenck DIKU, University of Copenhagen, Nikolaj Hey Hinnerskov DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Magnus Madsen Aarhus University, Martin Elsman University of Copenhagen
DOI
14:20
20m
Talk
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
OOPSLA 2024
Noam Zilberstein Cornell University, Angelina Saliling Cornell University, Alexandra Silva Cornell University
DOI
14:40
20m
Talk
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
OOPSLA 2024
Yichuan Li Nanjing University of Science and Technology, Wei Song Nanjing University of Science and Technology, Jeff Huang Texas A&M University
DOI
15:00
20m
Talk
Weighted Context-Free-Language Ordered Binary Decision Diagrams
OOPSLA 2024
Meghana Aparna Sistla The University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Thomas Reps University of Wisconsin-Madison
DOI