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.

The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax.

One of the distinctive features of Agda, when compared with other similar systems such as Coq, is heavy reliance on metavariables for program construction.

When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code.

This feature allows incremental program construction in a way similar to tactics-based proof assistants such as Coq.

Programming in pure type theory involves a lot of tedious and repetitive proofs.

Typically, this works by writing an Agda function that optionally returns a proof of some property of interest.

The reflection mechanism allows quoting program fragments into, or unquoting them from, the abstract syntax tree.

[12] Agda has an extensive de facto standard library, which includes many useful definitions and theorems about basic data structures, such as natural numbers, lists, and vectors.