
What you will learn in this chapter
Key Words
type checking, type inference, formal semantics, type conversion and
coercion, overloading
Type Checking
6
We view type checking as evaluation with “abstract values”. Whereas dynamic semantics –
evaluation, deals with dynamically computed values like 0, 1, etc., static semantics – type checking
– deals with abstractions like int. A type system is sound if it correctly approximates the dynamic
behavior and predicts its outcome. For example, if the static semantics predicts that a term has the
type int, the dynamic evaluation of the term, if it terminates, will yield an integer.
As indicated in Chapter 5, ...