Due date: 11/30 @ at the beginning of class

The goal of this problem set is to explore type systems.

Warning: The second and third problem of this problem set depend on a solution of the first problem.

Problem 0:

Implement the typing rules for ISWIM as Redex metafunctions.

Hint: For complex cases in the type checker, design auxiliary metafunctions that perform the necessary equality tests and that produce the desired result type.

Develop a Redex test for a type soundness conjecture for the model.

Problem 1:

Add typing rules for the loop and break construct from problem set 8 to the solution of problem 0.

Problem 2:

Add typing rules for the cell type and its operations from problem set 9 to the solution of problem 0.