Finished Final Project. Proved Progress for an extended version of the Simply Typed Lambda Calculus. I also showed a non terminating term and proved it.
I want to thank Robert Rand for teaching CMSC631 and introducing us Coq and Cameron Moy for helping me narrow my focus on a smaller language then Scheme.