The Agda standard library: version 2.0

Matthew L. Daggitt; Guillaume Allais; James McKinna; Andreas Abel; Nathan van Doorn; James Wood; Ulf Norell; Donnacha Oisín Kidney; Sergei Meshveliani; Sandro Stucki; Jacques Carette; Alex Rice; Jason Z. S. Hu; Li-yao Xia; Shu-Hung You; Reed Mullanix; Wen Kokke

doi:10.21105/joss.09241

The Agda standard library: version 2.0

Matthew L. Daggitt, Guillaume Allais, James McKinna, Andreas Abel, Nathan van Doorn, James Wood, Ulf Norell, Donnacha Oisín Kidney, Sergei Meshveliani, Sandro Stucki, Jacques Carette, Alex Rice, Jason Z. S. Hu, Li-yao Xia, Shu-Hung You, Reed Mullanix, Wen Kokke

Research output: Contribution to journal › Article › peer-review

Abstract

Agda (The Agda Development Team, 2024) is a dependently-typed functional language that serves as both a programming language and an interactive theorem prover (ITP). In Agda, one can formulate requirements on programs as types and build programs satisfying these requirements interactively. The Curry-Howard correspondance (Wadler, 2015) allows types and programs to be seen as theorems and proofs. We present the Agda standard library (The Agda community, 2023) (agda-stdlib), which provides functions and mathematical concepts helpful in the development of both programs and proofs.

Original language	English
Article number	9241
Number of pages	4
Journal	Journal of Open Source Software
Volume	10
Issue number	116
DOIs	https://doi.org/10.21105/joss.09241
Publication status	Published - 20 Dec 2025

Keywords

Agda
language extensions
functional programming

Access to Document

10.21105/joss.09241Licence: CC BY 4.0

Daggitt-etal-JOSS-2025-The-Agda-standard-library-version-2Final published version, 218 KBLicence: CC BY 4.0

Cite this

@article{ec487d3f6e4f43d0acbb01c977be793a,

title = "The Agda standard library: version 2.0",

abstract = "Agda (The Agda Development Team, 2024) is a dependently-typed functional language that serves as both a programming language and an interactive theorem prover (ITP). In Agda, one can formulate requirements on programs as types and build programs satisfying these requirements interactively. The Curry-Howard correspondance (Wadler, 2015) allows types and programs to be seen as theorems and proofs. We present the Agda standard library (The Agda community, 2023) (agda-stdlib), which provides functions and mathematical concepts helpful in the development of both programs and proofs.",

keywords = "Agda, language extensions, functional programming",

author = "Daggitt, \{Matthew L.\} and Guillaume Allais and James McKinna and Andreas Abel and \{van Doorn\}, Nathan and James Wood and Ulf Norell and Kidney, \{Donnacha Ois{\'i}n\} and Sergei Meshveliani and Sandro Stucki and Jacques Carette and Alex Rice and Hu, \{Jason Z. S.\} and Li-yao Xia and Shu-Hung You and Reed Mullanix and Wen Kokke",

year = "2025",

month = dec,

day = "20",

doi = "10.21105/joss.09241",

language = "English",

volume = "10",

number = "116",

}

TY - JOUR

T1 - The Agda standard library

T2 - version 2.0

AU - Daggitt, Matthew L.

AU - Allais, Guillaume

AU - McKinna, James

AU - Abel, Andreas

AU - van Doorn, Nathan

AU - Wood, James

AU - Norell, Ulf

AU - Kidney, Donnacha Oisín

AU - Meshveliani, Sergei

AU - Stucki, Sandro

AU - Carette, Jacques

AU - Rice, Alex

AU - Hu, Jason Z. S.

AU - Xia, Li-yao

AU - You, Shu-Hung

AU - Mullanix, Reed

AU - Kokke, Wen

PY - 2025/12/20

Y1 - 2025/12/20

N2 - Agda (The Agda Development Team, 2024) is a dependently-typed functional language that serves as both a programming language and an interactive theorem prover (ITP). In Agda, one can formulate requirements on programs as types and build programs satisfying these requirements interactively. The Curry-Howard correspondance (Wadler, 2015) allows types and programs to be seen as theorems and proofs. We present the Agda standard library (The Agda community, 2023) (agda-stdlib), which provides functions and mathematical concepts helpful in the development of both programs and proofs.

AB - Agda (The Agda Development Team, 2024) is a dependently-typed functional language that serves as both a programming language and an interactive theorem prover (ITP). In Agda, one can formulate requirements on programs as types and build programs satisfying these requirements interactively. The Curry-Howard correspondance (Wadler, 2015) allows types and programs to be seen as theorems and proofs. We present the Agda standard library (The Agda community, 2023) (agda-stdlib), which provides functions and mathematical concepts helpful in the development of both programs and proofs.

KW - Agda

KW - language extensions

KW - functional programming

U2 - 10.21105/joss.09241

DO - 10.21105/joss.09241

M3 - Article

SN - 2475-9066

VL - 10

JO - Journal of Open Source Software

JF - Journal of Open Source Software

IS - 116

M1 - 9241

ER -

The Agda standard library: version 2.0

Abstract

Keywords

Access to Document

Fingerprint

Cite this