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 original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally named Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition. Wikipedia

Created Year: 2007
Developed by: Chalmers University of Technology
Operating systems: Microsoft Windows • Unix-like operating system
Implemented in: Haskell
File extensions: agda, lagda

Wikidata: Q20479

Influenced: Idris

Influenced by: Epigram • Haskell • Rocq

Programming paradigms: purely functional programming

Language types: dependently typed programming language • functional programming language • purely functional programming language

module agda where
open import IO

main = run (putStrLn "Hello World")