Compositional theories for host-core languages

TL;DR

This paper introduces the host-core type theory, an extension of Benton's Linear-Non-Linear type theory, providing a formal framework for multi-language programming with a focus on data linearity management.

Contribution

It presents the typed calculus HC, a minimal host-core system with a denotational model and a strong syntax-semantics correspondence, enhancing understanding of host-core language properties.

Findings

Formalization of host-core type theory with properties

Denotational model using enriched categories

Characterization of host-core languages via internal language

Abstract

Linear type theories, of various types and kinds, are of fundamental importance in most programming language research nowadays. In this paper we describe an extension of Benton's Linear-Non-Linear type theory and model for which we can prove some extra properties that make the system better behaved as far as its theory is concerned. We call this system the host-core type theory. The syntax of a host-core language is split into two parts, representing respectively a host language H and a core language C, embedded in H. This idea, derived from Benton's Linear-Non-Linear formulation of Linear Logic, allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms. 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 HC, a minimal and flexible host-core system that captures and standardizes common properties of an ideal class of host-core languages. We provide a denotational model in terms of enriched categories and we state a strong correspondence between syntax and semantics through the notion of internal language. The latter result provides some useful characterizations of host-core style, otherwise difficult to obtain. We also discuss some concrete instances, extensions and specializations of the system HC.