(Chapter 30).
Leave your definitions and proof in your homework14 directory.
Define a type system from the literature (recent PL conference) in
SASyLF and prove one nontrivial theorem about it.
Undergraduate students or graduate students with special permission
may instead prove Corollary 30.3.11 for
(Chapter 30).
Leave your definitions and proof in your homework14 directory.
For the final exam (30% of grade), you may continue this project and prove type soundness for the type system, in which case you should put it in your homework15 directory. Otherwise, you will do a take-home examination.