Pratap Singh

CS PhD student at CMU

less than 1 minute read

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 simply-typed lambda calculus, and LF, which adds dependent types. We based our proofs on those developed by Sørensen and Urzyczyn1, but we simplified and modified their presentation to make the proofs more digestible.

Check out my project writeup to see the proofs.

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