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.
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.
Add typing rules for the
construct from problem set 8 to the solution of problem 0.
Add typing rules for the cell type and its operations from problem set 9
to the solution of problem 0.