Agda is a dependently typed, total functional programming language and interactive theorem prover based on Martin-Löf’s type theory. It allows expressing programs and proofs in the same language, using the Curry–Howard correspondence. It features interactive development via Emacs, Atom, or VS Code. 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. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. 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 has many similarities with other proof assistants based on dependent types, such as Coq, Epigram, Matita and NuPRL.
Features
- Dependently typed language enabling encoding of proofs as types
- Totality and termination checking to ensure consistency
- Interactive proof development with metavariables and Emacs/Vim/VS Code integration
- Unicode support and syntax reminiscent of Haskell
- Standard library containing definitions for core data structures and proofs
- Backends including MAlonzo (Haskell) and JavaScript for compilation targets
Project Samples
