Phase Distinctions in Type Theory

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 is carried out in two phases: a typechecking phase (compile-time) and an execution phase (run time).