Strong Normalization for Lambda Calculi
For my final project in CS252r: Advanced Topics in Programming Languages in Spring 2021, I worked with Dr. Anitha Gollamudi on developing simplified proofs of strong normalization for complex calculi in the lambda cube. Primarily, we focused on System F, which adds polymorphism to the simplytyped lambda calculus, and LF, which adds dependent types. We based our proofs on those developed by Sørensen and Urzyczyn^{1}, but we simplified and modified their presentation to make the proofs more digestible.
Check out my project writeup to see the proofs.

M.H. Sørensen and P. Urzyczyn. Lectures on the CurryHoward Isomorphism. Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. ↩