Joshua Dunfield
Email: joshuad at cs [dot] queensu.ca
Office: Goodwin 534
Office hours: Thursdays 15:30-17:00 + TBA + by appointment,
and usually anytime my door is open
How to address me:
How not to address me:
I do not expect to use onQ for this course.
Goodwin 521, Tuesday 13:30–15:00 and Friday 13:30–15:00
Week 1 (Jan. 8: lec1.pdf, 11 lec2.pdf) | Course overview. Grammars, rules and derivations. Small-step and big-step semantics; metatheory. |
Week 2 No lectures (I will be travelling), but you must read: lec3.pdf, lec4.pdf | Metatheory, continued: induction on derivations. Soundness and completeness. Type soundness. Assignment 1 (.pdf) |
Week 3 (..., Jan. 25 expr1.rkt, lec6-8.pdf) | Racket. Mathematical logic and natural deduction. Assignment 1 due Friday, Jan. 26 |
Week 4 (Jan. 29, Feb. 1; lec6-8.pdf) | Assignment 2 out (see above). Natural deduction; harmony. |
Week 5 (Feb. 5, 8; lec9.pdf, natural-deduction.rkt, lec10.pdf (updated 2018–02–11)) | Negation in natural deduction. Sequent calculus. Assignment 2 due Friday, Feb. 8 in class. |
Week 6 (Feb. 12, 15; lec11.pdf, lec12.pdf) | Proof Game. Extending our expression language: lambda.rkt, lec12.pdf |
Reading week | Reading week (no lectures) |
Week 7 (Feb. 26, Mar. 1; lec12.pdf, lec13.pdf, rec.rkt) | Lambda calculus, small-step evaluation. - Assignment 3 due Tuesday, Feb. 26. |
Week 8 (Mar. 5, 8; lec14.pdf) | Type systems. Type preservation. |
Week 9 (Mar. 12, 15; lec15.pdf) | Progress. Subtyping. |
Week 10 (Mar. 19, 22; lec16.pdf) | In-class exam March 19 (preview). Imperative languages, effects and state. Polymorphism. |
Week 11 (Mar. 26, 29) | Student presentations (at least Mar. 26, possibly Mar. 29). |
Week 12 (Apr. 2, 5) | Denotational semantics. Dependent types and refinement types. |
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 in reading 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.
Tentative guidelines and deadlines: