CSE 506: Proof Assistants (Winter 2014)

This quarter we'll explore the use of proof assistants to formally verify software.

Class Meeting, Text, and Logistics

Wed / Fri
10:30 - 11:50
CSE 203

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.

Projects: Learn by Doing

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.

Presentations

Sometime in the quarter, you'll get the opportunity to lead the discussion for a chapter of CPDT.

Upcoming Schedule (flexible, stay tuned)

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
Finals Project Presentations

You may want to check out material from: