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.

翻译：线性类型理论（包括各种类型和种类）在现代编程语言研究中具有基础性重要性。本文描述了Benton线性-非线性类型理论及其模型的扩展，我们能够证明该扩展系统在理论层面具备更优的良构性质，并将其命名为宿主-核心类型理论。宿主-核心语言的语法被划分为两部分，分别代表宿主语言H和嵌入式核心语言C。这一源自Benton线性逻辑线性-非线性表达的思想，实现了数据线性的灵活管理，在非经典计算范式中尤为实用。宿主-核心风格可视为多语言编程（即异构编程语言环境下的软件开发过程）的简化概念。本文提出了带类型演算HC——一个最小且灵活的宿主-核心系统，它捕获并标准化了理想宿主-核心语言类别的共性特征。我们通过富范畴构建了指称模型，并借助内部语言概念建立了语法与语义间的强对应关系。这一结果为宿主-核心风格提供了难以通过其他途径获得的实用特征刻画。此外，我们还讨论了系统HC的具体实例、扩展及特化形式。