Fakultät für Informatik

TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

TUM

  Home  |  Forschung/Kompetenz  |  Lehre  |  Personen  |  Publikationen  |  Abschlussarbeiten  |  Sonstiges  |  Kontakt  | 

  Suche  

Vorlesung | Wintersemester 2006/2007
Types for Programming Languages
Christian Urban
 

> Lehre

> Vorlesungen

Vorlesungsseite

Types for Programming Languages

Time: Wednesdays 10:15-11:45 Place: Zuse (MI 01.11.018)

Final exam on 7th February

The aim of this lecture course is to show by example how type systems for programming languages can be defined and their properties developed using structural and operational techniques. At the end of the course students should appreciate how type systems can be used to constrain or describe the dynamic behaviour of programs, be able to use a rule-based specification of a type system to infer typings and to establish type soundness results. This course will draw a lot of inspiration from the types course given by Andrew Pitts at the University of Cambridge. It will be organised along the lines:

  • Introduction. The role of type systems in programming languages and formalisation of simple type systems. Establishing properties of type systems using structural induction techniques.

  • ML polymorphism. ML-style polymorphism. Principal type schemes and type inference. Correctness proof for the type inference algorithm W.

  • Polymorphic reference types. The pitfalls of combining ML-polymorphism with reference types.

  • Polymorphic lambda calculus. Syntax and reduction semantics. Examples of datatypes definable in the polymorphic lambda calculus.

  • Further topics. Subtyping and types for object oriented programming languages; typed assembly languages.

There will be two written exams, one at the middle and one at the end of the semester. The lectures will be given in English.

Recommended reading

  • Pierce, B.C. (2002). Types and Programming Languages. MIT Press.
  • Cardelli, L. (1997). Type Systems. In CRC handbook of computer science and engineering. CRC Press.
  • Cardelli, L. (1987). Basic Polymorphic Typechecking. Science of computer programming, vol. 8, pp. 147-172.
  • Gunter, C. (1992). Semantics of Programming Languages. MIT Press.
  • Morrisett, G. (2005). Chapter in Advanced Topics in Types and Programming Languages. MIT Press.

Slides (PDF)

[Lec 1] [Lec 2] [Lec 3] [Lec 4] [Lec 5, Ho 5] [Lec 6] [Lec 7] [Lec 8] [Lec 9] [Lec 10] [Lec 11]

Slides (PS)

[Lec 1] [Lec 2] [Lec 3] [Lec 4] [Lec 5, Ho 5] [Lec 6] [Lec 7] [Lec 8] [Lec 9] [Lec 10] [Lec 11]

Appraisal Form

elsewhere

 

 

© Software & Systems Engineering Research Group
Sitemap |  Kontakt/Impressum
Letzte Änderung: 2007-04-21 14:07:57