PLDB
Languages Features Calendar CSV Lists Blog About Sponsor Add Language
GitHub icon

Agda

Agda

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

#173on PLDB 15Years 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 Example Token
MultiLine Comments
Integers
-- \d+
Floats
-- \d+[eE][+-]?\d+
Hexadecimals
-- 0[xX][\da-fA-F]+
Strings
"Hello world"
"
Print() Debugging putStrLn
Comments
-- A comment
Line Comments
-- A comment
--
Typed Holes
Semantic Indentation ϴ

Books about Agda on goodreads

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

Books about Agda from ISBNdb

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
blitzbasic.html · agda.html · frege.html

View source

PLDB - Build the next great programming language · v2022 · Day 32 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub · feedback@pldb.com