<p>Though it many not be obviously directly related, one thing that comes to mind is the concept of "blame" by <a href="http://homepages.inf.ed.ac.uk/wadler/topics/blame.html" rel="nofollow" rel="nofollow">Wadler et al.</a>.  This give you a theoretical basis to think about mixing together different typing regimes into a coherent whole.</p>

<p>In essence, blame allows you to mix together languages with weaker type guarantees with languages that have stronger type guarantees without losing all the benefits of the strong guarantees.  The idea is that the parts of the system with weaker guarantees will get the "blame" if certain things go wrong, localizing runtime type errors.</p>

<p>Hopefully you can see how that might be useful for FFI and bindings that apply to languages with varying type systems.</p>

<p>Edit:  See Sam TH's answer for a fuller intellectual history of the concept of "blame".</p>

CC BY-SA 3.0
2011-03-27T17:34:03.087Z
2011-04-09T01:32:25.887Z
2011-04-09T01:32:25.887Z
Marc Hamann
<p>Following up to Marc's comment, I want to correct the record on blame.  Wadler neither introduced the concept of blame, which is due to <a href="http://www.ccs.neu.edu/scheme/pubs/icfp2002-ff.pdf">Findler and Felleisen</a>, nor introduced blame for mediating between different languages, which originates in <a href="http://www.ccs.neu.edu/scheme/pubs/dls06-tf.pdf">my 2006 paper</a>.</p>

<p>However, Marc is entirely correct on the point of blame, and the Matthews paper that Dave points out also discusses this issue.</p>

CC BY-SA 2.5
2011-04-06T16:32:33.817Z
The "Well Typed Programs" paper indeed provides the correct cites, and claims its specific contribution as providing "a uniform view of recent work on contracts, gradual
types, and hybrid types by introducing a notion of blame (from
contracts) to a type system with casts (similar to intermediate languagesused for gradual and hybrid types), yielding a system that we call evolutionary types."
sclv
CC BY-SA 3.0
2011-04-09T01:30:54.437Z
My apologies Sam for failing to give full credit to all those who had a share for the origins of "blame".  It just happened to be the papers that Wadler co-authored that introduced **me** to the idea and that I'm most readily familiar with.
Marc Hamann
CC BY-SA 2.5
2011-04-06T12:54:11.240Z
2011-04-06T12:54:11.240Z
Sam Tobin-Hochstadt
<p>The paper <a href="http://people.cs.uchicago.edu/~jacobm/papers/multilang/matthews-findler-popl07-bw.pdf" rel="nofollow">Operational Semantics for Multi-Language Programs</a>
by Jacob Matthews and   Robert Bruce Findler presents two approaches for defining the semantics of programs written in two programming languages, taking particular care of data defined in one language and used in the other.  The <strong>lump embedding</strong> allows values created in one language to appear in running code of another, but these are can only be passed around, not operated on (or perhaps operated on by only a small interface). 
The <strong>natural embedding</strong>  allows values in one language to be used in the other by performing a so-called <em>cross-language cast</em>, which converts values from one language to the other.</p>

<p>The paper <a href="http://www.cse.lehigh.edu/~gtan/paper/jnimodel_tr.pdf" rel="nofollow">JNI Light: An Operational Model for the Core JNI</a> by Gang Tan presents a formal semantics of how existing JNI works. In contrast to the previous paper, this is formalises many of the low level details of what's going on, rather than trying to explore the issues from a foundational perspective.</p>

<p>Work on type-checking foreign function calls, such as <a href="https://www.cs.umd.edu/grad/scholarlypapers/papers/furr-scholary.pdf" rel="nofollow">Checking Type Safety of Foreign Function Calls</a> by Michael Furr and Jeffrey Foster,  provide also a formal framework in which to phrase the type system and prove its soundness.</p>

<p>Looking at the references in these papers and finding where they are cited using google
scholar will help you discover a more thorough picture of what has been done in the area.</p>

CC BY-SA 3.0
2011-03-27T17:33:34.033Z
2015-12-05T18:24:49.773Z
2015-12-05T18:24:49.773Z
Dave Clarke
<p>Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings? </p>

<p>I have asked <a href="https://stackoverflow.com/questions/5440968/understand-foreign-function-interface-ffi-and-language-binding">some implementation issues on stackoverflow</a>, which is not suitable here. But I would like to ask from this site's view and see what I could possibly get from here.</p>

<p>Really appreciate your reply!</p>

<p>Thanks to Dave Clarke for <a href="https://cstheory.meta.stackexchange.com/questions/1080/are-my-questions-acceptable-here/1085#1085">his reply on meta</a>！ </p>

<pl.programming-languages><semantics>
Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?
Tim
# Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?

(Asked by: username_0 on 2011-03-27)

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?

I have asked [some implementation issues on stackoverflow](https://stackoverflow.com/questions/5440968/understand-foreign-function-interface-ffi-and-language-binding), which is not suitable here. But I would like to ask from this site's view and see what I could possibly get from here.

Really appreciate your reply!

Thanks to username_4 for [his reply on meta](https://cstheory.meta.stackexchange.com/questions/1080/are-my-questions-acceptable-here/1085#1085)！

**Tags:** pl.programming-languages, semantics


---

## 3 answers

### Answer by username_4 on 2011-03-27. Score: 18 | Accepted answer

The paper [Operational Semantics for Multi-Language Programs](http://people.cs.uchicago.edu/~jacobm/papers/multilang/matthews-findler-popl07-bw.pdf)
by Jacob Matthews and Robert Bruce Findler presents two approaches for defining the semantics of programs written in two programming languages, taking particular care of data defined in one language and used in the other. The **lump embedding** allows values created in one language to appear in running code of another, but these are can only be passed around, not operated on (or perhaps operated on by only a small interface).
The **natural embedding** allows values in one language to be used in the other by performing a so-called *cross-language cast*, which converts values from one language to the other.

The paper [JNI Light: An Operational Model for the Core JNI](http://www.cse.lehigh.edu/~gtan/paper/jnimodel_tr.pdf) by Gang Tan presents a formal semantics of how existing JNI works. In contrast to the previous paper, this is formalises many of the low level details of what's going on, rather than trying to explore the issues from a foundational perspective.

Work on type-checking foreign function calls, such as [Checking Type Safety of Foreign Function Calls](https://www.cs.umd.edu/grad/scholarlypapers/papers/furr-scholary.pdf) by Michael Furr and Jeffrey Foster, provide also a formal framework in which to phrase the type system and prove its soundness.

Looking at the references in these papers and finding where they are cited using google
scholar will help you discover a more thorough picture of what has been done in the area.


---

### Answer by username_2 on 2011-04-06. Score: 10

Following up to Marc's comment, I want to correct the record on blame. Wadler neither introduced the concept of blame, which is due to [Findler and Felleisen](http://www.ccs.neu.edu/scheme/pubs/icfp2002-ff.pdf), nor introduced blame for mediating between different languages, which originates in [my 2006 paper](http://www.ccs.neu.edu/scheme/pubs/dls06-tf.pdf).

However, Marc is entirely correct on the point of blame, and the Matthews paper that Dave points out also discusses this issue.

> **Comments:**
> **username_3**: The "Well Typed Programs" paper indeed provides the correct cites, and claims its specific contribution as providing "a uniform view of recent work on contracts, gradual types, and hybrid types by introducing a notion of blame (from contracts) to a type system with casts (similar to intermediate languagesused for gradual and hybrid types), yielding a system that we call evolutionary types."  
> **username_1**: My apologies Sam for failing to give full credit to all those who had a share for the origins of "blame".  It just happened to be the papers that Wadler co-authored that introduced **me** to the idea and that I'm most readily familiar with.  

---

### Answer by username_1 on 2011-03-27. Score: 9

Though it many not be obviously directly related, one thing that comes to mind is the concept of "blame" by [Wadler et al.](http://homepages.inf.ed.ac.uk/wadler/topics/blame.html). This give you a theoretical basis to think about mixing together different typing regimes into a coherent whole.

In essence, blame allows you to mix together languages with weaker type guarantees with languages that have stronger type guarantees without losing all the benefits of the strong guarantees. The idea is that the parts of the system with weaker guarantees will get the "blame" if certain things go wrong, localizing runtime type errors.

Hopefully you can see how that might be useful for FFI and bindings that apply to languages with varying type systems.

Edit: See Sam TH's answer for a fuller intellectual history of the concept of "blame".


---

