I worked with Ruben Gamboa and Melissa Weiderrecht on this project for my Senior Design class. We developed a Scheme interpreter in ACL2, which enables us to prove partial correctness of student programs. This paper got accepted into Trends in Functional Programming (TFP) conference in Oklahoma.