A calculus for link-time compilation

Abstract. We present a module calculus for studying a simple model of link-time compilation. The calculus is stratified into a term calculus, a core module calculus, and a linking calculus. At each level, we show that the calculus enjoys a computational soundness property: if two terms are equivalent in the calculus, then they have the same outcome in a smallstep operational semantics. This implies that any module transformation justified by the calculus is meaning preserving. This result is interesting because recursive module bindings thwart confluence at two levels of our calculus, and prohibit application of the traditional technique for showing computational soundness, which requires confluence. We introduce a new technique, based on properties we call lift and project, that uses a weaker notion of confluence with respect to evaluation to establish computational soundness for our module calculus. We also introduce the weak distributivity property for a transformation T operating on modules D1 and D2 linked by ⊕: T (D1 ⊕ D2) = T (T (D1) ⊕ T (D2)). We argue that this property finds promising candidates for link-time optimizations.