Fall 2007 Peter Selinger 
See the Course Information Sheet. 
Final Exam Location (posted Nov 13). Our final exam will be on Thursday, Dec 6, at 3:30pm. The location will be Dunn 302. 
As announced, graduate students in this course are expected to give an
inclass presentation (a presentation is optional for undergraduates
and auditors). Here is a list of seven suggested topics. You can
choose from these topics or make up your own topic; in either case,
please see me for approval.

Problem Set 1, due Thursday, Oct 4. Please do the exercises from the course notes, up to p.20, except for Exercises 2.1 and 10(a)(b).
Problem Set 2, due Thursday, Oct 25.
Problem Set 3, due Tuesday, Nov 6 (firm deadline, please!).

All notes in a single file:Pages 194 (updated Nov 21): [ps] [pdf].Individual Files:Pages 116 (Introduction; untyped lambda calculus) (posted Sept 24): [ps] [pdf].Pages 1720 (Programming in untyped lambda calculus) (posted Oct 1): [ps] [pdf]. Pages 2128 (ChurchRosser) (posted Oct 9): [ps] [pdf]. Pages 2934 (ChurchRosser) (posted Oct 11): [ps] [pdf]. Pages 3538 (Combinatory algebras) (posted Oct 19): [ps] [pdf]. Pages 3945 (Lambda algebras) (posted Oct 23, corrected Nov 5): [ps] [pdf]. Pages 4653 (Simplytyped lambda calculus; natural deduction) (posted Oct 30): [ps] [pdf]. Pages 5465 (CurryHoward isomorphism; sums; classical logic) (posted Nov 5): [ps] [pdf]. Pages 6694 (Polymorphism; strong normalization; models of simplytyped lambda calculus; PCF; complete partial orders) (posted Nov 21): [ps] [pdf]. 
Proofs and Types: The book "Proofs and Types" by Girard,
Lafont, and Taylor is available from this website.
The following chapters were handed out in class:
Chapter
11: System F. Chapter 6: strong normalization for simplytyped
lambda calculus. Chapter 14: strong normalization for System F.
