Basic Links
Lecture Notes and Lectures
- Nicolai's lecture notes (after each lecture, I will try to write up what we have done and make these notes available here)
- Venanzio's lecture notes
In any case, I strongly advise you to take your own notes during the lecture!
Log of the lecture:
- Lecture 1 --- 31 Jan 2018 --- Nicolai --- discussed syntax and semantics; specified the syntax of a simple language of arithmetical expressions via a Backus-Naur form and via derivation rules; gave one possible denotational semantic
- Lecture 2 --- 01 Feb 2018 --- Nicolai --- continued with the simple language; gave an example of a possible operational semantic; proved confluence for our language and discussed that confluence can fail for other languages
- Lecture 3 --- 07 Feb 2018 --- Nicolai --- introduction to Agda; see the Agda file linked below (in section "Agda")
- Lecture 4 --- 08 Feb 2018 --- Nicolai --- discussed G54FPP projects; normal form theorem for our laguage of arithmeitcal epressions; part of proof of statement that "[[e]] is value => e reduces to value"
- Lecture 5 --- 14 Feb 2018 --- Nicolai --- induction principle for the language of arithmetical expressions, use it to prove the theorem ([[e]] = True => e ->* t) and ([[e]] = False => e ->* f) and ([[e]] = n => e -> s(s(...(s z)...)))
- Lecture 6 --- 15 Feb 2018 --- Nicolai --- implemented operational semantics in Agda, see Agda file linked below
- Lecture 7 --- 21 Feb 2018 --- Venanzio --- introduction to λ-calculus
- Lecture 8 --- 22 Feb 2018 --- Venanzio --- data structures in λ-calculus: Church Numerals
- Lecture 9 --- 28 Feb 2018 --- Venanzio --- abstract syntax trees, substitution, Booleas and pairs
- Lecture 10 --- 1 Mar 2018 --- Venanzio --- recursion in λ-calculus, Y combinator
- Lecture 11 --- 7 Mar 2018 --- Venanzio --- simply typed λ-calculus
- Lecture 12 --- 8 Mar 2018 --- Venanzio --- System T
- Lecture 13 --- 14 Mar 2018 --- Venanzio --- Recursive types - Inductive
- Lecture 14 --- 15 Mar 2018 --- Venanzio --- CoInductive types
- Lecture 15 --- 21 Mar 2018 --- Venanzio --- (Initial) Algebras and (Final) Coalgebras
- Lecture 16 --- 22 Mar 2018 --- Venanzio --- System F
- Lecture 17 --- 25 Apr 2018 --- Venanzio --- Review of Type Systems
- Lecture 18 --- 2 May 2018 --- Nicolai --- Basics of System F
- Lecture 19 --- 3 May 2018 --- Nicolai --- Revision of main topics, exam preparation; final lecture of the module
Assessment and Coursework for G54FOP
On-line Tests
The coursework consists in three short tests on Moodle.
Every week 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.
- Test 1, Wednesday 2 May 2018
- Test 2, Wednesday 9 May 2018
- Test 3, Wednesday 16 May 2018
Previous Years Exam Papers
Agda
Agda is a programming language and a proof assistant.
Here are some links to help you install and learn Agda:
Agda file from the lecture:
Recommended Sources
G54FPP mini project
This module can be taken in addition to G54FOP.
It gives you the opportunity to learn more about a specific topic that is related to FOP.
Your task is to:
- Choose a topic: this can be one that I suggest (see below), or one that you come up with yourself.
- Work on the topic: this can include an Agda formalisation and/or literature work, depending on what you have chosen.
- Write a report on what you have done or found out: it should be understandable for your FOP classmates.
- Give a presentation for the rest of the class.
Timewise, the plan is as follows.
You should choose a topic at the end of February.
You then will have March and April (plus early May) to work on it.
The presentations will be in early May, and the reports should be handed in shortly after.
Update: Please submit your report by 14 May. Presentations will take place on 18 May.
Agda projects include a formalisation (you can also use Coq if you prefer).
Some suggested topics are ("A" for "Agda"):
- Formalise the confluence result for operational semantics (lecture 2).
- Formalise the connection between denotational and operational semantics (lecture 4; easier than lecture 2).
- Formalise the pidgeonhole principle.
- Formalise confluence for the lambda calculus (hard).
- Formalise different sorting algorithms.
- Formally prove that there are infinitely many primes.
- Suggest your own formalisation project (e.g. basic automaton theory, graph theory, ...).
Some none-formalisation topics could be (where "L" stands for "literature").
If you want to do any of these, we will discuss what exactly you would do.
They may still include Haskell or Agda, depending on your preferences.
- Primitive recursion and the Ackermann function.
- An introduction to Martin-Lof type theory.
- An introduction to automata theory.
- Any of the topics on Venanzio's website.
- Suggest your own topic (e.g. cryptography, blockchain, ...).