Foundations of Programming studies some of the fundamental mathematical concepts that underlie modern programming languages, including aspects of recent and current research. Example topics include: basic lambda calculus; operational semantics; types and type systems; and domain theory. You’ll spend around two hours per week in lectures studying for this module.
The FPP mini project provides you with the opportunity to deepen your understanding of the mathematical foundations of programming languages by studying in depth a specific topic related to your course. You’ll discuss your topic with your supervisor, choosing from a list of proposed topics. You’ll be required to write a report on your chosen topic and give a presentation on its central aspects.
The main textbook for the module is Types and Programming Languages by Benjamin C. Pierce (I will refer to it by TPL from now on). You must write down careful notes during the lectures, since not all the material is covered by the book. (In particular, the book doesn't cover denotational semantics.)
Two other excellent references are: The Formal Semantics of Programming Languages by Glynn Winskel; Lambda Calculi with Types by Henk Barendregt and Denotational Semantics by R. D. Tennent, respectively in Volume 2 and 3 of the Handbook of Logic in Computer Science.
In this section you will find, after each lecture, a list of topics that were taught and references to the chapters of the textbook.
Date | Topics | Textbook |
---|---|---|
1. 28 Jan 2014 | Introduction: What FOP is about A simple untyped language |
TPL Chapters 1 and 3 |
2. 30 Jan 2014 | λ-calculus Church numerals |
TPL Chapter 5: 5.1,5.2 |
3. 4 Feb 2014 | λ-terms for Booleans and pairs reduction, normalization, confluence |
TPL 5.3 |
4. 6 Feb 2014 | Substitution and variable capture Reduction and normalization |
... |
5. 11 Feb 2014 | Recursion and the Y combinator Lists and streams |
... |
6. 13 Feb 2014 | Introduction to type systems | TPL Chapter 8 |
7. 18 Feb 2014 | The simply typed λ-calculus | TPL Chapter 9 |
8. 20 Feb 2014 | system T | ... |
9. 25 Feb 2014 | Ackermann Function Type constructors |
TPL Chapter 11 |
10. 27 Feb 2014 | Products, Sums, Lists | ... |
11. 4 Mar 2014 | Inductive Types Binary and Finitely Branching Trees |
TPL Chapter 20 |
12. 6 Mar 2014 | Inductive Types: Pattern Matching, Iterators (Folds) and Recursors |
... |
13. 11 Mar 2014 | The μ operator | ... |
14. 13 Mar 2014 | Rules for μ types | ... |
15. 18 Mar 2014 | Coinductive Types Initial Algebras and Final Coalgebras |
(TPL Chapter 21: 21.1-2) |
16. 20 Mar 2014 | System F | TPL Ch.22: 22.1-2, Ch.23: 23.1-3 |
17. 25 Mar 2014 | Encoding of Inductive types in System F |
TPL 23.4 |
18. 27 Mar 2014 | Properties of System F | TPL 23.5 |
19. 1 Apr 2014 | Review of the module Exam preparation |
... |
20. 3 Apr 2014 | Exam topics and structure SET survey |
... |
If you don't understand something or have any issues with the topics, don't be shy and ask. The first place to look for answers to questions about the module is the FOP forum on Moodle.
I will have office hours on Tuesday from 13:00 to 15:00 and Friday from 15:00 to 16:00. My office is A07 in the Computer Science Building. You can come and ask any question about the material explained in the lectures.
Please don't hesitate to ask me any question you may have about the module. You can contact me by e-mail: put G54FOP/FPP in the subject line, so I know immediately that it is about this module.
The purpose of the optional mini-project, formally the module G54FPP Foundations of Programming Mini-Project, is to provide G54FOP students with the opportunity to deepen their understanding of the mathematical foundations of programming languages by an in-depth study of a specific topic related to what is covered in G54FOP. I will give you a list of suggested topics with references. However, it is not exclusive: feel free to discuss other topics or amended versions of the suggested ones with the G54FOP/FPP convener.
After choosing a topic, your task is to
The report should be targeted at your fellow students; i.e., you can assume the reader will know the basics of operational semantics, lambda-calculus, etc. The expected length is around 10 pages, which is about 3000 to 4000 words excluding diagrams, code, references, or any appendices you feel have to be enclosed.
The deadline for the report is Wednesday 16 April 2013.
You can send it directly to me by e-mail.
The presentation will be on Monday 12 May.
The front cover of the report should clearly state:
Be sure to read carefully the regulations about submission of coursework and plagiarism in the student handbook.
Here is a list of topics from which you can choose your mini-project. For each topic I suggest a reference (article or book chapter) from which you can start learning it. From there you should expand your horizon and consult related material. Once you've decided to do the project, send me an email with the title G54FPP project preferences containing a single line with your name and the numbers of the projects in order of preference. For example, if I sent the message Venanzio Capretta, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, it would mean that Functional Programming with Streams is my first choice for a project topic, while Deriving Programs from Specifications is the one I like the least. I will then use an algorithm to assign projects in a way that maximises preferences. (You will always be allowed to discuss a change with me if you're not happy with the topic.)
Lazy functional programming allows the definition of infinite sequences, called streams. You will study how we can program with them and the mathematical theory to reason about them.
Reference: Ralf Hinze, Functional pearl: streams and unique fixed points.
The most important variants of typed λ-calculi can be classified according to the presence of three characteristics: polymorphism, dependent types, higher sorts. So they can be arranged into a cube of systems.
Reference: Henk Barendregt, Lambda calculi with types.
There is a nice similarity between operations on streams (infinite sequence) and traditional differential calculus. You will study how we can define functions on streams by giving differential equations on them and under what conditions they can be solved.
Reference: Kupke, Niqui and Rutten, Stream Differential Equations: concrete formats for coinductive definitions.
Labelled transition systems model very simple processes that may run forever. Bisimulation is the correct notion of equality on them: it characterizes when the behaviour of two processes is the same.
Reference: Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Chapters 1 and 2.
Most recursive data types can be defined in the purely functional language of system F by using polymorphism, that is, the quantification over all types.
Reference: Böhm and Berarducci, Automatic synthesis of typed Λ-programs on term algebras.
In an earlier module you studied the proof assistant Coq. Now you will learn how it is possible to define infinite data structures and propositions with infinite proofs.
Reference: Bertot and Casteran, Interactive Theorem Proving and Program Development, Chapter 13.
You will study a formal system called CCS, invented by Robin Milner, to model independent processes that can interact with each other through communication channels.
Reference: Davide Sangiorgi, Introduction to Bisimulation and Coinduction, Chapter 3.
Tony Hoare invented an elegant logical system to reason about imperative programs. It is based on the notion of invariant for loops. With it, you can specify properties of programs and prove them formally.
Reference: Huth and Ryan, Logic in Computer Science, Chapter 4.
The Pi calculus is a formal system that describes mobile components that communicate and change their structure. It provides a conceptual framework for understanding mobility and mathematical tools for expressing systems and reasoning about their behaviours.
Sangiorgi and Walker, The pi-calculus: a Theory of Mobile Processes, Chapter 1 and part of Chapter 2.
Functional programs are given by equations defining functions. So they may be manipulated by equational reasoning. We use this style of reasoning to calculate programs, in the same way that one calculates numeric values in arithmetic. A program can thus be derived from its specification by an equational derivation.
Gibbons, Calculating functional programs.