Homework

We are planning on 6 homework assignments this quarter. Each homework will involve formalizing programs and proving properties about their behavior, both in Coq and doing more traditional “pen and paper” style proofs. We also expect several homework assignments to involve writing some code in the languages we are formalizing.

Please submit homework solutions via the 505 Gradescope. See the 505 Overview section on homework for more information on points and partners. The 505 Gitlab may also host drafts of upcoming assignments; early feedback is welcome!

Homework 1

Assignment:  hw1.zip  (browse)

Due: Friday, January 6 by 5pm PT

This first homework is a quick, tutorial introduction to Coq based on material from the first lecture of Week 01 and is the only homework that must be completed individually.

Homework 2

Assignment:  hw2.zip  (browse)

Due: Friday, January 20 by 5pm PT

This homework focuses on proofs by induction in Coq as well as inductive propositions. It covers material from  Week 01 and f Week 02. Homework 2 and subsequent homework assignments should be completed with your partner.

Homework 3

Assignment:  hw3.zip  (browse)

Due: Friday, February 3 by 5pm PT

This homework covers inductive propositions, transition systems, and a little bit of Imp. Transition systems, the focus of Week 03, are a mathematical framework that we can use to study potentially infinite computations, such as while loops. (Recall that all our interpreters from Week 02 had to "obviously" terminate in order for Coq to accept them. So interpreters can't handle while loops.) 

Homework 4

Assignment:  hw4.zip  (browse)

Due: Friday, February 17 by 5pm PT

This homework covers inductive propositions, Imp programs as transition systems, Hoare logic, and a little bit of untyped lambda calculus. 

Homework 5

Assignment:  hw5.zip  (browse)

Due: Friday, March 3 by 5pm PT

This homework covers untyped lambda calculus and simply typed lambda calculus. 

Homework 6

Assignment:  hw6.zip  (browse)

Due: Friday, March 10 by 5pm PT

This homework mostly focuses on System F.