| Title: |
The Agda standard library : version 2.0 |
| Authors: |
Daggitt, Matthew L.; Allais, Guillaume; 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; Kokke, Wen |
| Publication Year: |
2025 |
| Collection: |
University of Strathclyde Glasgow: Strathprints |
| Subject Terms: |
Computer software |
| Description: |
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. |
| Document Type: |
article in journal/newspaper |
| File Description: |
text |
| Language: |
unknown |
| ISSN: |
2475-9066 |
| Relation: |
https://strathprints.strath.ac.uk/95153/1/Daggitt-etal-JOSS-2025-The-Agda-standard-library-version-2.pdf; 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 |
| DOI: |
10.21105/joss.09241 |
| Availability: |
https://strathprints.strath.ac.uk/95153/; https://doi.org/10.21105/joss.09241 |
| Rights: |
cc_by |
| Accession Number: |
edsbas.70214C03 |
| Database: |
BASE |