G54FOP/FPP Mathematical Foundations of Programming & Optional Mini-Project

Spring 2013

Model answers to the May 2013 exam now available!

Overview


Literature

There is no main reference, except for your own notes from the lectures along with any electronic lecture slides [ELS13] or other supplementary material. However, you will likely find it useful to have a book to give you an additional perspective on and more depth to the material covered, as well as a help to understand some of the harder topics. Some suggestions below.

The book Types and Programming Languages [Pie02] by Benjamin Pierce covers many of the topics of the module in depth. It is recommended though not essential reading. The book itself is very good for further studies, both as a textbook and as a reference book. The library has copies.

The G52MAL lecture notes [AN07] (PDF) provides additional background on formal language theory for those who need that. Alternatively, pretty much any book on formal languages and automata theory will also do, e.g. Introduction to Automata Theory, Languages, and Computation, 2nd edition [HMU01] by John E. Hopcroft, Rajeev Motwani & Jeffrey D. Ullman.


Lectures

Somewhat tentative overview; in particular towards the end.

OLN = Own Lecture Notes. For other references, see list at end of page.

Lecture#DateContentReading
1 31 Jan Administrative Details and Introduction;
Basic Formal Language Notions and Abstract Syntax
[ELS13, Le 1-A]
[OLN; ELS13, Le 1; AN07, pp. 6, pp. 21–37; HMU01, ch. 1, pp. 169–207, 211–214; Pie02, ch. 3, p. 53]
2 1 Feb Abstract Syntax and Induction on Terms [ELS13, Le 2; OLN; Pie02, ch. 2]
3 7 Feb Introduction to Programming Language Semantics [ELS13 Le 3; OLN; Pie02, ch. 3]
4 8 Feb Operational Semantics I: Basics [OLN; Pie02, ch. 3]
5 14 Feb Operational Semantics II: Induction on Derivations [ELS13 Le 5; OLN; Pie02, ch. 3]
6 15 Feb Operational Semantics III: State [ELS12 Le 6; OLN; Pie02, ch. 13
7 21 Feb The Untyped Lambda-Calculus I: Introduction [ELS13, Le 7; OLN; Pie02, ch. 5]
8 22 Feb The Untyped Lambda-Calculus II: Programming in the Lambda Calculus [OLN; Pie02, ch. 5]
9 28 Feb The Untyped Lambda-Calculus III: Programming in the Lambda Calculus (cont.) [OLN; Pie02, ch. 5]
10 1 Mar The Untyped Lambda-Calculus IV: Recursion [OLN; Pie02, ch. 5]
-- 7 Mar CANCELLED
-- 8 Mar CANCELLED
11 14 Mar The Untyped Lambda-Calculus V: Operational Semantics and Reduction Orders [ELS13 Le 11; OLN; Pie02, ch. 5]
12 15 Mar Types and Type Systems I [ELS13, Le 12; OLN; Pie02, ch. 1, ch. 8]
13 21 Mar Types and Type Systems II [ELS13, Le 13; OLN; Pie02, ch. 14, ch. 9]
14 22 Mar The Polymorphic Lambda Calculus (System F) [ELS13 Le 14; OLN; Pie02, ch. 23]
15 25 Apr Denotational Semantics and Domain Theory I [ELS13 Le 15; OLN]
16 26 Apr Denotational Semantics and Domain Theory II [ELS13 Le 16; OLN]
17 2 May Denotational Semantics and Domain Theory III [ELS13 Le 17 & 18; OLN]
18 3 May Denotational Semantics and Domain Theory IV [ELS13 Le 17 & 18; OLN]
19 9 May No lecture
20 10 May No lecture

Copies of lecture notes, slides, any major pieces of program code, or other electronic material used during the lectures can be found here.


Assessment

G54FOP assessment:

See below for further details on the examination. (Any resit is also 100 % exam.)

G54FPP (optional mini-project) assessment:

However, in the case of a resit: See below for further details on G54FPP: the optional mini-project.


G54FPP: Optional 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. A list of suggested topics is available here. However, it is not exclusive: feel free to discuss other topics or amended versions of the suggested ones with the G54FOP/FPP convenor.

Once a topic has been chosen, the task is to

on this topic.

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.

Deadline for the report: Friday 3 May 2013, 17:00.

The front cover of the report should clearly state:

Submission: Electronically using the CW system, PDF format only.

The presentation should be an introduction to your topic, targeted so that it is understandable to your peers given what we have covered in this module. Thus you can assume a knowledgeable audience, and then in particular, a good understanding of G54FOP (and prerequisites), but not any specific knowledge about your particular topic. Each student gets a 25 minute slot: 20 for the actual presentation, 5 for discussion. Slides and/or the whiteboard can be used.

The presentations will take place 14 May, 9:00–12:00, C1 the Exchange.

For the discussion, a “discussant” model will be adopted: each student will be appointed to lead the discussion on one of the other students' presentations. The discussion be structured to:

The discussant will need to prepare for this by reading through the report in some depth before the presentation. The discussant should also ensure the rest of the audience gets an opportunity to ask questions.

10 % of the overall G54FPP mark is for active participation in the presentations. Concretely, this means:

Presentation topics and schedule, 14 May 2013:
TimeStudentTopicDiscussant
9:00 Niall O'Dwyer Dead-code elimination, variable liveness, and expression availability David
9:25 Michael Gale What should I wear? Parametric polymorphism and its decidability Laurence
9:50–10:00: Break
10:00 Roland Thiolliere Program correctness for distributed systems Niall
10:25 Andrew Burnett The pi calculus: A Process Calculi Michael
10:50–11:00: Break
11:00 David McGillicuddy Premises: easy to make, hard to evaluate — a review of abstract machines Roland
11:25 Laurence Herbert Techniques for proving Program Correctness — Hoare & Separation Logic Andrew


Examination

Some basic information about the exam:

Past examination papers can be found via the Intranet Portal under the Library Tab. Search for Exam Papers. Or see here for further info.

Model answers to some past exams can be found here (note that exam formats may vary slightly, e.g. number of compulsory questions):


References


Last updated 5 June 2013.