FOP image

School of Computer Science
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB, UK

T: +44(0) 115 9514251
F: +44(0) 115 9514254
E: csit-enquiries@cs.nott.ac.uk

HMU cover

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.

Lecture Notes and Books

The main reference for the module consists in the lecture notes that will be provided on this page after each lecture. These contain the main ideas and concepts, but are not complete in detail. You must write down carefully your own notes during the lectures, since not all the material is covered by the given material.

Here are a some useful reference textbooks that you can consult to have more in-depth treatment of some topics.

Outline of lectures

In this section you will find, after each lecture, a list of topics that were taught and references to the chapters of the textbook.

DateTopicsLecture Material
1. Mon 30 Jan 2017 Introduction: What FOP is about
Denotational and Operational Semantics
Language of Arithmetic Expressions
Chapter 1 of Lecture Notes
Outline of Lecture 1
TPL Chapters 1 and 3
2. Thu 2 Feb 2017 Semantics of Arith Expressions
Denotational Interpretation
Reduction and Congruence Rules
Outline of Lecture 2
3. Mon 6 Feb 2017 Evaluation Strategies: Eager and Lazy
Untyped λ-calculus
Chapter 2 of Lecture Notes
Outline of Lecture 3
TPL Chapter 5
4. Thu 9 Feb 2017 Church Numerals
Abstract Syntax Trees
Free Variables and Substitution
Booleans and Pairs
Outline of Lecture 4
Computerphile video by Graham Hutton
5. Mon 13 Feb 2017 λ-terms for lists
Non-normalizing terms
Iteration and Recursion
Chapter 3 of Lecture Notes
Outline of Lecture 5
6. Thu 16 Feb 2017 The Y combinator
Factorial and Hailstone
Streams
Outline of Lecture 6
7. Mon 20 Feb 2017 Confluence, Evaluation Strategies
Introduction to type systems
Typed arithmetic expressions
Chapter 4 of Lecture Notes
Outline of Lecture 7
TPL Chapters 8
8. Thu 23 Feb 2017 The simply typed λ-calculus
Programming with simple types
Properties of simple types
Outline of Lecture 8
TPL Chapters 9
9. Mon 27 Feb 2017 Early Module Feedback
Haskell Implementations of
(Simply Typed) Lambda Calculus
Haskell Files:
Untypled λ-calculus
Simply Typed λ-calculus
10. Thu 2 Mar 2017 System T
Programming in system T
Ackermann Function
Chapter 5 of Lecture Notes
Outline of Lecture 10
11. Mon 6 Mar 2017 Interactive session
Programming in system T
Fibonacci Numbers
Haskell implementation of
System T
12. Thu 9 Mar 2017 Bit Streams
Enumerations, Products, Sums
Chapter 6 of Lecture Notes
Outline of Lecture 12
TPL Chapter 11
13. Mon 13 Mar 2017 Recursive Types
Inductive Types: Lists, Trees
Outline of Lecture 13
TPL Chapters 20, 21
14. Thu 16 Mar 2017 Inductive Types: The μ operator Outline of Lecture 14
15. Mon 20 Mar 2017 Coinductive Types: The ν Operator
Coalgebras
Outline of Lecture 15
16. Thu 23 Mar 2017 Haskell implementation of
Inductive and CoInductive Types
Mapping between Streams and Trees
Haskell implementation of
mu and nu types
17. Mon 27 Mar 2017 System F
Polymorphic Functions
Naturals and Lists in System F
Chapter 7 of Lecture Notes
Outline of Lecture 17
18. Thu 30 Mar 2017 Inductive Types
in System F
Outline of Lecture 18
19. Mon 3 Apr 2017 SEM/SET survey
Exam preparation
Exam Paper Spring 2013/14
20. Thu 6 Apr 2017 Exam preparation Exam Paper Autumn 2014/15
Easter Break
21. Mon 8 May 2017 G54FPP presentations ...
22. Thu 11 May 2017 G54FPP presentations ...
End of lectures

Coursework and Feedback

The coursework consists in four short tests on Moodle. Every couple of weeks you will find a quiz on the Moodle page. The quiz consists of 10 short questions; you have 30 minutes to answer them all. Access to the quiz will be open for the whole specified day. You can choose at what time you want to do it, but once you start you have half hour to complete it. You must solve it by yourself with no help from others. Be sure to read carefully the regulations about plagiarism in the student handbook. Each quiz will cover the material of the lectures up to the quiz's date.

Your coursework mark will be the average sum of the scores of all the tests; it counts for 25% of your final mark.

DateTestTopics
Fri 17 Feb 2017 Test 1 Lectures 1-5
Fri 10 Mar 2017 Test 2 Lectures 6-11
Fri 31 Mar 2017 Test 3 Lectures 12-17
Mon 15 May 2017 Test 4 Lectures 18-20

You can also raise your coursework mark by helping me improve the lecture notes: You get one point for every error you find on the lecture notes. So you may get full marks on the coursework by finding 25 mistakes! (Of course, you can't get more that 25%.) To claim this reward, post the error on the forum. Also questions and suggestions that lead to improvement of the notes will count. Only the first student to communicate a mistake will get the point for it.

Contacting the teacher

If you don't understand something or have any issues with the topics, don't be shy and ask. You can contact me by e-mail: put G54FOP/FPP in the subject line, so I know immediately that it is about this module.

G54FPP mini project

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 presentations will be on 8 and 11 May 2017.
The deadline for the report is 19 May 2017.
Hand in the hard copy of your report to Student Services before 15:00.

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.

Marking criteria

In the 10-pages FPP project report, you must explain a topic at a level that should be understandable to your classmates in G54FOP. The presentation will be given during the last FOP lecture and all the FOP students will attend it and have the opportunity to ask questions. You don't need to do an extensive review of the literature: I just point you to one or two articles or book chapters that you shuld refer to. You must read them, understand them (they are at a fairly advanced level) and then manage to synthesise the main ideas and some of the content in your report and presentation. You will be marked on the understanding that you show, the capacity to explain complex notions, the clarity and correctness of your exposition. I don't ask you to do original work, but simply to demonstrate insight about the material and ability to explain it clearly.

List of topics

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.)

  1. Functional Programming with Streams

    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.

  2. The Barendregt Cube

    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.

  3. Stream Differential Equations

    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.

  4. Labelled transition systems and bisimulation

    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.

  5. Data types in system F

    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.

  6. Infinite objects and proofs in type theory

    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.

  7. The calculus of communicating systems

    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.

  8. Hoare Logic

    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.

  9. The Pi Calculus

    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.

  10. Deriving Programs from Specifications

    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.