[home]
Math 4680/5680, Topics in Logic and Computation
Fall 2013
Peter Selinger

Course Information

See the Course Information Sheet.

Announcements

Extra class time: We will have a make-up class on Tuesday, November 26, from 10:30-11:30. We will meet in the usual classroom (Chase 319).

Presentations: There will be 10 student presentations. Please see the schedule below.

Final exam: We decided to have the final exam on December 9, from 11–2. The exam will be in Chase 227 (second floor seminar room).

Reading: Strong Normalization (posted Nov 1). I am currently lecturing on the proof of the Strong Normalization Theorem. The proof can be found in Chapter 6 of "Proofs and Types", which is freely available for download (see "Links" below).

Midterm. Our midterm will be on Monday, October 21 in class. The midterm covers everything up to the October 11 class, i.e., up to and including the definition and typing rules of the simply-typed lambda calculus. This corresponds to Sections 1-4, 5.1, 5.2, and 6.1 of the lecture notes.

Office hours. My current office hours are Monday 1-2 and Wednesday 1-2.

No class on Monday, Sept 9. There will be no class on Monday, Sept. 9. See you all on Wednesday!

Welcome to the course (posted Sep 6). Here you will find assigments, any handouts, and other up-to-date information about the course.

Homework Assignments

  Due Homework
1. Mon, Sep 23 Lectures notes, problems 1, 3.
2. Mon, Sep 30 Lectures notes, problems 5-11.
3. Fri, Oct 18 Lectures notes, problems 13, 15, 16, 18, 19, 20.
4. Fri, Nov 8 Lectures notes, problems 26-29, 32.
5. Wed, Dec 4 Handout 1, problems 39, 40, 43.

Presentation topics

Here are some possible topics for in-class presentations:
  • Simply-typed lambda calculus and cartesian-closed categories (Darien)
  • Models of untyped lambda calclulus: the Pω model (Francisco)
  • Krivine's abstract machine
  • Continuation passing style and the double-negation translation (Brian)
  • Intuitionistic logic and Kripke models (MacGregor)
  • The pi-calculus; concurrent processes (Travis)
  • Evaluation strategies: call-by-name and call-by-value
  • Functional programming languages: Haskell, ML, and/or Agda (Melanie)
  • Proof assistants: Coq, Isabelle, and/or HOL (Justin)
  • Higher-order logic (Seth)
  • Denotational semantics: PCF and DCPO's (Ben)
  • Equational theories of the lambda calculus; solvability (Abdullah)
Please talk to me for references or more information on these topics. And here is the schedule by date:
  • Mon Nov 25: Abdullah and Melanie.
  • Tue Nov 26, 10:30a, Chase 319: MacGregor and Justin.
  • Wed Nov 27: Darien and Seth.
  • Fri Nov 29: Ben and Brian.
  • Mon Dec 2: Travis and Francisco.

Links

Lecture Notes: P. Selinger, "Lecture Notes on the Lambda Calculus", available from http://arxiv.org/abs/0804.3434.

Handout 1: Lecture Notes on Polymorphism (Nov 23): [pdf].

Additional Reading: J.-Y. Girard, Y. Lafont and P. Taylor, "Proofs and Types", available from http://www.paultaylor.eu/stable/Proofs+Types.html.



To Peter Selinger's Homepage: [home]
Peter Selinger / Department of Mathematics and Statistics / Dalhousie University
selinger@mathstat.dal.ca / PGP key