Elena Machkasova and Franklyn Turbak. 
<b>A Calculus for Link-Time Compilation.</b>
<i> Programming Languages and Systems: 9th European Symposium on Programming, ESOP 2000. </i>
Published as <i> Lecture Notes in Computer Science 1782 </i>,
Gert Smolka (Ed.)
<hr>
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 <i> computational soundness </i> property: 
if two terms are equivalent in the calculus, then they 
have the same outcome in a 
small-step 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 <i> lift </i> and <i> project </i>
that uses a weaker notion of <i> confluence with respect to
evaluation </i> to establish computational soundness for our 
module calculus.
We also introduce the <i> weak distributivity property </i>
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.
<hr>[<a href="esop00-modules.ps">PS</a>]  [<a href="esop00-modules.pdf">PDF</a>]