On the Multi-Language Construction

Two elementary arguments lie at the heart of the multi-language paradigm: the large availability of existing programming languages, along with a very high number of already written libraries, and software that, in general, needs to interoperate. Although there is consensus in claiming that there is no best programming language regardless of the context [4, 8], it is equally true that many of them are conceived and designed in order to excel for specific tasks. Such examples are R for statistical and graphical computation, Perl for data wrangling, Assembly and C for low-level memory management, etc. “Interoperability between languages has been a problem since the second programming language was invented” [8], so it is hardly surprising that developers have focused on the design of cross-language interoperability mechanisms, enabling programmers to combine code written in different languages. In this sense, we speak of multi-languages.

The field of cross-language interoperability has been driven more by practical concerns than by theoretical questions. The current scenario sees several engines and frameworks [13, 28, 29, 44, 47] (among others) to mix programming languages but only [30] discusses the semantic issues related to the multi-language design from a theoretical perspective. Moreover, the existing interoperability mechanisms differ considerably not only from the viewpoint of the combined languages, but also in terms of the approach used to provide the interoperation. For instance, Nashorn [47] is a JavaScript interpreter written in Java to allow embedding JavaScript in Java applications. Such engineering design works in a similar fashion of embedded interpreters [40, 41].¹ On the contrary, Java Native Interface (JNI) framework [29] enables the interoperation of Java with native code written in C, , or Assembly through external procedure calls between languages, mirroring the widespread mechanism of foreign function interfaces (FFI) [14], whereas theoretical papers follow the more elegant approach of boundary functions (or, for short, boundaries) in the style of Matthews and Findler’s multi-language semantics [30]. Simply put, boundaries act as a gate between single-languages. When a value needs to flow on the other language, they perform a conversion so that it complies to the other language specifications.

The major issue concerning this new paradigm is that multi-language programs do not obey any of the semantics of the combined languages. As a consequence, any method of formal reasoning (such as static program analysis or verification) is neutralized by the absence of a semantics specification. In this paper, we propose an algebraic framework based on the mechanism of boundary functions [30] that unambiguously yields the syntax and the semantics of the multi-language regardless the combined languages.

The Lack of a Multi-Language Framework. The notion of multi-language is employed naively in several works in literature [2, 14, 21, 30, 35‐37, 49] to indicate the embedding of two programming languages into a new one, with its own syntax and semantics.

The most recurring way to design a multi-language is to exploit a mechanism (like embedded interpreters, FFI, or boundary functions) able to regulate both control flow and value conversion between the underlying languages [30], thus adequate to provide cross-language interoperability [8]. The full construction is usually carried out manually by language designers, which define the multi-language by reusing the formal specifications of the single-languages [2, 30, 36, 37] and by applying the selected mechanism for achieving the interoperation. Inevitably, therefore, all these resulting multi-languages notably differ one from another.

These different ways to achieve a cross-language interoperation are all attributable to the lack of a formal description of multi-language that does not provide neither a method for language designers to conceive new multi-languages nor any guarantee on the correctness of such constructions.

The Proposed Framework: Roadmap and Contributions. Matthews and Findler [30] propose boundary functions as a way to regulate the flow of values between languages. They show their approach on different variants of the same multi-language obtained by mixing ML [33] and Scheme [9], representing two “syntactically sugared” versions of the simply-typed and untyped lambda calculi, respectively.

