Dependent Types Assignment 3

In this assignment, you'll practice working with first-class functions and lists. The Pie exercises cover chapters 4 and 5. You'll also extend your normalizer for the untyped lambda calculus.

The Pie assignment should be completed by writing a definition for each claim, and then uncommenting the tests so that they all pass. Passing the tests is necessary, but not sufficient, for completing the exercise - you should also follow the instructions in the file.

1. Start from this file, which contains the Pie exercises
2. I'll provide a skeleton of the normalizer in Haskell and Racket. You may choose any language at all to implement your normalizer, but these files may provide a starting point.
3. Submit your 3.pie and your normalizer implementation, as a .zip archive with all files on Gradescope.

Parts of this assignment are written by David Christiansen and used with permission.