Lectures: Wednesday 13:1515:00, room INM 203
Lab: Wednesday 15:1517:00, room INF 1 Newsgroup: epfl.ic.cours.typesystems RSS Feeds: News Feed
News
 15.02.2007
 Assignment and solution of the final exam are now available.
 31.01.2007
 Lecture slides 14 are now available.
 23.01.2007
 Lecture slides 13 are now available.
 17.01.2007
 Lecture slides 12 and Exercise 6 are now available.
 10.01.2007
 Lecture slides 11 are now available.
 22.12.2006
 Assignment and solution of the midterm exam are now available.
 20.12.2006
 Lecture slides 10 and Exercise 5 are now available.
 13.12.2006
 Lecture slides 9 are now available.
 11.12.2006
 Deadline for Exercise 4 has been extended to Friday 15.
 06.12.2006
 Lecture slides 8 and Exercise 4 are now available.
 29.11.2006
 Lecture slides 7 are now available.
 22.11.2006
 Lecture slides 6 and exercise 3 are now available.
 15.11.2006
 Lecture slides 5 are now available; Lecture slides 4 and exercise 2 were updated.
 08.11.2006
 Lecture slides 4 and exercise 2 are now available.
 02.11.2006
 Implementation hints have been added to the exercise 1 page.
 01.11.2006
 Lecture slides 2 and 3 are now available.
 26.10.2006
 A newsgroup forum is available now for questions and comments related to this course. Direct your news client to epfl.ic.cours.typesystems or browse it through a web interface.
 25.10.2006
 Lecture slides 1 and exercise 1 are now available.
Overview
The study of type systems and of programming languages, from a typetheoretic perspective, has important applications in software engeneering, language design, highperformance compilers, and security.
In this course the student will learn the basic principles of type systems as they a appear in modern programming languages. The acquired knowledge will be sufficient to design small type systems, but it will also sharpen the student's awareness of typeful programming as such. The latter is an indispensable task when programming in strongly typed languages.
Content:
 simple types, lambdacalculus
 normalization, references, exceptions
 subtyping
 recursive types
 polymorphism
 bounded quantification
 advanced features of the Scala type system
Textbook:
Type Systems and Programming Languages (TAPL), Benjamin C. Pierce, MIT Press, 2002, ISBN 0262162091.
Lectures
The semester starts on October 23, 2006 and ends on February 9, 2007 (14 weeks).
Date  13:1515:00, INM203 (Lecture)  15:1517:00, INF119 (Lab) 

25.10.2006  Introduction, Combinator Parsers (pdf, 1x2, 2x2) 
Handin on November 8

01.11.2006  Arithmetic Expressions  Abstract Syntax and Proof Principles (pdf, 1x2, 2x2)  
08.11.2006 
Handin on November 22


15.11.2006  The Untyped Lambda Calculus  Part 2 (pdf, 1x2, 2x2)  
22.11.2006  The Simply Typed Lambda Calculus (pdf, 1x2, 2x2) 
Handin on December 5

29.11.2006  Simple Extensions to STLC (pdf, 1x2, 2x2)  
06.12.2006  More Extensions to STLC (pdf, 1x2, 2x2) 
Handin on December 15

13.12.2006  Recursion, References and Store Typings (pdf, 1x2, 2x2)  
20.12.2006 
Midterm exam
(assignment,
solution)

Handin on January 16

Christmas & New Year  
10.01.2007  Subtyping (pdf, 1x2, 2x2)  
17.01.2007  Objects (pdf, 1x2, 2x2) 
Handin January 30

24.01.2007  Featherweight Java (pdf, 1x2, 2x2)  
31.01.2007  Featherweight Scala (pdf, 1x2, 2x2)  
07.02.2007 
Final exam
(assignment,
solution)

Exercices
The course is accompanied by (written and programming) exercises. Students are allowed and encouraged to work in groups of two (both, for the programming and the written exercises). We plan two have 12 written assignments and one programming assignment which have to be turned in. The result will make up one third of your grade.
Grades
Final course grades will be computed as follows:
Homework and Project  30% 
Midterm exam  30% 
Final exam  40% 
Resources
Lambda Calculus:
 Lambda Calculus Interpreters by Lloyd Allison.
 Lambda Calculus Interpreter by David Stotts, Fall 2005.
 Notes on Simply Typed Lambda Calculus by Ralph Loader, University of Edinburgh, February 1998.
Type Systems Courses:
 Advanced Type Systems (CMSC 320011, Winter 2006) by Derek Dreyer.
 Type Systems for Programming Languages (CMSC 336, Winter 2002) by David MacQueen, one of the developers of SML/NJ.