Skip to main content
Cornell University


Meeting Times:Tue/Thr 2:55-4:10

Location: Phillips 403

Instructor: Robert Constable
rc at cs dot cornell dot edu
Office: 320 Gates Hall
Office Hours: After class and by appointment

Texts & Resources

Free text book: Type Theory and Functional Programming. Various educational and research articles will be handed out as course material. The 2008 book Logicomix: An Epic Search for Truth by Doxiadis and Papadimitriou is related recreational reading. The lecture notes will constitute a small booklet for this approach to constructive type theory.


Homework Policies

Cornell University has a Code of Academic Integrity, with which you should be familiar. Violations of this code are treated very seriously by Cornell and can have long-term repercussions. In this course, you are encouraged to discuss the content of the course with other students, and you may also discuss homework problems with other students. However, you must do your own work, write up assignments yourself, and if you discuss a problem with another student, you are expected to document this fact in your write-up. It is a violation of the code to copy work, including programs, from other students; it is also a violation to use solutions to homework problems from previous iterations of the same course. Note that Cornell holds responsible for the code violation both the recipient and the donor of improper information.