Sat 25 Jan 2020 11:30 - 12:00 at Orleans - Programming features Chair(s): Giuseppe Castagna

In practice, FFIs are implemented by translation to a target language and by conversions at the level of the target. We wish to establish type soundness in such a setting, where there are two languages making foreign calls to one another. In particular, we want a notion of \emph{convertibility}, that a type $\tau_A$ from language $A$ is convertible to a type $\tau_B$ from language $B$, which we will write $\tau_A \sim \tau_B$, such that conversions between these types maintain type soundness (dynamically or statically) of the overall system.

In this paper, we leverage the idea that sound FFIs are a generalization of sound gradual typing, except unlike gradual typing, FFIs mediate between languages \emph{without} a common underlying term language. We start with two languages and define type soundness in a manner inspired by the practical implementation strategy: that the languages will be translated to a common target. We do this using a realizability model, that is, by setting up a logical relation indexed by source types but inhabited by target terms that behave as dictated by the source types. The conversions $\tau_A \sim \tau_B$ that \emph{should} be allowed, are the ones implemented by target-level translations that convert terms that semantically behave like $\tau_A$ to terms that semantically behave like $\tau_B$ (and vice versa). This means that the converted term must either produce a runtime cast failure or produce some term or value that behaves as $\tau_B$. With the notion of $\tau_A \sim \tau_B$ in hand, we can type check a foreign function call, and based on the semantics of
$\tau_A \sim \tau_B$, we can prove that typing the foreign function call is sound.

#### Sat 25 JanDisplayed time zone: Saskatchewan, Central America change

 10:30 - 12:30 Programming featuresWGT at Orleans Chair(s): Giuseppe Castagna CNRS - Université de Paris, France 10:3030mTalk Gradual Algebraic Data TypesWGTMichael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile Pre-print File Attached 11:0030mTalk Gradual Typing for Extensibility by RowsWGTTaro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan Pre-print 11:3030mTalk Foreign Function Typing: Semantic Type Soundness for FFIsWGTDaniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA Pre-print 12:0030mTalk Space-Efficient Monotonic ReferencesWGTDeyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA Pre-print