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.
Somewhat tentative overview; in particular towards the end.
OLN = Own Lecture Notes. For other references, see list at end of page.
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]|
|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.
G54FPP (optional mini-project) assessment:
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
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:
10 % of the overall G54FPP mark is for active participation in the presentations. Concretely, this means:
Presentation topics and schedule, 14 May 2013:
|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|
|10:00||Roland Thiolliere||Program correctness for distributed systems||Niall|
|10:25||Andrew Burnett||The pi calculus: A Process Calculi||Michael|
|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|
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):