L'article Operational Semantics for Multi-Language Programs
de Jacob Matthews et Robert Bruce Findler présente deux approches pour définir la sémantique des programmes écrits dans deux langages de programmation, en prenant particulièrement soin des données définies dans une langue et utilisées dans l'autre. L' incorporation forfaitaire permet aux valeurs créées dans une langue d'apparaître dans le code en cours d'exécution d'une autre, mais celles-ci ne peuvent être transmises, pas exploitées (ou peut-être exploitées uniquement par une petite interface). L' incorporation naturelle permet d'utiliser des valeurs dans une langue dans l'autre en effectuant une conversion dite multilingue , qui convertit les valeurs d'une langue dans l'autre.
L'article JNI Light: An Operational Model for the Core JNI de Gang Tan présente une sémantique formelle du fonctionnement de JNI existant. Contrairement à l'article précédent, cela formalise de nombreux détails de bas niveau de ce qui se passe, plutôt que d'essayer d'explorer les problèmes d'un point de vue fondamental.
Les travaux sur la vérification de type des appels de fonction étrangère, tels que la vérification de la sécurité des types d'appels de fonction étrangère par Michael Furr et Jeffrey Foster, fournissent également un cadre formel dans lequel formuler le système de type et prouver sa solidité.
En regardant les références dans ces articles et en trouvant où ils sont cités à l'aide de google scholar, vous pourrez découvrir une image plus approfondie de ce qui a été fait dans la région.
Bien que beaucoup ne soient pas manifestement directement liés, une chose qui me vient à l'esprit est le concept de «blâme» de Wadler et al. . Cela vous donne une base théorique pour penser à mélanger différents régimes de typage dans un ensemble cohérent.
En substance, le blâme vous permet de mélanger des langues avec des garanties de type plus faibles avec des langues qui ont des garanties de type plus fortes sans perdre tous les avantages des garanties fortes. L'idée est que les parties du système avec des garanties plus faibles obtiendront le "blâme" si certaines choses tournent mal, localisant les erreurs de type d'exécution.
J'espère que vous pouvez voir comment cela pourrait être utile pour FFI et les liaisons qui s'appliquent aux langues avec des systèmes de types différents.
Edit: Voir la réponse de Sam TH pour une histoire intellectuelle plus complète du concept de «blâme».
la source