Rather than showing the embedding of two fixed languages, we extend their approach to the much broader class of order-sorted algebras [19] with the aim of providing a framework that works regardless of the inherent nature of the combined languages. There are a number of reasons to choose order-sorted algebras as the underlying framework for generalizing the multi-language construction. From the first formulation of initial algebra semantics [17], the algebraic approach to program semantics [16] has become a cornerstone in the theory of programming languages [27]. Order-sorted algebras provide a mathematical tool for representing formal systems as algebraic structures through a systematic use of the notion of sort and subsort to model different forms of polymorphism [18, 19], a key aspect when dealing with multi-languages sharing operators among the single-languages. They were initially proposed to ensure a rigorous model-theoretic semantics for error handling, multiple inheritance, retracts, selectors for multiple constructors, polymorphism, and overloading. In the years, several uses [3, 6, 11, 24, 25, 38, 39, 52] and different variants [38, 43, 45, 51] have been proposed for order-sorted algebras, making them a solid starting point for the development of a new framework. In particular, results on rewriting logic [32] extend easily to the order-sorted case [31], thus facilitating a future extension of this paper towards the operational semantics world. Improvements of the order-sorted algebra framework have also been proposed to model languages together with their type systems [10] and to extend order-sorted specification with high-order functions [38] (see [48] and [18] for detailed surveys).

In this paper, we propose three different multi-language constructions according to the semantic properties of boundary functions. The first one models a general notion of multi-language that do not require any constraints on boundaries (Sect. 3). We argue that when such generality is superfluous, we can achieve a neater approach where boundary functions do not need to be annotated with sorts. Indeed, we show that when the cross-language conversion of a term does not depend on the sort at which the term is considered (i.e., when boundaries are subsort polymorphic) the framework is powerful enough to apply the correct conversion (Sect. 4.1). This last construction is an improvement of the original notion of boundaries in [30]. From a practical point of view, it allows programmers to avoid to explicitly deal with sorts when writing code, a non-trivial task that could introduce type cast bugs in real world languages. Finally, we provide a very specific notion of multi-language where no extra operator is added to the syntax (Sect. 4.2). This approach is particularly useful to extend a language in a modular fashion and ensuring the backward compatibility with “old” programs. For each one of these variants we prove an initiality theorem, which in turn ensures the uniqueness of the multi-language semantics and thereby legitimating the proposed framework. Moreover, we show that the framework guarantees a fundamental closure property on the construction: The resulting multi-language admits an order-sorted representation, i.e., it falls within the same formal model of the combined languages. Finally, we model the multi-language designed in [30] in order to show an instantiation of the framework (Sect. 6).

All the algebraic background of the paper is firstly stated in [15, 17, 19]. We briefly introduce here the main definitions and results, and we illustrate them on a simple running example.

Given a set of sorts S, an S-sorted set A is a family of sets indexed by S, i.e., . Similarly, an S-sorted function is a family of functions . We stick to the convention of using s and w as metavariables for sorts in S and \(S^*\), respectively, and we use the \(\mathbb {blackboard}\) \(\mathbb {bold}\) typeface to indicate a specific sort in S. In addition, if A is an S-sorted set and \(w = s_1\ldots s_n \in S^+\), we denote by \(A_w\) the cartesian product \(A_{s_1} \times \cdots \times A_{s_n}\). Likewise, if f is an S-sorted function and \(a_i \in A_{s_i}\) for \(i = 1, \ldots , n\), then the function is such that \(f_w(a_1, \ldots , a_n) = (f_{s_1}(a_1), \ldots , f_{s_n}(a_n))\). Given \(P \subseteq S\), the restriction of an S-sorted function f to P is denoted by and it is the P-sorted function . Finally, if is a function, we still use the symbol g to denote the direct image map of g (also called the additive lift of g), i.e., the function such that . Analogously, if \(\le \) is a binary relation on a set A (with elements \(a \in A\)), we use the same relation symbol to denote its pointwise extension, i.e., we write \(a_1 \ldots a_n \le a'_1\ldots a'_n\) for \(a_1 \le a'_1, \ldots , a_n \le a'_n\).

The basic notions underpinning the order-sorted algebra framework are the definitions of signature, that models symbols forming terms of the language, and algebra, that provides an algebraic meaning to symbols.

