Functional programming and type systems (48h, 6 ECTS)
Persons in charge: Giuseppe Castagna and Xavier Leroy
Teachers in 2010-2011
Type systems (17h30, Didier Rémy)
Towards proved programs (10h, Yann Régis Gianas)
Subtyping and recursive types (10h, Giuseppe Castagna)
Program transformations (12h30, Xavier Leroy)
Programming project (François Pottier)
Aims
This course presents the principles and formalisms that underlie many of
today's typed functional programming languages.
The first part of the course presents the basis of type systems. We study
various type systems, all of which aim to guarantee, before a program is
executed, that it is safe (i.e., it runs without crashing). Besides the
definition of these type systems, we study how this guarantee is obtained
(type soundness proof); how one can verify programs with type decorations
(type checking) or automatically determine whether a program without any
type annotations is well-typed (type inference).
In the second part, we study more advanced type-related techniques that
enable to express finer invariants of data structures and programs.
In the third part, we study subtyping, following a syntactic approach, in
the setting of elementary type systems (simply-typed lambda-calculus, System
F) and in the presence of recursive types. Then, we present semantic
subtyping and its application to typing semi-structured data (XML)
and its transformations.
In the fourth part, we present some transformations of functional programs
that are used in programming or in the compilation of functional programs,
in particular into abstract machine code; we show that the operational
semantics of programs is preserved by these transformations; in some cases,
well-typedness is also preserved.
Evaluation
Two written exams (a partial and a final exam) and a programming project
are used to evaluate the students.
Approximate syllabus
Simple (monomorphic) type systems.
Parametric polymorphism (System F and ML).
Type soundness: subject reduction and progress theorems.
Type inference via constraint solving.
Recursion; imperative features; recursive types
Algebraic data types. Existential types.
Overloading. Haskell type classes.
Types systems with stronger notions of type conversion:
indexed types, type functions and type families, proofs terms in types.
Refinement types
Contract and hybrid type checking.
Hoare style logical assertions.
Subtyping: simple types, System F, recursive types,
Semantic subtyping. Typing of XML and its transformations.
Operational semantics, environments and closures.
Compilation into abstract machines and its correctness proofs.
Program transformations: continuation passing style, monads, closure
conversion, defunctionalization.
Programming project
As part of this course, the students will be given an individual programming
task that will be used to illustrate, put into practice, or explore in
details one particular topic of the course. The task will be announced
after the first part of the course and will have to be submitted by the end
of the course; it will count for the evaluation of the students.
Pre-requisites
Elementary notions of operational semantics and lambda-calculus (rewriting
rules, inference rules), and a taste for programming, particularly in ocaml.
Languages and lecture notes
The course notes are in English. The lectures are by default in French, but
English could be used if French were a real problem for some students.
Bibliography
Types and Programming Languages, Benjamin C. Pierce, MIT Press, 2002.
François Pottier also maintains a
reading list.
Pedagogic team
Giuseppe Castagna
Xavier Leroy
François Pottier
Yann Régis-Gianas
Didier Rémy
Previous years
This course is based on the shorter course that was taught in previous years:
