In this dissertation we develop an approach for reconciling \emphopen programming -- the development of programs that support dynamic exchange of higher-order values with other processes -- with strong static \emphtyping in programming languages.
We present the design of a concrete programming language, \emphAlice ML, that consists of a conventional functional language extended with a set of orthogonal features like higher-order modules, dynamic type checking, higher-order serialisation, and concurrency. On top of these a flexible system of dynamic components and a simple but expressive notion of distribution is realised. The central concept in this design is the \emphpackage, a first-class value embedding a module along with its interface type, which is dynamically checked whenever the module is extracted.
Furthermore, we develop a formal model for \emphabstract types that is not invalidated by the presence of primitives for dynamic type inspection, as is the case for the standard model based on existential quantification. For that purpose, we present an idealised language in form of an extended $\lambda$-calculus, which can express dynamic generation of types. This calculus is the first to combine and explore the interference of sealing and type inspection with higher-order \emphsingleton kinds, a feature for expressing sharing constraints on abstract types. A novel notion of \emphabstracton kinds classifies abstract types. Higher-order type and kind \emphcoercions allow for modular translucent encapsulation of values at arbitrary type.