If \(\sigma \in \varSigma _{w, s}\) (or, and \(\sigma :s\) when \(w = \varepsilon \), as shorthands), we call \(\sigma \) an operator (symbol) or function symbol, w the arity, s the sort, and (w, s) the rank of \(\sigma \); if \(w = \varepsilon \), we say that \(\sigma \) is a constant (symbol). We name \(\le \) the subsort relation and \(\varSigma \) a signature when is clear from the context. We abuse notation and write \(\sigma \in \varSigma \) when \(\sigma \in \bigcup _{w, s}\varSigma _{w, s}\).

An important property of signatures, related to polymorphism, is regularity. Its relevance lies in the possibility of linking each term to a unique least sort (see Proposition 2.10 in [19]).

The freely generated algebra \(\mathcal {T}_\varSigma \) over a given signature provides the notion of term with respect to .

The class of all the order-sorted -algebras and the class of all order-sorted -homomorphisms form a category denote by . Furthermore, the homomorphism definition determines the property of the term algebra \(\mathcal {T}_\varSigma \) of being an initial object in its category whenever the signature is regular. Since initiality is preserved by isomorphisms, it allows to identify \(\mathcal {T}_\varSigma \) with the abstract syntax of the language. If \(\mathcal {T}_\varSigma \) is initial, the homomorphism leaving \(\mathcal {T}_\varSigma \) and going to an algebra \(\mathcal {A}\) is called the semantic function (with respect to \(\mathcal {A}\)).

Example. Let \(L_1\) and \(L_2\) be two formal languages (see Fig. 1). The former is a language to construct simple mathematical expressions: \(n \in \mathbb {N}\) is the metavariable for natural numbers, while e inductively generates all the possible additions (Fig. 1a). The latter is a language to build strings over a finite alphabet of symbols : is the metavariable for atoms (or, characters), whereas s concatenates them into strings (Fig. 1b). A term in \(L_1\) and \(L_2\) denotes an element in the sets and , accordingly to equations in Fig. 2a and b, respectively.

The syntax of the language \(L_1\) can be modeled by an order-sorted signature defined as follows: , a set with sorts (stands for expressions) and (stands for natural numbers); \(\le _1\) is the reflexive relation on \(S_1\) plus (natural numbers are expressions); and the operators in \(\varSigma _1\) are and . Similarly, the signature models the syntax of the language \(L_2\): the set carries the sort for strings and the sort for atomic symbols (or, characters) the subsort relation \(\le _2\) is the reflexive relation on \(S_2\) plus (characters are one-symbol strings); and the operator symbols in \(\varSigma _2\) are , and . Semantics of \(L_1\) and \(L_2\) can be embodied by algebras \(\mathcal {A}_1\) and \(\mathcal {A}_2\) over the signatures and , respectively. We set the interpretation domains of \(\mathcal {A}_1\) to and those of \(\mathcal {A}_2\) to . Moreover, we define the interpretation functions as follows (the juxtaposition of two or more strings denotes their concatenation, and we use \(\hat{a}\) as metavariable ranging over ):Since and are regular, then \(\mathcal {A}_1\) and \(\mathcal {A}_2\) induce the semantic functions and , providing semantics to the languages.

The first step towards a multi-language specification is the choice of which terms of one language can be employed in the others [30, 35, 36]. For instance, a multi-language requirement could demand to use ML expressions in place of Scheme expressions and, possibly, but not necessarily, vice versa (such a multi-language is designed in [30]). A multi-language signature is an amenable formalism to specify the compatibility relation between syntactic categories across two languages.

In the following, we always assume that the sets of sorts \(S_1\) and \(S_2\) of the order-sorted signatures and are disjoint.³ Condition (1s) requires the multi-language subsort relation \(\le \) to preserve the original subsort relations \(\le _1\) and \(\le _2\) (i.e., \(\mathord {\le } \cap S_i \times S_i = \mathord {\le _i}\)). The join relation \(\ltimes \) provides a compatibility relation between sorts⁴ in and . More precisely, \(S_i \ni s \ltimes s' \in S_j\) suggests that we want to use terms in \(T_{\varSigma _i, s}\) in place of terms in \(T_{\varSigma _j, s'}\), whereas the intra-language subsort relation \(\preccurlyeq \) shifts the standard notion of subsort from the order-sorted to the multi-language world. In a nutshell, the relation \(\mathord {\le } = \mathord {\preccurlyeq } \cup \mathord {\ltimes }\) can only join (through \(\ltimes \)) the underlying languages without introducing distortions (indeed, \(\mathord {\preccurlyeq } = \mathord {\le _1} \cup \mathord {\le _2}\)).

