Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2019.16
URN: urn:nbn:de:0030-drops-108087
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10808/
Turcotte, Alexi ; Arteca, Ellen ; Richards, Gregor
Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language
| pdf-format: |
|
Abstract
Foreign function interfaces (FFIs) allow programs written in one language (called the host language) to call functions written in another language (called the guest language), and are widespread throughout modern programming languages, with C FFIs being the most prevalent. Unfortunately, reasoning about C FFIs can be very challenging, particularly when using traditional methods which necessitate a full model of the guest language in order to guarantee anything about the whole language. To address this, we propose a framework for defining whole language semantics of FFIs without needing to model the guest language, which makes reasoning about C FFIs feasible. We show that with such a semantics, one can guarantee some form of soundness of the overall language, as well as attribute errors in well-typed host language programs to the guest language. We also present an implementation of this scheme, Poseidon Lua, which shows a speedup over a traditional Lua C FFI.
BibTeX - Entry
@InProceedings{turcotte_et_al:LIPIcs:2019:10808,
author = {Alexi Turcotte and Ellen Arteca and Gregor Richards},
title = {{Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language}},
booktitle = {33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
pages = {16:1--16:32},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-111-5},
ISSN = {1868-8969},
year = {2019},
volume = {134},
editor = {Alastair F. Donaldson},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10808},
URN = {urn:nbn:de:0030-drops-108087},
doi = {10.4230/LIPIcs.ECOOP.2019.16},
annote = {Keywords: Formal Semantics, Language Interoperation, Lua, C, Foreign Function Interfaces}
}
| Keywords: | Formal Semantics, Language Interoperation, Lua, C, Foreign Function Interfaces | |
| Seminar: | 33rd European Conference on Object-Oriented Programming (ECOOP 2019) | |
| Issue date: | 2019 | |
| Date of publication: | 10.07.2019 | |
| Supplementary Material: | ECOOP 2019 Artifact Evaluation approved artifact available at https://dx.doi.org/10.4230/DARTS.5.2.9 |
