Challenges of Multilingual Program Specification and Analysis

Carlo A. Furia; Abhishek Tiwari

Home/Archive/arXiv

arXiv · 2407.11661

Challenges of Multilingual Program Specification and Analysis

Carlo A. Furia·Abhishek Tiwari

View original source ↗Read source document ↗Export metadata ↓

Abstract

Multilingual programs, whose implementations are made of different languages, are gaining traction especially in domains, such as web programming, that particularly benefit from the additional flexibility brought by using multiple languages. In this paper, we discuss the impact that the features commonly used in multilingual programming have on our capability of specifying and analyzing them. To this end, we first outline a few broad categories of multilingual programming, according to the mechanisms that are used for inter-language communication. Based on these categories, we describe several instances of multilingual programs, as well as the intricacies that formally reasoning about their behavior would entail. We also summarize the state of the art in multilingual program analysis, including the challenges that remain open. These contributions can help understand the lay of the land in multilingual program specification and analysis, and motivate further work in this area.

Explore related subjects

cs.PL cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Carlo A. Furia, Abhishek Tiwari. 2024-07-16. Challenges of Multilingual Program Specification and Analysis. https://arxiv.org/abs/2407.11661

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study

Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite.

cs.PL↗

arXiv2026

A Linked List of Cases in Language Design

LispBM is a Lisp dialect for microcontrollers and embedded systems. This paper is about the changes made to LispBM resulting from it being integrated into the VESC family of firmware and thus gaining a userbase. As a surprise to Author 1, the new users of LispBM wrote programs larger than ever imagined. This used up all available heap space and we were forced to find a way to evaluate Lisp programs partitioned across RAM and flash memory. This story and a couple more, like the one about the Lisp-image system for fast boots, are the core contribution of this paper. When the first versions of the VESC firmware with a built-in Lisp runtime system were released, there was some grumbling here and there about Lisp and its syntax, as expected. To our delight, most seemed very excited about a scripting language in the firmware. To the engineer and builder users, the choice of syntax seemed to matter less than the potential it opened up for them.

cs.PL↗

arXiv2026

Expressive power of one-shot control operators and coroutines

Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators---which restrict the use of captured continuations to at most once---are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation.

cs.PL↗