Skip to Main content Skip to Navigation
Conference papers

FabULous Interoperability for ML and a Linear Language

Gabriel Scherer 1, 2 Max New 1 Nick Rioux 1 Amal Ahmed 1, 3
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages. We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system. To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01929158
Contributor : Scherer Gabriel <>
Submitted on : Wednesday, November 21, 2018 - 10:32:38 AM
Last modification on : Friday, April 30, 2021 - 10:02:40 AM
Long-term archiving on: : Friday, February 22, 2019 - 12:56:09 PM

File

1707.04984.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Gabriel Scherer, Max New, Nick Rioux, Amal Ahmed. FabULous Interoperability for ML and a Linear Language. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89366-2_8⟩. ⟨hal-01929158⟩

Share

Metrics

Record views

143

Files downloads

163