Foundations for Programming Languages

A course of the FCT UNL PhD Program in Computer Science

Accreditation for the Carnegie Mellon | Portugal Dual Degree in Computer Science.

Summary

Programming languages are among the most important and well-developed artifacts of computer science. The study of programming languages has always been a very active field with many applications - to software engineering, compiler technology, security, and concurrency. Even today, new programming language abstractions are being proposed, together with associated analysis techniques. The study of type theory and its application in programming language design plays a key role in the course.

The course has two parts. Firstly, students will learn techniques to formally define the semantics of programming languages, and to enforce and reason about safety properties of programs by means of type systems (functional, imperative, and concurrent languages will be covered). Secondly, students will learn about several state-of-the-art applications of programming language techniques, with a focus on language-based program certification and language-based security. This course should be regarded as a necessary requirement for any student interested in pursuing programming language research.

Course Information (2009-10)

Lectures: Friday 11-13h.

Tutorials: Wednesday 10-12h.

Instructors: Luís Caires [João Seco, Carla Ferreira].

Lectures

Lecture 1. 23 Oct.
Inductive Definitions. Judgment Systems. Induction principles for a judgment system (or set of judgement systems). The language lambda N (lambda calculus with natural numbers). Inductive definition of expressions and values. Inductive definition of evaluation. Names and binding. Capture avoiding substitution. Basic properties of the operational semantics and their proof.
Homework is section 1 of the handouts.
Lecture 1A. 28 Oct.
Expressing the semantics of programming languages: oparational semantics, small-step, big-step, abstract machines. Operational correspondences. Compiler correctness.
Lecture 2. 30 Oct.
Motivation for types and type systems. The simply typed lambda calculus. Inductive definition of typability; typing contexts. Basic properties of typing and their proof: Preservation of typing under reduction ; Preservation of typing under substitution; Progress; Type safety.
Homework is section 2.1 of the handouts.
Lecture 3. 4 Nov.
Proving properties of typed programs using logical predicates. Strong normalization of the simply typed lambda calculus.
Homework is section 2.2 of the handouts.
Lecture 4. 11 Nov.
Curry-Howard correspondence between programs and proofs, propositions and types. Product and sum types. Induction and recursive types. Godel System T.
Lecture 5. 18 Nov.
Strong normalization of System T. Strong normalization in lambda T, a programming language with general first-order inductive types.
Homework is section 2.3 of the handouts.
Lecture 6. 25 Nov.
State and higher-order store. A type system for a language with higher-order store. Type safety for higher-order store.
Homework: Homework is section 3.1 of the handouts.
Lecture 7. 4 Dec.
Dependent types and first-order quantification. Polymorphic types and second-order quantification. Girard-Reynolds System F. Generic and abstract types.
Homework: Read Chapters 23 and 24 of Harper's book.
Lecture 8. 11 Dec.
The Logical Framework LF. Encodings in LF of logics and programming languages. Adequacy of representation. The twelf tool. Twelf implementations of two simple systems: a theory of natural numbers, and the simply typed lambda calculus.
Homework:
Lecture 9. 17 Dec.
Refinement Types.
Lecture 10. 5 Jan.
Types for Concurrent Mobile Processes.

Homework

There is a document listing the homework exercises (updated 4 Dec). At some point, we will also propose a programming assignment (Ocaml and Twelf).

Bibliography

Text books (we will use parts)

Types and Programming Languages, Benjamin C. Pierce, 2002.
Practical Foundations of Programming Languages (draft), Robert Harper, 2009.