Overview

Type systems are pervasive in modern programming languages, and their applications range from preventing runtime errors or giving support to object-oriented analysis and design methodologies to static analysis techniques used to ensure various properties of executable code.

However, types have a quite long story — in some sense, older than programming languages themselves — and familiarity with their mathematical foundations must be gained in order to master the techniques common to different systems and applications.

The first part of the course will cover the foundations and "abstract" type systems: simply-typed λ-calculus and extensions, such as sum and product types or λ2. These lectures provide the basic language and algorithms used throughout the course. The second part of the course deals with features of type systems present in actual programming languages, such as polymorphism (parametric and ad hoc), references, inheritance, etc. Finally, the third part consists in individual (supervised) work on some topic chosen by the student, and leading to a final presentation. The goal here is to serve both the individual needs (research, professional) of the students while giving their classmates a broad view of this growing field.

Some basic knowledge of logic and functional and/or logic programming is assumed as a prerequisite.

Structure of the course

1. Introduction: History and prehistory of type systems.
2. Review: The (untyped) λ-calculus.
3. Review: Natural deduction for intuitionistic logic.
4. The simply-typed λ-calculus.
5. The Curry-Howard isomorphism.
6. Second-order propositional logic and λ2.
7. Hindley-Milner polymorphism.
8. HM variations: reference types, records with subtyping.
9. Research on topics for final presentations.
10. Individual work on the chosen assignment.
11. Students' presentations session.

Lecturers and office hours

• Julio Mariño
  D-2308 - jmarino |at| fi DOT upm DOT es
  Office hours: to be posted. Send me an e-mail to get an appointment.

Lectures take place at D-2319 (the Programming Languages meeting room) every Thursday (11:00 – 13:00) and Friday (09:00 – 11:00) during the first eight weeks of the spring semester 2014. However, the actual times can be negotiated considering the students' needs and availability of free slots.

---

Last modified: Mon Oct 7 18:30:15 CET 2013