Embedded Files
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.
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!
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 3
Homework 3
Due: Friday, May 2 by 5pm PT
This homework covers ASTs, interpreters, transition systems, and a little bit of Imp. Transition systems, the focus of Week 04, are a mathematical framework that we can use to study potentially infinite computations, such as while loops. (Recall that all our interpreters from Week 03 had to "obviously" terminate in order for Coq to accept them. So interpreters can't handle while loops.)
Page updated
Report abuse