Joshua Dunfield
Email: joshuad at cs [dot] queensu.ca
Office: Goodwin 534
Office hours: Wednesdays 13:00–14:30, Fridays 13:00–14:30,
and usually anytime my door is open
Goodwin 521, Tuesday 14:30–16:00, Thursday 13:30–15:00
Week 1 (Jan. 9: lec1.pdf, 11 lec2.pdf) | Course overview. Grammars, rules and derivations. Small-step and big-step semantics; metatheory. |
Week 2 (Jan. 16: lec3.pdf, 18 lec4.pdf) | Metatheory, continued: induction on derivations. Soundness and completeness. Type soundness. Assignment 1 (.pdf) |
Week 3 (Jan. 23 expr1.rkt, 25 lec6-8.pdf) | Racket. Mathematical logic and natural deduction. Assignment 1 due Friday, Jan. 26 |
Week 4 (Jan. 30, Feb. 1; lec6-8.pdf) | Assignment 2 out (see above). Natural deduction; harmony. |
Week 5 (Feb. 6, 8; lec9.pdf, natural-deduction.rkt, lec10.pdf (updated 2018–02–11)) | Negation in natural deduction. Sequent calculus. Assignment 2 due Thursday, Feb. 8 in class. |
Week 6 (Feb. 13, 15; lec11.pdf, lec12.pdf) | Proof Game. Extending our expression language: lambda.rkt, lec12.pdf |
Reading week | Reading week (no lectures) |
Week 7 (Feb. 27, Mar. 1; lec12.pdf, lec13.pdf, rec.rkt) | Lambda calculus, small-step evaluation. Assignment 3 due Friday, Mar. 2. |
Week 8 (Mar. 6, 8; lec14.pdf) | Type systems. Type preservation. Assignment 4 due Saturday, Mar. 10. |
Week 9 (Mar. 13, 15; lec15.pdf) | Progress. Subtyping. Assignment 5 due Monday, Mar. 19. |
Week 10 (Mar. 20, 22) | Polymorphism. Ordered linear sequent calculus. Take-home exam. All material through lec15.pdf is in scope. Material on polymorphism from Mar. 20 is not in scope. |
Week 11 (Mar. 27, 29; lec16.pdf) | Imperative languages, effects and state. Denotational semantics. Presentation topic proposal due Monday, Mar. 26. |
Week 12 (Apr. 3, 5) | Student presentations. |
We will follow my lecture notes, which will be posted either before or shortly after the corresponding lecture(s).
The following books take somewhat different approaches from my core material, but you may find them useful.
Additional resources:
For the student presentations, you will need to form a group (probably of 2 or 3), do some semi-independent reading on a suitable topic, and give a "mini-lecture" (probably around 20 minutes) near the end of the term.
Here is a tentative list of suggested topics. One reason it's tentative is that this is the first time I've taught this course, so the set of topics we get through in my lectures isn't fixed. However, 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 different aspects of union types.
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 "presenting the paper": research papers are written narrowly, and usually difficult to understand even for experts. Expect that at least 75% of your presentation will be "old news", with the remaining 25% or so from a couple of recent papers.