J. Dunfield
Email: joshuad at cs [dot] queensu.ca
Office: Goodwin 534
Office hours: Wednesdays 13:00–14:00, Thursdays 14:00–15:00 + by appointment,
and usually anytime my door is open
How to address me:
How not to address me:
I will make limited use of onQ for this course.
Week 1 (Jan. 7 and 8: lec1.pdf, Jan. 8 and 10: lec2.pdf) | Course overview. Grammars, rules and derivations. Small-step and big-step semantics; metatheory. |
Week 2 (Jan. 14: lec3.pdf; Jan. 15–16: lec4.pdf) | Metatheory, continued: induction on derivations. Soundness and completeness. Type soundness. Assignment 1 (.pdf) |
Week 3 (lec6-8.pdf) (there is no lec5.pdf) | Mathematical logic, natural deduction, harmony. Assignment 1 due Friday, Jan. 24 |
Week 4 (Jan. 28 lec9.pdf; Jan. 29, 31 lec10.pdf) | Natural deduction: negation. Sequent calculus. |
Week 5 (Feb. 4, 5, 7 lec12.pdf, lec13.pdf) | Extending our expression language. Assignment 2 out. |
Week 6 (Feb. 11, 13, 14: lec14.pdf) | Lambda calculus, small-step evaluation, type preservation. Assignment 2 due Friday, Feb. 14. |
Reading week | Reading week (no lectures) |
Week 7 (Feb. 25, 26: lec14.pdf; Feb. 28: lec15.pdf) | Type preservation and progress. Subtyping. |
Week 8 (Mar. 3: lec15.pdf—extended to reflect lecture contents; Mar. 4: no lecture; Mar. 6: no lecture, but read lec16.pdf, to be extended) | Subtyping. Imperative languages, effects and state. |
Week 9 (Mar. 10, 11: lec16.pdf; Mar. 13: lec17.pdf) | Imperative languages, effects and state. Polymorphism. |
Week 10 | No lectures. |
Week 11 | Student presentations (tentative). |
Week 12 | Student presentations (tentative). |
We will (mostly) follow my lecture notes, which will be posted either before or shortly after the corresponding lecture(s). I strongly recommend that you read the lecture notes closely! You can probably miss some lectures without major problems, as long as you understand the lecture notes.
Most students do not find the material in 865 to be easy. If you fall behind and don't have enough time to catch up on reading and attend lecture, you may want to prioritize reading the lecture notes.
The following books take somewhat different approaches from my core material, but you may find them useful.
Additional resources:
Racket resources (assuming we use Racket):
For your project, you will:
Here is a tentative list of suggested topics. Some of these will be covered to some extent in lecture. But even if I (say) cover union types in class, there is still an opportunity for you to cover them in more detail, or to look at aspects of union types that I didn't cover.
Recent conference proceedings (POPL, ICFP, ESOP, OOPSLA, ...) may also give you ideas of active topics that interest you; I will work with you to define a topic suitable for presentation. I don't recommend just picking one recent paper and summarizing it: research papers are written narrowly, and usually difficult to understand even for experts. Expect that at least 75% of your report and presentation will be "old news", with the remaining 25% or so from a couple of recent papers.
Guidelines and deadlines: