Существует ли какая-либо теория языков программирования, описывающая интерфейсы сторонних функций (FFI) и привязки к нескольким языкам?

Существует ли какая-либо теория языков программирования, описывающая интерфейсы сторонних функций (FFI) и привязки к нескольким языкам?

Я задал некоторые вопросы реализации на стеке потока , который здесь не подходит. Но я хотел бы спросить с точки зрения этого сайта и посмотреть, что я мог бы получить отсюда.

Очень ценю ваш ответ!

Благодаря Dave Clarke за его ответ на мета !

В статье « Операционная семантика для многоязычных программ » Джейкоба Мэтьюса и Роберта Брюса Финдлера представлены два подхода к определению семантики программ, написанных на двух языках программирования, с особой заботой о данных, определенных на одном языке и используемых на другом. Единовременное вложение позволяет ценности , созданные на одном языке , чтобы появиться в запуске кода другого, но они могут быть переданы только вокруг, но не работает на (или , возможно , оперировали лишь небольшой интерфейс). Естественное вложение позволяет значениям в одном языке , которые будут использоваться в другом, выполняя так называемый межъязыковой бросок , который преобразует значения с одного языка на другой.

В статье « Свет JNI: операционная модель для ядра JNI » Ган Тана представлена ​​формальная семантика того, как работает существующий JNI. В отличие от предыдущего документа, это формализует многие детали происходящего на низком уровне, а не пытается исследовать проблемы с фундаментальной точки зрения.

Работа по проверке типов вызовов внешних функций, такая как Проверка безопасности типов вызовов внешних функций Майкла Ферра и Джеффри Фостера, также предоставляет формальную основу для формулировки системы типов и подтверждения ее правильности.

Просматривая ссылки в этих статьях и выясняя, где они цитируются с помощью google scholar, вы сможете найти более полную картину того, что было сделано в этой области.

После комментария Марка я хочу исправить обвинения. Уодлер не ввел концепцию вины, которая возникла из-за Финдлера и Феллайзена, и не ввел вину за посредничество между разными языками, которая возникла в моей статье 2006 года .

Тем не менее, Марк совершенно прав в этом вопросе, и в статье Мэтьюса, на которую указывает Дейв, также обсуждается этот вопрос.

Хотя это явно не связано напрямую, одна вещь, которая приходит на ум, - это концепция «вины» Wadler et al. , Это дает вам теоретическую основу для размышления о смешении различных режимов набора в единое целое.

По сути, обвинение позволяет вам смешивать языки с более слабыми гарантиями типов с языками, которые имеют более строгие гарантии типов, не теряя при этом всех преимуществ сильных гарантий. Идея состоит в том, что части системы с более слабыми гарантиями получат «вину», если некоторые вещи пойдут не так, локализуя ошибки типа времени выполнения.

Надеемся, вы увидите, как это может быть полезно для FFI и привязок, которые применяются к языкам с различными системами типов.

Отредактируйте: См. Ответ Сэма TH для более полной интеллектуальной истории понятия "обвинения".