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: Saskatchewan, Central America change

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