This quarter we will learn techniques for thinking crisply about programming languages, write some fascinating programs, and discuss various design tradeoffs. We will cover the traditional 505 material using the Coq proof assistant.
| Meeting | Mon, Wed 9:15 THO 325 |
| Instructor | Zach Tatlock (ztatlock@cs) |
| Fri 10:00 CSE 546 | |
| TA | Doug Woos (dwoos@cs) |
| Thu 11:00 CSE 674 | |
| Tutor | Eric Mullen (emullen@cs) |
| Mon 11:00 CSE 674 | |
| Tutor | Joe Redmon (pjreddie@cs) |
| Wed 11:00 CSE 218 | |
| Discussion | Piazza |
| Syllabus | Calendar |
| Scores | 505 Gradebook |
Lecture 01 : Coq Tutorial (materials)
Lecture 02 : Lists and Induction (materials)
Lecture 03 : Syntax, Relations, Tactics (materials)
Lecture 04 : Expression Semantics, Relations vs. Functions (materials)
Lecture 05 : Statement Semantics, Big vs. Small Step (materials)
Lecture 06 : Analysis, Termination (materials)
Lecture 07 : Termination on Paper, Pseudo Denotational Semantics (materials)
Lecture 08 : Lambda Calculus, Reduction Strategies (materials)
Lecture 09 : Church Encodings, Y (materials)
Lecture 10 : STLC, Type Safety Proof (materials)
Lecture 11 : Extending STLC (materials)
Lecture 12, 13 : Extending STCL (materials)
Lecture 14 : Subtyping (materials)
Lecture 15 : System F (materials)
Lecture 16 : Recursive Types (materials)
Lecture 17 : Curry Howard (materials)
We will read and discuss a hadful of papers this quarter. Most of the readings are relatively non-technical; they're intended to foster discussion and debate. By 4pm the day before each discussion, please submit a short paper review. Your review should have 3 paragraphs: (1) a high-level summary of the paper and a concise recap of its main take-away; (2) a description of what you valued learning from the paper and what the paper's greatest strengths are; and (3) a discussion of what you disagreed with or felt could be improved to make the paper stronger.
Note that summaries are due at 4pm the day before discussion. Submit reading summaries via the 505 Dropbox.
| Oct 14 | The Future of Computing: Logic or Biology |
| Oct 28 | Proof of a Program: FIND |
| Nov 18 | Social Processes and Proofs of Theorems and Programs |
| Dec 09 | Formal Certification of a Compiler Back-end |
Please work on your homeworks with a partner. It should be more fun and help you meet folks in the department you may not have otherwise gotten a chance to work with. To find a partner who is not in your lab, try the Piazza partner search. Also, make sure to work with a different partner for each homework. Only one member of each team should submit a solution. Please clearly indicate both team members in a comment at the top of your submission. Happy hacking :)
Make sure to check out the tactic index to get up to speed with Coq tactics and see what's available!
Submit homeworks via the 505 Dropbox. If you absolutely must, you can turn homework in up to 2 days late, but the policy is to subtract 10% per day.
Homework 01 : due Friday, October 9 at 4pm
Homework 02 : due Friday, October 23 at 4pm
Homework 03 : due Monday, November 23 at 4pm
Submit exams via the 505 Dropbox.
Joe is leading the development of a new tactic index to help you learn what Coq tactics are available and how they work. Check it out and send us feedback!
Pierce's superb Software Foundations is very closely related to our course.
Chlipala's excellent Certified Programming with Dependent Types is great for continuing to develop more advanced Coq hacking skills.
The classic 505 materials and Types and Programming Language textbook are also excellent for learning all the material we'll cover in class and more, but from a traditional pen-and-paper perspective.
For some notes on bullets in proof scripts, see "Structuring proofs with bullets" and the Coq manual on bullets.