Compositional theories for host-core languages

The syntax of a host-core language is spitted in two parts, representing respectively a \emph{host language} H and a \emph{core language} C, embedded in H. This idea is rooted in Benton's Linear/non Linear formulation of Linear logic and allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms. Moreover, the host-core style can be viewed as a simplified notion of multi-language programming, the process of software development in a heterogeneous programming language. In this paper, we present the typed calculus HC0, a minimal and flexible host-core system that captures and standardizes common properties of an ideal class of host-core languages. We provide a denotation in terms of enriched categories and we state a strong correspondence between syntax and semantics through the notion of \emph{internal language}. The latter result provides some interesting characterizations of host-core style, otherwise difficult to achieve. We also show discuss some concrete instances, extensions and specializations of HC0.