Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length, and dependent pattern matching on such types. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive mode which can assist the programmer in writing the program. It shares many features with other purely functional programming languages, such as Haskell and Idris.
Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It supports proof automation and writing tactics through its reflection API. It has many similarities with other proof assistants based on dependent types, such as Rocq, Lean, and F*.
Agda is open-source and enjoys contributions from many authors. Agda 2 was originally written by Ulf Norell and is currently actively developed mainly by Andreas Abel, Nathaniel Burke, Lawrence Chonavel, Jesper Cockx, Nils Anders Danielsson, and András Kovács.
Latest releases
- 2026-06-17: Agda Standard Library 2.4 (all versions)
- 2025-07-05: Version 2.8.0 (all versions)
Getting started
- Install Agda on your own PC or try out Agda in the browser with the Agda Pad.
- Get your feet wet with a taste of Agda or one of the other language tutorials.
- Read about library management and other Agda features in the user manual.
- Ask any questions on the Agda mailing list or on the Agda Zulip server.
- Report bugs and feature requests to the issue tracker.
Agda libraries
- Standard library
- std-lib-classes (typeclasses) and std-lib-meta (metaprogramming and tactics)
- Cubical (standard library for Cubical Agda)
- Categories (category theory in Agda)
- UniMath (univalent mathematics in Agda, mainly formalizing existing mathematics)
- TypeTopology (univalent mathematics in Agda, mainly developing new mathematics)
- Other libraries and developments
Agda meetings
- Agda Implementors’ Meeting XLIII took place in Rzeszów, Poland from 2026-10-19 to 2026-10-24.
- Agda Implementors’ Meeting XLII took place in Leuven, Belgium from Monday 13 to Saturday 18 April 2026.
- Past Agda Meetings.