宿主-核心语言的组合理论
Compositional theories for host-core languages
AI总结：
本文扩展了Benton的线性-非线性类型理论，提出宿主-核心类型理论及类型化演算HC，通过充实范畴提供指称模型，并利用内部语言概念建立语法与语义的强对应关系，为多语言编程提供理论支持。
摘要：
各种类型和种类的线性类型理论在当今大多数编程语言研究中具有根本重要性。在本文中，我们描述了 Benton 的线性-非线性类型理论及其模型的一个扩展，对于该扩展，我们可以证明一些额外的性质，使得该系统在其理论方面表现更好。我们将此系统称为宿主-核心类型理论。宿主-核心语言的语法分为两部分，分别表示宿主语言 H 和嵌入在 H 中的核心语言 C。这一源自 Benton 对线性逻辑的线性-非线性公式的想法，允许灵活管理数据线性，这在非经典计算范式中尤为有用。宿主-核心风格可被视为多语言编程的一种简化概念，即异构编程语言中的软件开发过程。在本文中，我们提出了类型化演算 HC，这是一个最小且灵活的宿主-核心系统，捕获并标准化了一类理想宿主-核心语言的共同性质。我们提供了基于充实范畴的指称模型，并通过内部语言的概念阐述了语法与语义之间的强对应关系。后一结果提供了宿主核心风格的一些有用特征，否则这些特征难以获得。我们还讨论了系统 HC 的一些具体实例、扩展和特化。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
