ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Mon 4 Sep 2023 16:00 - 16:22 at St Helens - TyDe: Type-Driven Runtimes Chair(s): Ningning Xie

Interoperability pervades nearly all mainstream language implementations, as
most systems leverage subcomponents written in different languages. And yet,
such linking can expose a language to foreign behaviors that are internally
inexpressible, which poses a serious threat to safety invariants and programmer
reasoning. To preserve such invariants, a language may try to add features to limit
the reliance on external libraries, but endless extensions can obscure the core
abstractions the language was designed to provide.

In this paper, we outline an approach that
encapsulates foreign code in a sound way—i.e., without disturbing the
invariants promised by types of the core language. First, one introduces novel
\emph{linking types} that characterize the behaviors of
foreign libraries that are inexpressible in the core language.
To reason about the soundness of linking,
one constructs a \emph{realizability model} that captures the meaning
of both core types and linking types as sets of target-language terms.
Using this model, one can formally prove when foreign behavior is \emph{encapsulated};
that is, unobservable to core code.
We show one way to discharge such proofs automatically by augmenting the compiler to insert verified \emph{encapsulation wrappers}
around components that use foreign libraries.

Inspired by existing approaches to FFIs, we develop a pair of case studies that
extend a pure, functional language: one extension for state, and another for
exceptions. The first allows us to implement mutable references via a library,
whereas the second allows us to implement $\mathtt{try}$ and $\mathtt{catch}$ as
library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.

Mon 4 Sep

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

16:00 - 17:30
TyDe: Type-Driven RuntimesTyDe at St Helens
Chair(s): Ningning Xie University of Toronto / Google DeepMind
Semantic Encapsulation using Linking Types
Daniel Patterson Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University, USA
Towards Tagless Interpretation of Stratified System F (Extended Abstract)
Peter Thiemann University of Freiburg, Germany, Marius Weidner University of Freiburg
File Attached
Types as First-Class Values in Fuzion (Extended Abstract)
Fridtjof Siebert Tokiwa Software GmbH
File Attached
Pipit: Reactive Systems in F★ (Extended Abstract)
Amos Robinson Australian National University, Australia, Alex Potanin Australian National University
File Attached