The role of an algebra is to provide an interpretation domain for each sort, as well as the meaning of every operator symbol in a given signature. When moving towards the multi-language context, the join relation \(\ltimes \) may add subsort constraints between sorts belonging to different signatures. Consequently, if \(s \ltimes s'\), a multi-language algebra has to specify how values of sort s may be interpreted as values of sort \(s'\). These specifications are called boundary functions [30] and provide an algebraic meaning to the subsort constraints added by \(\ltimes \). Henceforth, we define \(S = S_1 \cup S_2\), \(\varSigma = \varSigma _1 \cup \varSigma _2\), and, given \((w, s) \in S_i^* \times S_i\), we denote by \(\varSigma ^i_{w, s}\) the (w, s)-sorted component in \(\varSigma _i\).

If \(\mathcal {M}\) is an algebra, we adopt the convention of denoting by M (standard math font) its carrier set and by \(\mu \) (Greek math font) its boundary functions whenever possible. Condition (1a) is the semantic counterpart of condition (1s): It requires the multi-language to carry (i.e., preserve) the underlying languages order-sorted algebras, whereas the boundary functions model how values can flow between languages.

Given two multi-language -algebras \(\mathcal {A}\) and \(\mathcal {B}\) we can define morphisms between them that preserve the sorted structure of the underlying projected algebras.

Conditions (1h) and (2h) are easily intelligible when the domain algebra is the abstract syntax of the language [15]: Simply put, both conditions require the semantics of a term to be a function of the meaning of its subterms, in the sense of [15, 46]. In particular, the second condition demands that boundary functions act as operators.⁵

The identity homomorphism on a multi-language algebra \(\mathcal {A}\) is denoted by and it is the set-theoretic identity on the carrier set A of the algebra \(\mathcal {A}\). The composition of two homomorphisms and is defined as the sorted function composition , thus and associativity follows easily by the definition of \(\circ \).

Hence, as in the many-sorted and order-sorted case [15, 19], we have immediately the category of all the multi-language algebras over a multi-language signature:

The construction in Sect. 3 does not set any constraint on boundary functions, thus giving a great deal of flexibility to language designers. For instance, they can provide boundary functions that act differently with respect to the intra-language subsort relation \(\preccurlyeq \): According to the previous example, it would have been possible to define to employ different value conversion specifications for terms in , based on whether they are used as natural numbers ( ) or as expressions ( ). However, when this amount of flexibility is not needed, we can refine the previous construction by reducing the amount of syntax introduced by the associated signature. In this section we examine

In both cases, we prove that the introduced refinements do not affect the initiality of the term algebra, thereby providing unambiguous semantics to the multi-language.

The constructions in the previous sections beg the question whether a multi-language algebra admits an equivalent order-sorted representation. Conceptually, it would mean that being a multi-language is essentially a matter of perspective: By forgetting how the multi-language has been constructed, what is left is simply an ordinary language. Mathematically speaking, it requires us to exhibit a reduction functor F from the multi-language category to an order-sorted one, such that there is an isomorphism \(\phi \) between the carrier sets of the multi-language term -algebra \(\mathcal {T}\) and \(F(\mathcal {T})\), and such that for each \(t \in \mathcal {T}\) and for each multi-language -algebra \(\mathcal {A}\).

In the following, we denote the reduction functor by F, \(F^*\), and \(F^\star \) accordingly whether its domain is the category , , and , respectively.

