- HW1: Error handling in Big-step and Small-step semantics of IMP
- HW2: Error handling in Denotational Semantics of IMP
- HW3: Big-step, Small-step and Denotational Semantics of IMP++ (IMP enriched with side-effects, I/O, Halting, threads, and local variables)
- HW4: MSOS, RSEC, and CHAM Semantics of IMP++
- HW5: Category Theory Proofs
- HW6: Different definitions and evaluation strategies of Untyped Lambda Calculus
- Extra-Credit: A type-checker for System-F and subtype-polymorphic lambda-calculus