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
Some basic knowledge of logic and functional and/or logic programming is
assumed as a prerequisite.
Structure of the course
- Introduction: History and prehistory of type systems.
- Review: The (untyped) λ-calculus.
- Review: Natural deduction for intuitionistic logic.
- The simply-typed λ-calculus.
- The Curry-Howard isomorphism.
- Second-order propositional logic and λ2.
- Hindley-Milner polymorphism.
- HM variations: reference types, records with subtyping.
- Research on topics for final presentations.
- Individual work on the chosen assignment.
- 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
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