Language
Agda
Dependently typed, purely functional programming language and proof assistant
2007Appeared
manifest typing, static typing, nominative typing, dependent typing, inference typing, strong typingType system
2.8.0.2Latest version
1Languages it influenced
Facts
- Appeared
- 2007
- Type system
- manifest typing, static typing, nominative typing, dependent typing, inference typing, strong typing
- Latest version
- 2.8.0.2 (September 13, 2026)
- Languages it influenced
- 1
- Kind
- proof assistant, purely functional programming language, free software, functional programming language, dependently typed programming language
- Paradigms
- purely functional programming
- Developer
- Chalmers University of Technology
- Influenced by
- Rocq prover, Haskell, Epigram
- Implemented in
- Haskell
- File extensions
- .agda .lagda
- Licence
- BSD licenses
- Operating system
- Microsoft Windows, Unix-like operating system
- Influences listed
- 3
Sources: Wikidata (CC0) · Wikidata Q20479
Influenced · 1
| Language | Appeared | Paradigms | Type system | Languages it influenced |
|---|---|---|---|---|
| Idris | 2007 | total functional programming, functional programming, purely functional programming | static typing, dependent typing, linear typing, uniqueness typing | — |