This quarter we'll learn some techniques for thinking crisply about programming languages, write some fascinating programs, and discuss the design tradeoffs different language features present. Also, together we'll conduct a grand experiment: covering the traditional 505 material using the Coq proof assistant and a new interface called PeaCoq.
| Meeting | Mon, Wed 10:30 MGH 251 |
| Instructor | Zach Tatlock (ztatlock@cs) |
| Fri 10:30 CSE 546 | |
| TA | Eric Mullen (emullen@cs) |
| Thu 2:30 CSE 678 | |
| Dr. PeaCoq | Valentin Robert |
| (no Tue hours while Val is in San Diego) | |
| Discussion | Piazza |
| Mailing List | cse505a_wi15@uw.edu |
Episode 18 : Social Processes and CompCert (materials)
Episode 17 : Continuations II (materials)
Episode 16 : Curry-Howard + Continuations (materials)
Episode 15 : Fix + Curry-Howard (materials)
Episode 14 : Extending Simply Typed Lambda Calculus II (materials)
Episode 13 : Extending Simply Typed Lambda Calculus I (materials)
Episode 12 : Simply Typed Lambda Calculus (materials)
Episode 11 : Big Steps and Types Intro (materials)
Episode 10 : Formalizing Lambda Calculus (materials)
Episode 09 : Church Encodings (materials)
Episode 08 : Lambda Calculus (materials)
Episode 07 : Interpreters (materials)
Episode 06 : Operational Semantics and Proofs 2 (materials)
Episode 05 : Operational Semantics and Proofs 1 (materials)
Episode 04 : Inductive Predicates and Operational Semantics (materials)
Episode 03 : Lists and Syntax (materials)
Episode 02 : Hello PeaCoq (materials)
Episode 01 : And So It Begins (materials)
Homework 04 (bonus): due Wednesday, March 11 at 10am
Before our final lecture, please read both: For bonus points write a thoughtful paragraph about each paper and one question you'd like to discuss during lecture.
Homework 03 : due Friday, February 20 at 2pm
Homework 02 : due Friday, February 06 at 2pm
Homework 01 : due Friday, January 23 at 2pm
You can submit homework at the 505 Dropbox.
How to run PeaCoq on recycle / tricycle / bicycle:
$ ssh recycle.cs.washington.edu
$ ~ztatlock/PeaCoq/start-peacoq.sh
[ links to your PeaCoq instance will show up here ]
[ click on the recycle link to go to the editor ]
[ when you're done, kill the server with Control-C ]
^C
$ logout
How to run PeaCoq on attu:
$ ssh attu.cs.washington.edu
$ ~ztatlock/PeaCoq/start-peacoq.sh
[ links to your PeaCoq instance will show up here ]
[ click on the attu link to go to the editor ]
[ when you're done, kill the server with Control-C ]
^C
$ logout
Key Resources:
Superb Optional References: