Computation and Deduction 2009

These are notes for Computation and Deduction 2009.

Code from February 4. Homework: complete the progress proof.

Code from February 9. Homework: complete the preservation proof.

[http://www.cs.cmu.edu/~cmartens/canonical.pdf Writeup of the material on canonical forms LF presented on February 11.]

Code from February 23.

Code from March 2.

Code from March 4. Homework: complete the proof of the subst lemma.

Code from March 16. Homework: complete the trans/ifz and trans/app cases. (Incomplete solution.)

Code from March 18.

Code from March 25.

Code from March 30.

Code from April 1.

Code from April 6.

Code from April 8.

Code from April 13.

Code from April 15.

Project ideas from 15-851 1997: [http://www.cs.cmu.edu/~fp/courses/97-comp-ded/projects.html]

Code from April 20.

Code from April 22.

Code from April 27.

Code from April 29.