Foundations for Programming Languages
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 (2010-11)
Lectures: Thursday 14h-16h.
Tutorials: Wednesday 10-12h.
Lectures
- Lecture 1. 21 Oct.
Abstract and concrete syntax.
Inductive Definitions. Judgment Systems. Induction principles for a judgment system (or set of judgement systems).
Names and binding. Capture avoiding substitution.
The language lambda N (lambda calculus with natural numbers): inductive definition of expressions and values; inductive definition of evaluation.
Call by value and Call by name.
Homework LaTeX file.
Read Chapter 1 of Harper's book.
- Lecture 2. 28 Oct.
Expressing the (operational) semantics of programming languages: small-step, big-step, abstract machines.
Basic properties of operational semantics specifications and their proof.
Operational correspondences. Compiler correctness.
Landin's SECD machine and the compilation of lambda N.
Homework LaTeX file.
Read Chapter 3 (7,8) of Harper's book.
Look at SECD, you may also want to look at (some parts of) Danvy's paper below.
- Lecture 3. 11 Nov.
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.
- Lecture 4. 18 Nov.
Proving properties of typed programs using logical predicates. Strong normalization of the simply typed lambda calculus.
- Lecture 5. 25 Nov.
Curry-Howard correspondence between programs and proofs, propositions and types.
Natural deduction in intuitionistic propositional logic and the simply typed lambda calculus. Product and sum types.
Homework LaTeX file.
Read chapters 3-4 of Harper's book.
Read chapters 3-5 of the "Proofs and Types" book.
- Lecture 6. 2 Dec.
Curry-Howard correspondence between programs and proofs, propositions and types.
Universal and Existential Types. Polymorphism. System F.
Read chapters 21-22 of Harper's book.
- Lecture 7. 9 Dec.
Objects.
Read chapter 22 of Pierce's TPL book.
- Lecture 8. 13 Jan.
Applied type systems. Examples: A type system for information flow.
A type system for resource usage.
- Lecture 9. 27 Jan.
Student presentations.
Homework
There are running handouts listing the homework exercises.
Later on, we will also propose a programming assignment (Ocaml and (Twelf or Coq)).
Bibliography
Text books (we will use parts)
- Types and Programming Languages, Benjamin C. Pierce, 2002.
- Software Foundations, Benjamin C. Pierce,
Chris Casinghino,
Michael Greenberg,
Vilhelm Sjoberg,
Brent Yorgey, 2010.
- Practical Foundations of Programming Languages (draft), Robert Harper, 2009.
- Proofs and Types, Jean-Yves Girard, Yves Lafont and Paul Taylor, 1990.
Additional reading and resources