# A List of Tutorials¶

## Introduction to Agda¶

- Ulf Norell and James Chapman.
- Dependently Typed Programming in Agda. This is aimed at functional programmers.

- Ana Bove and Peter Dybjer.
- Dependent Types at Work. A gentle introduction including logic and proofs of programs.

- Ana Bove, Peter Dybjer, and Ulf Norell.
- A Brief Overview of Agda - A Functional Language with Dependent Types (in TPHOLs 2009) with an example of reflection. Code

- Anton Setzer.
- Lecture notes on Interactive Theorem Proving. Swansea University. These lecture notes are based on Agda and contain an introduction of Agda for students with a very basic background in logic and functional programming.

- Daniel Peebles.
- Introduction to Agda. Video of talk from the January 2011 Boston Haskell session at MIT.

- Conor McBride.
- Introduction to Dependently Typed Programming using Agda. (videos of lectures). Associated source files, with exercises.

- Andreas Abel.
- Agda lecture notes. Lecture notes used in teaching functional programming: basic introduction to Agda, Curry-Howard, equality, and verification of optimizations like fusion.

- Jan Malakhovski.

- Thorsten Altenkirch.
- Computer Aided Formal Reasoning - online lecture notes

- Daniel Licata.
- Dependently Typed Programming in Agda (OPLSS 2013).

- Phil Wadler.

- Aaron Stump.

- Diviánszky Péter.

- Musa Al-hassy.

## Courses using Agda¶

- Computer Aided Reasoning Material for a 3rd / 4th year course (g53cfr, g54 cfr) at the university of Nottingham 2010 by Thorsten Altenkirch
- Type Theory in Rosario Material for an Agda course in Rosario, Argentina in 2011 by Thorsten Altenkirch
- Software System Design and Implementation , undergrad(?) course at the University of New South Wales by Manuel Chakravarty.
- Tüübiteooria / Type Theory , graduate course at the University of Tartu by Varmo Vene and James Chapman.
- Advanced Topics in Programming Languages: Dependent Type Systems , course at the University of Pennsylvania by Stephanie Weirich.
- Categorical Logic , course at the University of Cambridge by Samuel Staton. - More info and feedback
- Dependently typed functional languages , master level course at EAFIT University by Andrés Sicard-Ramírez.
- Introduction to Dependently Typed Programming using Agda , research level course at the University of Edinburgh by Conor McBride.
- Agda , introductory course for master students at ELTE Eötvös Collegium in Budapest by Péter Diviánszky and Ambrus Kaposi.
- Types for Programs and Proofs , course at Chalmers University of Technology.
- Advanced Functional Programming (in German), course at Ludwig-Maximilians-University Munich.
- Dependently typed metaprogramming (in Agda) , Summer (2013) course at the University of Cambridge by Conor McBride.
- Computer-Checked Programs and Proofs (COMP 360-1), Dan Licata, Wesleyan, Fall 2013.
- Advanced Functional Programming Fall 2013 (CS410), Conor McBride, Strathclyde, notes from 2015, videos from 2017.
- Interactive Theorem proving (CS__336), Anton Setzer, Swansea University, Lent 2008.
- Inductive and inductive-recursive definitions in Intuitionistic Type Theory , lectures by Peter Dybjer at the Oregon Programming Languages Summer School 2015.
- Introduction to Univalent Foundations of Mathematics with Agda , MGS 2019 Martín Hötzel Escardó

## Miscellaneous¶

- Agda has a Wikipedia page