- The take home exam is now available. This refers to the following notes on simply typed lambda calculus. Note that successor should be a unary constructor (and not nullary as it was first written). The Fire system should be used for submitting your answers.
- Some key results about simply typed lambda calculus.
- The Agda User Manual includes a section on Agda's Emacs mode.
- A description of two simple and fundamental abstract machines.
- Note that lectures and exercise sessions are in several different rooms. Please consult TimeEdit for the correct information.
- Plan for lectures, exercise sessions and homework

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

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

- Computability via PCF by Peter Dybjer.

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

- Thursdays 10.00 - 11.45 beginning on 31 August.
- Mondays 13.15 - 15.00 beginning on 4 September.

- Mondays 15.15 - 17.00 beginning on 4 September.

**Take home exam**: Tuesday 17 October 800 - Friday 20 October 1200.**Presentation of advanced topic or of an Agda development**. You should work in pairs and choose a topic no later than on Thursday 14 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 at Chalmers, 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.

- Linus Johansson, linusjoh@student.chalmers.se
- Jacob Jonsson, jassob@dtek.se
- Joel Sjögren, joelsjogren.wii@gmail.com
- Nachiappan Valliappan, nacval@student.chalmers.se