Write a Blog >>
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

wgt-2020-papers
10:30 - 12:30: WGT - Programming features at Orleans
Chair(s): Giuseppe CastagnaCNRS - Université de Paris, France
wgt-2020-papers10:30 - 11:00
Talk
Michael GreenbergPomona College, Stefan MalewskiUniversity of Santiago de Chile, Éric TanterUniversity of Chile
Pre-print File Attached
wgt-2020-papers11:00 - 11:30
Talk
Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Pre-print
wgt-2020-papers11:30 - 12:00
Talk
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
Pre-print
wgt-2020-papers12:00 - 12:30
Talk
Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA
Pre-print