CSE 506

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)

Related Courses

You may want to check out material from:

• Northwestern PL Seminar Fall 2013

• Penn Advanced Martial Arts in Coq Fall 2012

• MIT Interactive Computer Theorem Proving Fall 2011

• CPDT Exercises