Discussion of the homework assignment from Exercises 06 and summary of invariants in case of subtyping (following Proving Safety Properties using Types).

Constraint-Based Type Checking

Unification

Note: get started on this assignment early.

• the solution can be long
• you will need the solution of this assignment to implement Labs 08
• no extensions will be given - this assignment is no less important than midterms that you may have in other classes

First, you need to read the description of type checking assignment in Labs 08.

Then, specify precisely

• a) abstract syntax of MiniJava+
• b) the set of all types that appear in programs
• c) the definition of the subtyping relation <: on these types

Then, write down a complete set of type checking rules for MiniJava+, that is

• d) for each statement and expression in the abstract syntax tree you will need to have one or more type checking rule.
• feel free to use any auxiliary functions that you need in your type checking rules, but please also define these functions precisely (using recursive mathematical definitions, and pseudo-code).

The type system rules should mention the environment and take the form seen in

• Typing Rules for Simple Language
• Lecture 07