A calculus of open modules: call-by-need strategy and confluence

We present a simple module calculus where selection and execution of a component is possible on open modules, that is, modules which still have to import some definitions from the outside. Hence, it provides a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing as basic terms configurations, which are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. Configurations can be manipulated by classical module/fragment operators, hence reduction steps can be either execution steps of the program or steps which perform module operators (called reconfiguration steps). Since configurations combine the features of lambda abstractions (first-class functions), records, environments with mutually recursive definitions, and modules, the calculus extends and integrates both traditional module calculi and recursive lambda calculi. We state confluence of the calculus, and propose different ways to prevent errors due to lack of some needed component, either by a purely static type system or by a combination of static and run-time checks. Moreover, we define a call-by-need strategy which performs module simplification only when needed and only once, leading to a generalization, including module features, of call-by-need lambda calculi. We prove soundness and completeness of this strategy using an approach based on information content which also allows to preserve confluence even in case local substitution rules are added to the calculus.