The Agda standard library : version 2.0

Tools

Daggitt, Matthew L. and Allais, Guillaume and McKinna, James and Abel, Andreas and van Doorn, Nathan and Wood, James and Norell, Ulf and Kidney, Donnacha Oisín and Meshveliani, Sergei and Stucki, Sandro and Carette, Jacques and Rice, Alex and Hu, Jason Z. S. and Xia, Li-yao and You, Shu-Hung and Mullanix, Reed and Kokke, Wen (2025) The Agda standard library : version 2.0. Journal of Open Source Software, 10 (116). 9241. ISSN 2475-9066 (https://doi.org/10.21105/joss.09241)

[thumbnail of Daggitt-etal-JOSS-2025-The-Agda-standard-library-version-2]
Preview
 Text. Filename: Daggitt-etal-JOSS-2025-The-Agda-standard-library-version-2.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (223kB)| Preview

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.

ORCID iDs

Daggitt, Matthew L., Allais, Guillaume ORCID logoORCID: https://orcid.org/0000-0002-4091-657X, McKinna, James, Abel, Andreas, van Doorn, Nathan, Wood, James, Norell, Ulf, Kidney, Donnacha Oisín, Meshveliani, Sergei, Stucki, Sandro, Carette, Jacques, Rice, Alex, Hu, Jason Z. S., Xia, Li-yao, You, Shu-Hung, Mullanix, Reed and Kokke, Wen;
CORE (COnnecting REpositories)