← All repos

agda

Agda is a dependently typed programming language / interactive theorem prover.

agdadependent-typesprogramming-languageproof-assistanttype-theory
Browse cluster: Lean4 Formal Verification & Cryptography
24,168commits
273contributors
14languages

Tech stack & purpose

Agda is a dependently typed programming language and interactive theorem prover built in Haskell. The repository contains the Agda language implementation along with its core library, backends for compilation to Haskell (GHC) and JavaScript, an Emacs mode for editing, and extensive documentation and testing infrastructure. The project is maintained by a community with contributions tracked through GitHub, and includes tooling for benchmarking, license reporting, and bisecting regressions.

Community & reference links

Languages

Haskell
55.5%
Agda
27.7%
TeX
6.6%
PostScript
3.8%
HTML
3.1%
Emacs Lisp
1.5%
Yacc
0.6%
Makefile
0.5%
Shell
0.3%
JavaScript
0.3%
Lex
0.1%
Nix
0.1%
CSS
0.0%
Perl
0.0%

Contributors (top 30 of 273)