In the case of and categories, the construction of F and \(F^*\) is very simple, and we illustrate it only for the plain multi-language algebras of Sect. 3: Let \(\mathcal {A}\) be a multi-language -algebra. Then, we define the order-sorted -algebra \(\mathcal {A}_\varPi \) (called the associated order-sorted algebra of \(\mathcal {A}\)) by setting

If \(\mathcal {A}\) and \(\mathcal {B}\) are multi-language -algebras, and h is a multi-language -homomorphism from \(\mathcal {A}\) to \(\mathcal {B}\), the functor F maps \(\mathcal {A}\) and \(\mathcal {B}\) to their associated order-sorted algebras \(\mathcal {A}_\varPi \) and \(\mathcal {B}_\varPi \) and the homomorphism h to itself. Since \(A_\varPi = A\), the isomorphism \(\phi \) is the identity function.

If \(\mathcal {A}\) is an multi-language -algebra, the construction of the reduction functor \(F^*\) is similar to the definition of F. The only difference is the equation in the condition (3\(\pi \)) that turns into

Finally, the definition of \(F^\star \) starting from the category of multi-language algebras is slightly different. We define \(F^\star \) as a map from the multi-language category to the order-sorted category . We denote the reduction of a multi-language algebra \(\mathcal {A}\) and a homomorphism as and . The order-sorted algebra has the same carrier sets of the multi-language algebra \(\mathcal {A}\), i.e., , and interpretation functions . Furthermore, we define . Intuitively, the algebra is formally defined simply by forgetting about the boundary functions, while the homomorphism inherits their semantics from h. Again, the isomorphism \(\phi \) is the identity.

Unfortunately, even though \(\mathcal {T}\) is an initial algebra in its category, is not: Given two multi-language algebras \(\mathcal {A}\) and \(\mathcal {A}'\) that differ only in the boundary functions (we denote by \(\alpha \) and \(\alpha '\) the families of boundary functions of \(\mathcal {A}\) and \(\mathcal {A}'\), respectively) they both get mapped by \(F^\star \) to the same order-sorted algebra . Thus, if and are the unique homomorphisms going from \(\mathcal {T}\) to \(\mathcal {A}\) and \(\mathcal {A}'\), the functor F maps them to two different order-sorted homomorphisms and both leaving and going to , hence losing the uniqueness property. However, this does not pose a problem once fixed a family of boundary functions:

The reduction theorems presented in this section have a strong consequence: all the already known results for the order-sorted algebras can be lifted to the multi-language world.

The first theoretical paper addressing the problem of multi-language construction is [30]. The authors study the so-called natural embedding (a more realistic improvement of the lump embedding [7, 30, 34, 40]), in which Scheme terms can be converted to equivalent ML terms, and vice versa.⁷ The novelty in their approach is how they succeed to define boundaries in order to translate values from Scheme to ML. Indeed, the latter does not admit an equivalent representation for each Scheme function. Their solution is to “represent a Scheme procedure in ML at type \(\tau _1\rightarrow \tau _2\) by a new procedure that takes an argument of type \(\tau _1\), converts it to a Scheme equivalent, runs the original Scheme procedure on that value, and then converts the result back to ML at type \(\tau _2\)”.

Our goal here is not to discuss a fully explained presentation of ML and Scheme languages in the form of order-sorted algebras, but rather to show how we can model the natural embedding construction in our framework. Doing so, we provide a sketchy formalization of Scheme and ML syntax and semantics, and we redirect the reader to [30] for all the languages details.

To provide the semantics of Scheme, we follow the same approach of Goguen et al. [15] where the denotational semantics of the simple applicative language (SAL) introduced by Reynolds [42] is given by means of an algebra, exploiting the initiality theorem. Such a language is a “syntactically sugared” version of the untyped lambda calculus with the fixpoint operator, which in turn is very similar to Scheme.

