WG211/M12Siek

Linking isn't Substitution by Jeremy Siek

While the static semantics of separate compilation has received considerable attention in the programming languages literature, the dynamic semantics has not been adequately studied. The meaning of linking two or more modules together is typically given by way of substitution. However, a substitution-based semantics is not suitable from a compiler writer's viewpoint because substitution erases the boundary between modules. The compiler writer needs to know what behaviors are internal, and therefore may be optimized, versus what behaviors are external, that is, observable by other modules. Many aspects of the external behavior are specified in the application binary interface (ABI) of a language but the interaction between internal and external behavior is often ill specified. As a step towards understanding the semantics of separate compilation, I draw on trace semantics (from concurrent calculi) to give meaning to a separately compiled lambda calculus.