Ups: Created page with "''Linking isn't Substitution'' by Jeremy Siek While the static semantics of separate compilation has received considerable attention in the programming languages literature, the..."

2013-05-29T21:04:20Z

Created page with "''Linking isn't Substitution'' by Jeremy Siek While the static semantics of separate compilation has received considerable attention in the programming languages literature, the..."

New page

''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.

WG211/M12Siek - Revision history

Ups: Created page with "''Linking isn't Substitution'' by Jeremy Siek While the static semantics of separate compilation has received considerable attention in the programming languages literature, the..."