- functional programming with dependent types;
- computer-assisted interactive proving in logical systems, including predicate logic;
- proving the correctness of functional programs;
- type systems and operational semantics for programming languages.

- Thursdays 10.00 – 11.45 beginning on 6 September.
- Mondays 13.15 – 15.00 beginning on 10 September.

Plan for lectures, exercise sessions and homework

- Mondays 15.15 – 17.00 beginning on 10 September.

- Thierry Coquand (TC), course responsible

- Peter Dybjer (PD),
course responsible

- Ulf Norell (UN), guest lecturer

- Fabian Ruch (FR), course assistant
- Andrea
Vezzosi (AV), course assistant

- The Agda User
Manual (including a section on Agda's
**Emacs mode**) - The Agda Homepage
- An Introduction to Programming and Proving in Agda preliminary lecture notes by Peter Dybjer
- Dependent Types at Work by Ana Bove and Peter Dybjer
- Dependently Typed Programming in Agda by Ulf Norell and James Chapman

- Types and Programming Languages by Benjamin Pierce, MIT Press. It is available online from Chalmers library.
- Verified Functional Programming in Agda by Aaron Stump, ACM Digital Library. Suggested reading is chapter 1-5. The book is available online from Chalmers library.
- The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software using the Coq system. (This is supplementary reading.)
- Programming Language Foundations in Agda by Wen Kokke and Phil Wadler.

- Computability via PCF by Peter Dybjer.

- Functional programming (essential).
- Basic knowledge of logic, including predicate logic.
- Some knowledge about programming languages.

- Take home exam: Tuesday 23 October 8.00 – Friday 26 October 12.00.
**Presentation of advanced topic or of an Agda development**. You should work in pairs and choose a topic no later than on Thursday 20 September 13.15. You will also be**opponents**for one of the presentations. Here are some talk proposals. Register your topic on this wiki. Bonus points will also be given for good presentations and opposition (max 4 pts) and for**attendance**at the presentations (max 3 x 1 pts).**Homework**. Bonus points will be given to students who have handed in homework and been prepared to present it in class (max 4 x 3 pts). The Fire system should be used for submitting your homework. Handwritten homework can also be handed in in class. Do**not**submit homework by email.- Both presentation and take home exam are obligatory. Homework is optional.
**Oral exam**. To get the grades 4 or 5, you need to take a short oral exam.

- Type Theory article in Stanford Encyclopedia of Philosophy by Thierry Coquand.
- Intuitionistic Type Theory article in Stanford Encyclopedia of Philosophy by Peter Dybjer and Erik Palmgren.
- Proving properties of programs by structural induction by Rod Burstall.
- Correctness of a Compiler for Arithmetic Expressions by John McCarthy and James Painter.
- The history of operational semantics by G. Plotkin.
- A video tutorial on operational semantics by D. Van Horn.
- Papers on parametric polymorphism by J. Reynolds.
- History of LISP by P. Graham.
- Homotopy Type Theory: Univalent Foundations of Mathematics.

- Tobias Andersson, tobande@student.chalmers.se
- Robert Krook, guskrooro@student.gu.se
- Heyu Qin, heyu@student.chalmers.se
- Ayberk Tosun, ayberk@student.chalmers.se