Semantic Analysis

A stage that comes after parsing and usually involves building a symbol table and type checking.

A symbol table can be implemented with a stack of dictionaries, each representing a scope.

A type checker can be described using logical rules of inference.

Subtyping can be expressed using Least Upper Bound construction.

Program is sound if for each expression its dynamic type is equal to its static type.