This quarter we'll explore the use of proof assistants to formally verify software.
Wed / Fri
10:30 - 11:50
This course will primarily follow Chlipala's life changing Certified Programming with Dependent Types.
You may also find Pierce's excellent Software Foundations helpful, as it provides a gentler learning curve, and of course, his classic Types and Programming Languages provides a more traditional treatment of PL topics, always good to have on hand.
Primarily, lectures will collaboratively demonstrate programming and proving in the Coq proof assistant. Our pace and direction will be strongly guided by your questions and discussion, so speak up! We'll start ``simply'' (you'll appreciate those scare quotes all too soon) and build up increasingly sophisticated techniques as the quarter progresses, so it's very important to stay on top of the reading as we go along.
IMPORTANT : Make sure you are signed up for the mailing list!
LESS IMPORTANT : Hang out in #uwplse on freenode.
During the quarter, you'll work in a team of two or three to formalize and verify a project of your own design (hopefully related to your research!). I'll meet with each team outside of lecture at the beginning and toward the middle of the quarter to help guide your efforts and set appropriate goals. At the end of the course, each team will present their project and results to the class.
10 weeks is very short. Start early and make a little progress each day! For inspiration, look at some project ideas.
Sometime in the quarter, you'll get the opportunity to lead the discussion for a chapter of CPDT.
|Date||Presenter - Topic|
|Jan 08||Zach - Intro, CPDT 2|
|Jan 10||Zach - CPDT 2|
|Jan 15||Calvin - CPDT 3|
|Jan 17||Calvin / Brandon M. - CPDT 3|
|Jan 22||(POPL) - project hackathon|
|Jan 24||(POPL) - project hackathon|
|Jan 29||Brandon M. - CPDT 3|
|Jan 31||Ben - CPDT 4|
|Feb 05||Riley - CPDT 5|
|Feb 07||Konstantin - CPDT 6|
|Feb 12||Kivanc - CPDT 6|
|Feb 14||Stuart - CPDT 7|
|Feb 19||Eric R. - CPDT 8|
|Feb 21||Doug - CPDT 8, CPDT 9|
|Feb 26||Pavel - CPDT 10|
|Feb 28||James - CPDT 17|
|Mar 05||Eric M. CPDT 14|
|Mar 07||Eric M. CPDT 14|
|Mar 12||Zach - CPDT 12|
|Mar 14||Colin - CPDT 15|
You may want to check out material from: