Phase Distinctions in Type Theory
Luca Cardelli · 1988
Type systems were originally introduced in programming languages to provide a degree of static checking, achieved through typechecking. As type systems become more complex and typechecking more sophisticated, the attribute static becomes less appropriate. The situation is better described by thinking that the execution of a program