  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.
