Agda (programming language) Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate tactics language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. Agda is based on Zhaohui Luo's unified theory of dependent types (UTT), a type theory similar to Martin-Löf type theory.
- Brutal [Meta]Introduction to Dependent Types in Agda
- Learn you and Agda and achieve enlightenment
- Agda vs. Coq vs. Idris
- Agda vs. Coq
- Dependently Typed Programming in Agda
- Dependent Types at Work
- A Brief Overview of Agda - A Functional Language with Dependent Types
- (Programming Languages) in Agda = Programming (Languages in Agda) by Philip Wadler
- Twitch: Proving things using Agda!
- Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
- "A Little Taste of Dependent Types" by David Christiansen
- David Sankel: The Intellectual Ascent to Agda
- A Demonstration of Agda
- Conor McBride - Dependently-Typed Metaprogramming: Introduction via Vectors