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 Gradesope. 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 2
Due: April 9 by 5pm PT
This homework focuses on proofs by induction in Coq as well as formalizing the syntax and semantics of PLs where programs always terminate for "obvious" reasons. It covers material from Week 01 and the beginning of Week 02. Homework 2 and subsequent homework assignments should be completed with your partner.
Homework 3
Due: April 23 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.) Don't forget to work with your partner!
