## Introductions 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 - Yoshiki Kinoshita.
*On the Agda Language (in Japanese)*Slides (English) Slides (Japanese) - 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,
*Brutal [Meta]Introduction to Dependent Types in Agda* - Thorsten Altenkirch, Computer Aided Formal Reasoning - online lecture notes
- Daniel Licata.
*Dependently Typed Programming in Agda*(OPLSS 2013). - Tesla Ice Zhang
*Some books about Formal Verification in Agda (in Chinese)*

## General introductions to programming with dependent types:

- Nicolas Oury and Wouter Swierstra.
*The Power Of Pi*(ICFP 2008). - Conor McBride.
*Epigram: Practical Programming with Dependent Types*(also available from Conor's web page). Lecture notes for the AFP Summer School 2004.

Page last modified on March 23, 2020, at 10:33 PM

Powered by
PmWiki