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.

翻译：各类线性类型理论在当今大多数编程语言研究中具有基础性重要性。本文描述了本顿线性-非线性类型理论及其模型的扩展，我们能够证明该系统具有若干额外性质，这些性质使该理论体系在理论层面表现更优。我们称此系统为宿主-核心类型理论。宿主-核心语言的语法分为两部分，分别表示宿主语言H和嵌入H中的核心语言C。这一源于本顿线性逻辑的线性-非线性表述的思想，允许对数据线性进行灵活管理，在非经典计算范式中尤为实用。宿主-核心范式可视为多语言编程的简化概念，即在异构编程语言中进行软件开发的过程。本文提出类型化演算HC——一个能捕捉并标准化理想宿主-核心语言类共同性质的最小化灵活系统。我们通过充实范畴构建指称模型，并借助内部语言概念阐明语法与语义间的强对应关系。后者为宿主-核心范式提供了若干其他方法难以获得的有用特征刻画。我们还讨论了HC系统的若干具体实例、扩展与特化方案。