The Agda standard library: version 2.0
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.
Authors
- Matthew L. Daggitt (ORCID: https://orcid.org/0000-0002-2552-3671)
- Andreas Abel (ORCID: https://orcid.org/0000-0003-0420-4492)
- Guillaume Allais (ORCID: https://orcid.org/0000-0002-4091-657X)
- Ulf Norell
- James Wood (ORCID: https://orcid.org/0000-0002-8080-3350)
- Reed Mullanix (ORCID: https://orcid.org/0000-0002-7970-4961)
- Sandro Stucki (ORCID: https://orcid.org/0000-0001-5608-8273)
- Jason Z. S. Hu (ORCID: https://orcid.org/0000-0001-6710-6262)
- Li-yao Xia (ORCID: https://orcid.org/0000-0003-2673-4400)
- S. D. Meshveliani (ORCID: https://orcid.org/0000-0002-4224-6178)
- James McKinna (ORCID: https://orcid.org/0000-0001-6745-2560)
- Donnacha Oisín Kidney (ORCID: https://orcid.org/0000-0003-4952-7359)
- Jacques Carette (ORCID: https://orcid.org/0000-0001-8993-9804)
- Wen Kokke (ORCID: https://orcid.org/0000-0002-1662-0381)
- Alex Rice (ORCID: https://orcid.org/0000-0002-2698-5122)
- Shu-Hung You (ORCID: https://orcid.org/0009-0003-0003-3945)
- Nathan van Doorn (ORCID: https://orcid.org/0009-0009-0598-3636)
Institutions
- Northwestern University (US)
- Amazon (United States) (US)
- Russian Academy of Sciences (RU)
- Institut national de recherche en sciences et technologies du numérique (FR)
- The University of Western Australia (AU)
- University of Strathclyde (GB)
- Heriot-Watt University (GB)
- Huawei Technologies (United Kingdom) (GB)
- Imperial College London (GB)
- Chalmers University of Technology (SE)
- University of Gothenburg (SE)
- McMaster University (CA)
- University of Edinburgh (GB)
Publication Details
- Journal
- The Journal of Open Source Software
- Published
- 2025-12-20
- DOI
- https://doi.org/10.21105/joss.09241
- Primary Topic
- Mathematics, Computing, and Information Processing
- Type
- article
- Field-Weighted Citation Impact
- 0.00