Let be a set of variables and be the naturals lattice with \(\top \) and \(\bot \) adjoined. From [46], there exists a complete lattice V such that satisfies the isomorphism , where \(+\) is the disjoint union with minimum and maximum elements identified, and is the complete lattice of Scott-continuous functions from V to V. Given , we define the injections and \(i_\xi = \phi ^{-1} \circ j_\xi \), and the projection such that . The set of all Scheme environments is the lattice of all total functions \(\text {P}= X\rightarrow V\) with componentwise ordering \(\rho \sqsubseteq \rho '\) if and only if \(\rho (x) \sqsubseteq \rho '(x)\) in V for all \(x \in X\). Furthermore, we define auxiliary functions (see [15] for a more detailed explanation) in order to provide the semantics of the language (in the following, \(x \in X\) and ):

The semantics of the language is obtained by defining an algebra \(\mathcal {H}\) over a signature ,⁸ then the initiality yields the unique homomorphism from the term algebra. A Scheme term denotes a continuous function in the semantic domain . The interpretation functions of the operators are defined by the following equations:For the sake of simplicity, we made a minor change to the language presented in [30]. They have an extra operator wrong to print an error message in case of an illegal operation, due to the lack of a type system. For instance, the sum of two functions produces the error wrong "non-number". To avoid to add cases almost everywhere in the definition of the interpretation functions, we let ill-typed terms to denote the value \(\bot \) without an explicit encoding of the error message. Furthermore, we denote by the function application.

The ML-like language defined in [30] is an extended version of the simply-typed lambda calculus. As before, we provide its semantics by defining an algebra \(\mathcal {M}\) over an order-sorted signature .

Let \(\text {I}\) (should read ‘iota’) be a set of base types and K a \(\text {I}\)-sorted set of base values . We inductively define the set of simple types \(\text {T}\): If \(\iota \) is a base type, then it is a simple type; If \(\tau , \tau '\) are simple types, then \((\tau )\rightarrow (\tau ')\) is a simple type (henceforth we omit the parentheses). We abuse notation and extend K to the -sorted set of simple values where \(K_{\tau \rightarrow \tau '} = K_\tau \rightarrow K_{\tau '}\).

The set of all ML environments is defined as the set of all total functions \(\varDelta = Y \rightarrow K\), where is a set of variables disjoint from X (this assumption comes from [30]) and \(K = \bigcup _{\tau \in \text {T}} K_\tau \). We instantiate and . The poset carries all the simple types (i.e., \(\text {T}\subseteq S_2\)) and the sort ; \(\le _2\) is the reflexive relation on \(S_2\) plus for each \(\tau \in \text {T}\). An ML term of type \(\tau \) denotes a total function in \(M_\tau = \varDelta \rightarrow K_\tau \), and we define . Due to the Turing-incompleteness of such a language, we do not need all the mathematical machinery of [15, 46] to formalize its semantics.Until now, we have just formalized the single-languages. The multi-language \(\mathcal {A}\) that combines Scheme and ML is obtained by requiring and in order to use ML terms in place of Scheme terms and vice versa. However, in the simplest version of the natural embedding, “the system has stuck states, since a boundary might receive a value of an inappropriate shape” [30]. They restore the type-soundness by first employing dynamic checks, and then by decoupling error-handling from the value conversion through the use of higher-order contracts [12]. We limit ourselves here to describe the first version; the subsequent refinements can be embodied by further complicating the semantics of the boundary functions (we do not have forced any constraints on them).

Since we need a value representing the notion of stuck state in ML, we have to extend the algebra \(\mathcal {M}\). This is particularly easy by exploiting the underlying framework: We make \(\mathcal {M}^\bot \) into an order-sorted -algebra by defining \(M_{\tau }^\bot = \varDelta ^\bot \rightarrow K_{\tau }^\bot \), where \(\varDelta ^\bot = Y \rightarrow K^\bot \), \(K^\bot = \bigcup _{\tau \in \text {T}} K_\tau ^\bot \), and , and the -sorted injection \(\phi \) from \(M_\tau \) to \(M_\tau ^\bot \) such that \(\varphi (\hat{t}) = \hat{t}\). Now, \(\mathcal {M}^\bot \) becomes an algebra by letting \(\varphi \) to be an order-sorted -homomorphism (this in turn forces ) and letting the interpretation functions to denote the value \(\bot \) in the remaining non-yet defined cases (namely, they compute the value \(\bot \) whenever one of their arguments is \(\bot \)).

