agda/doc/user-manual/getting-started/tutorial-list.rst

.. _tutorial-list:

*******************
A List of Tutorials
*******************

.. note::
  Some of the materials linked on this page have been created for
  older versions of Agda and might no longer apply directly to the
  latest release.

Books on Agda
=============

- Phil Wadler, Wen Kokke, and Jeremy G. Siek (2019). `Programming
  Languages Foundations in Agda <https://plfa.github.io/>`__
- Aaron Stump (2016). `Verified Functional Programming in Agda
  <https://dl.acm.org/doi/book/10.1145/2841316>`__

Tutorials and lecture notes
===========================

- Jesper Cockx (2021). `Programming and Proving in Agda
  <https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf>`__.
  An introduction to Agda for a general audience of functional
  programmers. It starts from basic knowledge of Haskell and builds up
  to using equational reasoning to formally prove correctness of
  functional programs.
- Musa Al-hassy (2019). `A slow-paced introduction to reflection in Agda <https://github.com/alhassy/gentle-intro-to-reflection>`__.
- Jesper Cockx (2019). `Formalize all the things (in Agda) <https://jesper.sikanda.be/posts/formalize-all-the-things.html>`__.
- Jan Malakhovski (2013). `Brutal [Meta]Introduction to Dependent
  Types in Agda <https://oxij.org/note/BrutalDepTypes/>`__.
- Diviánszky Péter (2012). `Agda Tutorial
  <https://people.inf.elte.hu/divip/AgdaTutorial/Index.html>`__.
- Ana Bove, Peter Dybjer, and Ulf Norell (2009). `A Brief Overview of
  Agda - A Functional Language with Dependent Types
  <https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation?action=download&upname=AgdaOverview2009.pdf>`__
  (in TPHOLs 2009) with an example of reflection.  `Code
  <http://www.cse.chalmers.se/~ulfn/code/tphols09/>`__.
- Andreas Abel (2009). `An Introduction to Dependent Types and Agda
  <http://www2.tcs.ifi.lmu.de/~abel/DepTypes.pdf>`__.  Lecture notes
  used in teaching functional programming: basic introduction to Agda,
  Curry-Howard, equality, and verification of optimizations like
  fusion.
- Ulf Norell and James Chapman (2008). `Dependently Typed Programming
  in Agda
  <http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf>`__.
  This is aimed at functional programmers.
- Ana Bove and Peter Dybjer (2008). `Dependent Types at Work
  <http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf>`__.
  A gentle introduction including logic and proofs of programs.
- Anton Setzer (2008). `Lecture notes on Interactive Theorem Proving
  <http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html>`__. 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.

Videos on Agda
==============

- Conor McBride (2014). `Introduction to Dependently Typed Programming
  using Agda
  <https://www.youtube.com/playlist?list=PL44F162A8B8CB7C87>`__.
  (videos of lectures). `Associated source files, with exercises
  <https://personal.cis.strath.ac.uk/conor.mcbride/pub/dtp/>`__.
- Daniel Licata (2013). `Dependently Typed Programming in Agda
  <https://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html>`__
  (at OPLSS 2013).
- Daniel Peebles (2011). `Introduction to Agda
  <https://www.youtube.com/playlist?p=B7F836675DCE009C>`__.  Video of
  talk from the January 2011 Boston Haskell session at MIT.


Courses using Agda
==================

- `Computer Aided Reasoning <http://www.cs.nott.ac.uk/~psztxa/g53cfr/>`__
  Material for a 3rd / 4th year course (g53cfr, g54 cfr) at the university of Nottingham 2010 by Thorsten Altenkirch
- `Type Theory in Rosario <http://www.cs.nott.ac.uk/~psztxa/rosario/>`__
  Material for an Agda course in Rosario, Argentina in 2011 by  Thorsten Altenkirch
- `Software System Design and Implementation <http://www.cse.unsw.edu.au/~cs3141/>`__,
  undergrad(?) course at the University of New South Wales by Manuel Chakravarty.
- `Tüübiteooria / Type Theory <https://courses.cs.ut.ee/2011/typet/Main/HomePage>`__,
  graduate course at the University of Tartu by Varmo Vene and James Chapman.
- `Advanced Topics in Programming Languages: Dependent Type Systems <https://www.seas.upenn.edu/~sweirich/cis670/09/>`__,
  course at the University of Pennsylvania by Stephanie Weirich.
- `Categorical Logic <https://www.cl.cam.ac.uk/teaching/0910/L20/>`__,
  course at the University of Cambridge by Samuel Staton.
- `Dependently typed functional languages <http://www1.eafit.edu.co/asr/courses/dependently-typed-functional-languages/>`_,
  master level course at EAFIT University by Andrés Sicard-Ramírez.
- `Introduction to Dependently Typed Programming using Agda <https://github.com/mietek/agda-intro>`__,
  research level course at the University of Edinburgh by Conor McBride.
- `Agda <https://people.inf.elte.hu/divip/AgdaTutorial/Index.html>`__,
  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 <http://www.cse.chalmers.se/edu/course/DAT140/>`__,
  course at Chalmers University of Technology.
- `Advanced Functional Programming <https://www.tcs.ifi.lmu.de/lehre/ss-2012/fun>`__
  (in German), course at Ludwig-Maximilians-University Munich.
- `Dependently typed metaprogramming (in Agda) <https://danel.ahman.ee/agda-course-13/>`__,
  Summer (2013) course at the University of Cambridge by Conor McBride.
- `Computer-Checked Programs and Proofs <http://dlicata.web.wesleyan.edu/teaching/ccpp-f13/>`__
  (COMP 360-1), Dan Licata, Wesleyan, Fall 2013.
- `Advanced Functional Programming Fall 2013 <https://github.com/pigworker/CS410-13>`__
  (CS410), Conor McBride, Strathclyde, `notes from 2015 <https://github.com/pigworker/CS410-15/blob/master/CS410-notes.pdf>`__, `videos from 2017 <https://github.com/pigworker/CS410-17/>`__.
- `Interactive Theorem proving <http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/>`__
  (CS__336), Anton Setzer, Swansea University, Lent 2008.
- `Inductive and inductive-recursive definitions in Intuitionistic Type Theory <https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html>`__,
  lectures by Peter Dybjer at the Oregon Programming Languages Summer School 2015.
- `Introduction to Univalent Foundations of Mathematics with Agda <https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html>`__ ,
  MGS 2019 Martín Hötzel Escardó
- `Higher-Dimensional Type Theory <https://favonia.org/courses/hdtt2020/>`__ (CSCI 8980), courses on homotopy type theory and cubical type theory, Favonia, the University of Minnesota, Spring 2020
- `Correct-by-construction Programming in Agda
  <https://github.com/jespercockx/ohrid19-agda>`__, a course at the
  EUTYPES Summer School '19 in Ohrid.
- `Lectures on Agda <https://www.mathstat.dal.ca/~selinger/agda-lectures/>`__,
  a course by Peter Selinger at Dalhousie University, Winter 2021.

Miscellaneous
=============

- Agda has a `Wikipedia page
  <https://en.wikipedia.org/wiki/Agda_(programming_language)>`__