Please refer this link from page 35 to 40.
There are 2 phases defined in PLs:
- Parsing and Type Checking to ensure the program is well-formed.
- Well-Behaved Execution of well-formed programs.
A language is said to be safe when well-formed and well-behaved execution are both achieved.
Static phase is specified by a statics comprising a set of rules for deriving type judgments stating that an expression is well-formed of a certain type.
Type safety tells us that the predictions about “some aspects of run-time safety by seeing that the types fit well in the program” is correct.
This note will use PFPL expression language E as example.