- FOP in the module catalogue
- FPP in the module catalogue
- Announcements on Moodle (announcements will be emailed to you automatically; login required)
- Moodle discussion forum (please ask questions here or in the lecture; login required)
- Venanzio Capretta's website for this module (last year)

- 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

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

- Test 1, Wednesday 2 May 2018
- Test 2, Wednesday 9 May 2018
- Test 3, Wednesday 16 May 2018

- Agda wiki
- Agda documentation (installation and much more)
- Agda on GitHub (install development version)
- Agda standard library on GitHub

- Lecture 3: as html (view in browser) and as .agda (open in emacs)
- Lecture 6: as html (view in browser) and as .agda (open in emacs)

- See Venanzio's recommendations and lecture notes
- For semantics: see Andrew Pitt's website (includes detailed notes)
- For Agda: see the links given above, and Thorsten Altenkirch's course
- ... (will be added later when we discuss other topics)

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.

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

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