Lectures: Wednesday 13:15-15:00, room INM 203
Lab: Wednesday 15:15-17:00, room INF 1
Newsgroup: epfl.ic.cours.type-systems
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 mid-term 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.type-systems 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 type-theoretic perspective, has important applications in software engeneering, language design, high-performance 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:

Textbook:

TAPL
Type Systems and Programming Languages (TAPL), Benjamin C. Pierce, MIT Press, 2002, ISBN 0-262-16209-1.

Lectures

The semester starts on October 23, 2006 and ends on February 9, 2007 (14 weeks).

Date 13:15-15:00, INM203 (Lecture) 15:15-17:00, INF119 (Lab)
25.10.2006 Introduction, Combinator Parsers (pdf, 1x2, 2x2)
Hand-in on November 8
01.11.2006 Arithmetic Expressions - Abstract Syntax and Proof Principles (pdf, 1x2, 2x2)
08.11.2006
Arithmetic Expressions - Reduction and Normal Forms (pdf, 1x2, 2x2)
The Untyped Lambda Calculus - Part 1 (pdf, 1x2, 2x2)
Hand-in 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)
Hand-in on December 5
29.11.2006 Simple Extensions to STLC (pdf, 1x2, 2x2)
06.12.2006 More Extensions to STLC (pdf, 1x2, 2x2)
Hand-in on December 15
13.12.2006 Recursion, References and Store Typings (pdf, 1x2, 2x2)
20.12.2006
Mid-term exam (assignment, solution)
Inference, Polymorphism (pdf, 1x2, 2x2)
Hand-in on January 16
Christmas & New Year
10.01.2007 Subtyping (pdf, 1x2, 2x2)
17.01.2007 Objects (pdf, 1x2, 2x2)
Hand-in 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 1-2 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%
Mid-term exam 30%
Final exam 40%

Resources

Lambda Calculus:

Type Systems Courses: