A Logical Foundation for Type-Safe Cross-Language Interoperability‹Programming› Keynote
Today’s software systems are complex and often made up of parts written in different programming languages with different computational and memory management strategies. This allows programmers to combine different languages and choose the most suitable one for a given problem. While this flexibility offers clear advantages, it also introduces significant challenges, as different programming languages may use different runtime environments, such as different VMs or hardware backends, which are hard to combine. Unfortunately, most existing foundations for interoperability assume that we compile languages into a common, uniform, low-level language, and do not scale easily to a cross-language interoperability where there is no such uniform backend. In this work, we propose a logical foundation for cross-language interoperability where we retain the operational semantics of each part. It is grounded in adjoint logic – a logic that unifies a wide collection of logics through the up-shift and down-shift modalities. We give a Curry-Howard interpretation of this logic where we use the down-shift modality to model foreign function calls, and the up-shift modality to model runtime code generation and execution. We sketch the statics and an operational semantics together with properties such as accessibility safety, which ensures that languages respect their user-defined boundaries, alongside type safety. Finally, we outline how we have used this foundation to reason about the interoperability between languages with fundamentally different runtime implementations such as functional languages and concurrent process languages or functional languages and quantum circuit description languages.
Wed 18 MarDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mKeynote | A Logical Foundation for Type-Safe Cross-Language Interoperability‹Programming› Keynote Keynotes Brigitte Pientka McGill University Link to publication | ||
