Show simple item record

dc.contributor.authorTurcotte, Alexi 18:42:43 (GMT) 18:42:43 (GMT)
dc.description.abstractForeign function interfaces (FFIs) are commonly used as a way to mix programming languages. In such systems, a program written in a host language calls functions written in a guest language from within the same program. Perhaps the most popular language to interface with is C, due in no small part to its performance (often gained through unsafe operations), and programmers often write performance-critical code in C and call it from other languages. But while C is a very performant language, it is far from being memory-safe, and one might expect C to introduce unsoundness into host language systems. This host/guest language relationship echoes that of typed and untyped code in gradual type systems. In such systems, untyped values flowing into typed code must be cast at the boundary between typed and untyped code, and this introduces the possibility for runtime type errors in otherwise statically guaranteed code. Similarly, when a host language calls a function written in a guest language, this introduces any unsoundness in the guest language to the host language, and new errors become possible at runtime. And when an FFI is being used to call C functions, anything is possible. In this thesis, we explore the effects of C on languages using a C FFI. To demonstrate, we give a formalization of Poseidon Lua, an environment wherein Typed Lua code may call C functions, cast C values, and allocate C data. To showcase the interaction between Lua and C, we choose to formalize a core calculus for Lua, and do not model C per se; instead, we reason about C as if C calls were a black-box, remaining general with respect to C's semantics, while carefully quantifying the effects that C can have on Lua by leveraging the concept of blame from gradual typing. We present a nondeterministic operational semantics for Poseidon Lua, and use blame to assure that C is always at fault for runtime errors in Lua.en
dc.publisherUniversity of Waterlooen
dc.subjectProgramming Languagesen
dc.subjectFormal Semanticsen
dc.subjectForeign Function Interfacesen
dc.titleReasoning About Foreign Function Interfaces: Blame and Nondeterministic Formal Semanticsen
dc.typeMaster Thesisen
dc.pendingfalse R. Cheriton School of Computer Scienceen Scienceen of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorRichards, Gregor
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages