Agda Programming Language
Agda is a dependently typed programming language based on intuitionistic type theory. It has inductive families, which are like Haskell’s GADTs, but they can be indexed by values and not just types.
Agda external tutorials
Awesome Agda tutorials and guides from all over the Internet.
- Programming Language Foundations in AgdaLevel: Beginner. By: Adam Chlipala. Duration: 20+ hours.A series of interactive and self-contained lectures covering the foundations of programming languages using Agda.