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 Jan Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

 10:30 - 12:30: WGT - Programming features at Orleans Chair(s): Giuseppe CastagnaCNRS - Université de Paris, France 10:30 - 11:00Talk Gradual Algebraic Data TypesMichael GreenbergPomona College, Stefan MalewskiUniversity of Santiago de Chile, Éric TanterUniversity of Chile Pre-print File Attached 11:00 - 11:30Talk Gradual Typing for Extensibility by RowsTaro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan Pre-print 11:30 - 12:00Talk Foreign Function Typing: Semantic Type Soundness for FFIsDaniel PattersonNortheastern University, Amal AhmedNortheastern University, USA Pre-print 12:00 - 12:30Talk Space-Efficient Monotonic ReferencesDeyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA Pre-print