A Calculus of Components with Dynamic Type-Checking

We present a simple module calculus modeling software composition in an open environment, where some components can be provided from the outside after execution has started. Operators for combining software components are as in previous module calculi; here, we focus on the new problems posed by the fact that components are not all available at compile time. In particular, we want to be able to statically check internal consistency of local code, by only specifying a required type for missing components, and then to perform dynamic checks which ensure that code received from the outside, which is assumed to travel with its type, can be successfully accepted, without requiring to type-check the whole code again.We consider two alternative solutions. The former uses simple dynamic checks based on standard subtyping, that is, a component can be safely combined with local code if it provides the expected features, and all additional features are hidden, thus avoiding conflict problems. The latter preserves the semantics we would get having all components statically available, but requires a more involved type system based on constraints, where dynamic checks prevent conflicts