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:
- simple types, lambda-calculus
- 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 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 |
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)
|
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:
- 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 32001-1, Winter 2006) by Derek Dreyer.
- Type Systems for Programming Languages (CMSC 336, Winter 2002) by David MacQueen, one of the developers of SML/NJ.