General Information
This is a research seminar, not a lecture course. Lectures will be organized around the discussion of one or more esearch papers taken from the conference proceedings and journals in the area of programming languages, logic, and type theory. You will be expected to read each paper covered and be prepared to discuss it in class. To facillitate the discussion, you are expected to post on WebCT prior to the class two positive and two negative aspects of the paper together with a question.
In addition, you will be required to lead 3 inclass discussion(s). Each presentation must be accompanied in advance by typeset lecture slides in either Powerpoint or LaTeX slide format and you must send a pdffile containing the slides to the instructor prior to class. The presenter's slides will be posted on the course web site for future reference. The presenter is responsible for presenting a summary and a critical analysis of the paper(s) assigned to her (45 min), and to lead discussion (30min). The audience for a given paper is required to read the relevant papers in advance as preparation for the presentation.
The papers listed below represent an initial sample of the material we will cover in this class. It is to be expected that further reading will be required.
The practical component of the course will consist of a twopart project. In the first part, you will use existing dependentlytyped programming language or proof assistant to assess its usability and power. An intermediate report is due in midOctober which will be reviewed by your peers. In the second part, you will design and implement a tool or technique which improves an existing programming/proof environment or tests its usability for a novel application. Your final report should take into account the comments you received during the first round and incorporate them. Your results and experiences will be presented to the class during a workshop.
There will also be a final exam consisting of essay questions requiring a synthesis of some or all of the papers covered in the course.
 The schedule below is subject to change throughout the semester.
Please note that some of the links below will not work yet.
Schedule
Date 
Lecture 
Notes 

Thu 
Sep 1 
Overview 
Ch 2: Dependent types, Advanced Topics in Types and Programming Languages, B. Pierce 

Tue 
Sep 6 
Dependent types cont. 
Ch 2: Dependent types, Advanced Topics in Types and Programming Languages, B. Pierce 

Thu 
Sep 8 
How to read a paper 


Tue 
Sep 13 
Languages of the future 

Francisco Ferreira 
Thu 
Sep 15 
Dependently typed programming 

Andrew Cave 
Tue 
Sep 20 
DML 

Ian Clement 
Thu 
Sep 22 
Termination via dependent types 

David Thibodeau 
Tue 
Sep 27 
Sized types 

Costin Badescu 
Thu 
Sep 29 
Programming with Coq 

Olivier Savary Belanger 
Tue 
Oct 4 
Cayenne 

Ian Clement 
Thu 
Oct 6 

Francisco Ferreira 

Tue 
Oct 11 
Proof certificates 

David Thibodeau 
Thu 
Oct 13 
No class; invited lecture by Dale Miller on Friday. 

Tue 
Oct 18 
Logical frameworks 

Brigitte Pientka 
Thu 
Oct 20 

Brigitte Pientka 

Tue 
Oct 25 
Beluga 

Brigitte Pientka 
Thu 
Oct 27 
Delphin 

Brigitte Pientka 
Tue 
Nov 1 
Other approaches to binding 

Andrew Cave 
Thu 
Nov 3 
Programming theorem provers 

Costin Badescu 
Tue 
Nov 8 
Combining programming and proving 

David Thibodeau 
Thu 
Nov 10 
Proof irrelevance 

Olivier Savary Belanger 
Tue 
Nov 15 
Proofcarrying Code 

Costin Badescu 
Thu 
Nov 17 
Class cancelled 


Tue 
Nov 22 
Proofcarrying authorization 

Ian Clement 
Thu 
Nov 24 
Extensible proofchecking 

Olivier Savary Belanger 
Tue 
Nov 29 
Homotopy Type Theory (Introduction) 

Andrew Cave 
Thu 
Dec 1 
Workshop day 