Please read Chapter 22 in your textbook.
Please do the following problems:
Prove that constraint type checking is total and sound using the SASyLF definitions and skeleton provided. We will not prove completeness for this homework. Finishing the totality theorem is easy, the soundness theorem is difficult.
You will need to use SASyLF 1.0.2 (uwm 16) or later.
The newest change is the addition of and judgments.
Look at the and.slf file in the examples directory,
and in $CLASSHOME/src/homework12.
Optionally, prove the variable substitution lemma used in the proof of soundness. Only attempt this part if you complete the main proof.
Find two ``constraint-based'' type systems in the literature. Cite them. What forms do the constraints take? Are proofs given for totality, soundness and completeness? Explain!