Agda - Programming language

< >

Agda is a programming language created in 2007 by Ulf Norell and Catarina Coquand.

 #173on PLDB 16Years Old 731Users 7Books 14Papers 2kRepos

Try now: TIO

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 current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. Read more on Wikipedia...

Example from hello-world:
```module agda where open import IO main = run (putStrLn "Hello World") ```
Example from Linguist:
```module NatCat where open import Relation.Binary.PropositionalEquality -- If you can show that a relation only ever has one inhabitant -- you get the category laws for free module EasyCategory (obj : Set) (_⟶_ : obj → obj → Set) (_∘_ : ∀ {x y z} → x ⟶ y → y ⟶ z → x ⟶ z) (id : ∀ x → x ⟶ x) (single-inhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s) where idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r idʳ x y r = single-inhabitant x y (r ∘ id y) r idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r idˡ x y r = single-inhabitant x y (id x ∘ r) r ∘-assoc : ∀ w x y z (r : w ⟶ x) (s : x ⟶ y) (t : y ⟶ z) → (r ∘ s) ∘ t ≡ r ∘ (s ∘ t) ∘-assoc w x y z r s t = single-inhabitant w z ((r ∘ s) ∘ t) (r ∘ (s ∘ t)) open import Data.Nat same : (x y : ℕ) (r s : x ≤ y) → r ≡ s same .0 y z≤n z≤n = refl same .(suc m) .(suc n) (s≤s {m} {n} r) (s≤s s) = cong s≤s (same m n r s) ≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z ≤-trans .0 y z z≤n s = z≤n ≤-trans .(suc m) .(suc n) .(suc n₁) (s≤s {m} {n} r) (s≤s {.n} {n₁} s) = s≤s (≤-trans m n n₁ r s) ≤-refl : ∀ x → x ≤ x ≤-refl zero = z≤n ≤-refl (suc x) = s≤s (≤-refl x) module Nat-EasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤-trans x y z) ≤-refl same ```
Example from Wikipedia:
```data _≤_ : ℕ → ℕ → Set where z≤n : {n : ℕ} → zero ≤ n s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m```

Language features

Feature Supported Token Example
Integers
`-- \d+`
Floats
`-- \d+[eE][+-]?\d+`
`-- 0[xX][\da-fA-F]+`
Strings "
`"Hello world"`
Print() Debugging putStrLn
`-- A comment`
`-- A comment`
Typed Holes
Semantic Indentation X

title author year reviews ratings rating
Verified Functional Programming in Agda Aaron Stump 0 1 4.00
Verified Functional Programming in Agda Aaron Stump 0 0 0.0
Programming Language Foundations in Agda Philip Wadler 0 0 0.0

title authors year publisher
Verified Functional Programming in Agda (ACM Books) Stump, Aaron 2016 ACM Books
Verified Functional Programming in Agda (ACM Books) Stump, Aaron 2016 ACM Books
Verified Functional Programming in Agda Aaron Stump 20160201 Morgan & Claypool Publishers
Verified Functional Programming in Agda Aaron Stump 20160201 Morgan & Claypool Publishers

Publications about Agda from Semantic Scholar

title authors year citations influentialCitations
A Brief Overview of Agda - A Functional Language with Dependent Types A. Bove and P. Dybjer and U. Norell 2009 248 22
On the bright side of type classes: instance arguments in Agda D. Devriese and F. Piessens 2011 62 2
Programming Language Foundations in Agda P. Wadler 2018 31 1
Verified Functional Programming in Agda Aaron Stump 2016 27 1
Integrating an Automated Theorem Prover into Agda S. Foster and G. Struth 2011 15 0
Pi-Ware: Hardware Description and Verification in Agda J. P. P. Flor and W. Swierstra and Y. Sijsling 2015 11 1
Auto in Agda - Programming Proof Search Using Reflection Pepijn Kokke and W. Swierstra 2015 11 2
Programming language foundations in Agda Wen Kokke and Jeremy G. Siek and P. Wadler 2020 6 0
Embedding a logical theory of constructions in Agda A. Bove and P. Dybjer and Andrés Sicard-Ramírez 2009 5 0
Dependently Typed Web Client Applications - FRP in Agda in HTML5 A. Jeffrey 2013 4 0
Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda Ernesto Copello and Á. Tasistro and Brunone Bianchi 2014 2 0
Formalizing Constructive Quantifier Elimination in Agda J. Pope 2018 1 0
Programming assurance cases in Agda M. Takeyama 2011 1 0
An approach to translating Haskell programs to Agda and reasoning about them H. Carr and Christa Jenkins and Mark Moir and Victor Cacciari Miraldo and Lisandra Silva 2022 1 0
limbo.html · agda.html · blitzbasic.html
- Build the next great programming language · Search · Day 213 · About · Blog · Acknowledgements · Traffic · Traffic Today · GitHub · feedback@pldb.com