|
|
| Lectures: |
Wednesday 13:15-15:00, room
INM 203
|
| Lab: |
Wednesday 15:15-17:00, room
INF 119
|
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.
- simple types, lambda-calculus
- normalization, references, exceptions
- subtyping
- recursive types
- polymorphism
- bounded quantification
- advanced features of the Scala type system
Lecturer: Dr. Sebastian Maneth,
 BC360,
 31226
Assistant: Burak Emir,
INR320,
36867
Course schedule
| Date |
13:15-15:00, INM203 (Lecture) |
15:15-17:00, INF119 (Lab) |
| 20.10.04 |
1 Introduction, Arithmetic
Expressions, Induction, Evaluation
Read: TAPL Ch 1 - 4
[
slides,
4 on 1,
6 on 1
]
|
Arithmetic Expressions [Description/Errata/Solution]
|
| 27.10.04 |
2 (untyped) Lambda-Calculus
Read: TAPL Ch 5 - 7
[
slides,
4 on 1,
6 on 1
]
|
de Bruijn terms, Call-by-Value evaluation [Description/Partial Solution/Tips]
|
| 03.11.04 |
3 Simply Typed Lambda-Calculus
Read: TAPL Ch 8 - 10
[
slides,
4 on 1,
6 on 1
]
|
Simply Typed Lambda Calculus with Let [Description/Tips]
|
| 10.11.04 |
4 Extensions, Normalization
Read: TAPL Ch 11 - 14
[
slides,
4 on 1,
6 on 1
]
|
"Buffer" session [Description]
|
| 17.11.04 |
5 Subtyping
Read: TAPL Ch 15 - 17
[
slides,
4 on 1,
6 on 1
]
|
Records and Subtyping [Description]
|
| 24.11.04 |
6 Objects, Classes, and Featherweight Java
Read: TAPL Ch 18 - 19
[
slides,
4 on 1,
6 on 1
]
|
Assignment: FJ
|
| 1.12.04 |
7 Featherweight Java
Read: TAPL Ch 19
[
slides,
4 on 1,
6 on 1
]
|
Assignment: FJ
|
| 8.12.04 |
8 Type Reconstruction, Let-Polymorphism
Read: TAPL Ch 22
[
slides,
4 on 1,
6 on 1
]
|
Assignment: FJ
|
| 15.12.04 |
9 Systems F and F-sub
Read: TAPL Ch 23,26
[
slides,
4 on 1,
6 on 1
]
|
Written Assignment
|
| 22.12.04 |
10 System F-sub
Read: TAPL Ch 28
[
slides,
4 on 1,
6 on 1
]
|
Discussion on written assignment
|
| 12.01.05 |
11 FGJ = FG + Generics
Read:
FJ paper,
GJ paper
[
slides,
4 on 1,
6 on 1
]*
|
Type Reconstruction
|
| 19.01.05 |
12 Introduction to Scala's Type System
Read:
Scalabale
Component Abstraction paper,
Expression Problem paper
[
slides: Overview
]
[
slides: Paper 1
]
[
slides: Paper 2,
4 on 1,
6 on 1
]
|
Assignment: FGJ
|
| 26.01.05 |
13 Featherweight Scala
[
[UPDATED] slides(PDF),
2 on 1(PS),
4 on 1(PS)
]
|
Assignment: FGJ
|
| 02.02.05 |
14 Featherweight Scala (cont.d)
[
[UPDATED] slides(PDF),
2 on 1(PS),
4 on 1(PS)
]
|
Assignment: FGJ
|
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.
The oral exam will be on 07.02.2005 between 8:00 and 13:00.
It will cover the lecture notes (slides) and the
corresponding information that can be found in the TAPL book
and the articles linked from this page.
Your final grade will be made up from the result of
the oral exam (1/2) and from the result of the assignments (1/2).
Please register for a 20 minute time slot for your
individual exam, by sending an email to Yvette.Dubuis@epfl.ch
or by signing up with her in person (room INR328).
Course book
NEW:Cardelli and Wegner's On Understanding Types, Data Abstraction and Polymorphism is a very readable survey on type system features.
What follows are some facts that you might useful or interesting. You do not need them for the course, but should read them if you wonder why lambda calculus is considered a programming language.
- Although the lambda calculus is so small, it very simple to extend
it and define programming languages. Peter Landin has described this in
his famous paper on "The next 700 Programming Languages".
- The fact that imperative operations like assignment and sequencing
are missing from the calculus does not mean that you cannot do it. You
can get an idea how for instance from Phil Wadler's
"Essence of Functional Programming" and Simon Peyton Jones, Phil Wadler: "Imperative Functional Programming".
- If you want to learn more about the lambda calculus, the standard reference is Henk Barendregt's book "The Lambda Calculus: Its Syntax and Semantics". There is an online summary and a copy in the IC library.
|