The boundary function moves the Scheme value in \(M_\tau \):where andVice versa, moves values from ML to Scheme. Its definition is analogous to the previous case: where \(\hat{n} = \delta \mapsto n\), andThese definitions adhere the conversion approach of the natural embedding in [30]: If \(\hat{e}\) is the value denoted by a natural number in Scheme, then it is converted—aside from cases deriving from ill-typed terms—by to the corresponding constant function denoting the same natural value in ML. Otherwise, if \(\hat{e}\) is the value denoted by a Scheme function, then it is mapped by to the ML function with variable x at type \(\tau \rightarrow \tau '\) such that converts its argument of type \(\tau \) to the Scheme equivalent by its conversion through to x. Then it runs the original procedure \(\hat{e}\) on it and convert back the result by .

Since the given boundary functions are subsort polymorphic, we can improve the construction and handle all the value conversions with a single polymorphic operator as explained in Sect. 4.1.

To the best of our knowledge, this is the first attempt to provide a formal semantics of a multi-language independently from the combined languages.

Related Works. Cross-language interoperability is a well-researched area both from theoretical and practical points of view. The most related work to our approach is undoubtedly [30], which provides operational semantics to a combined language obtained by embedding a Scheme-like language into an ML-like language. Such an outcome is achieved by introducing boundaries, syntactic constructs that model the flow of values from one language to the other. Ours boundary functions draw heavily from their work. Nonetheless, we shift them to a semantic level, in order to several variants of multi-language constructions.

[7, 21, 36, 40, 53] take a similar line and combine typed and untyped languages (Lua and ML [40], Java and PLT Scheme [21], or Assembly and a typed functional language [36]), focusing on typing issues and values exchanging techniques. Instead of focusing on a particular problem, we adopt a rather general framework to model languages. This choice abstracts away many low-level details, allowing us to reason on semantic concerns in more general terms, without having to fix any particular pair of languages.

A lot of work has been done on multi-language runtime mechanisms: [20] provides a type system for a fragment of Microsoft Intermediate Language (IL) used by the .NET framework, that allows programmers to write components in several languages (C#, Visual Basic, VBScript, ...) which are then translated to IL. [22] proposes a virtual machine that can execute the composition of dynamically typed programming languages (Ruby and JavaScript) and statically typed one (C). [4, 5] describes a multi-language runtime mechanism achieved by combining single-language interpreters of (different versions of) Python and Prolog.

Future Works. From our perspective, the research presented in this paper opens up on three directions. Firstly, future works should aim to provide an operational semantics to the formalization of multi-languages. Rewriting logic seems the most reasonable approach to unifying the denotational world, presented in this paper, to the operational one [31]. This line of research is particularly useful in order to move towards an implementation of an automatic tool able to combine languages such that the resulting multi-language guarantees the results proved in the paper.

Secondly, future research applies to use the multi-language model in order to study the problem of analyzing multi-language programs. In particular, we aim at investigating how it is possible to obtain analyses of multi-language programs by merging already existing analyses of the single combined languages.

Finally, further studies should investigate the problem of compiling multi-languages. Current compilers are closed tools, non-parametric on language constructs (for instance, we cannot compile a single if-then-else term of a standard language like C or Java unless it is plugged into a valid program). Several works on typing [1, 20, 26], compiling [2, 37], and running [23, 50] multi-language programs already exist, but without providing a formal notion of multi-language. It would be beneficial to study how their approaches can be applied to the formal framework developed in this paper.