This page lists some Agda libraries and other developments written in Agda. Please link to your own developments here, including supporting reports/slides/documentation. You can also create a separate wiki page describing the development.
Libraries, i.e. code which is intended to be reused
It would be nice if all libraries listed here had a free software licence.
- The "standard" library.
- Ulf Norell's Agda Prelude: an alternative to the Agda standard library (and incompatible with the same) that focuses more on programming and type checking time performance, and which is closer to Haskell's standard libraries.
- Agda Prelude: a version of the standard library with type classes and prelude.
- AoPA: Algebra of Programming in Agda.
- SYSTEM.agda makes it easy to refer to Haskell built-in types.
- Total Parser Combinators (darcs repository).
- Correct-by-Construction Pretty-Printing (darcs repository).
- Some data structures: Sorted lists, 2-3 trees, Arne Andersson trees and Left-leaning Red-Black trees, by Stevan Andjelkovic, Linus Ek, and Ola Holmström. Left-leaning Red-Black trees with deletion by Julien Oster.
- Interactive programs in Agda including simple Graphics applications.
- Towards a reflective solver for the theory of dense linear orders (darcs repository).
- agda-tactics: Library for reflective tactics, with the semiring solver as an example.
- A library to play with free theorems.
- Lemmachine: REST'ful web framework
- finite-prover: a library for proving propositions on sets with finitely-many elements, like Bool.
- DTGP: Dependently Typed Genetic Programming.
- agda-system-io: a library for streaming I/O with semantics as a lax braided monoidal category.
- agda-web-semantic: a library for processing data from the semantic web.
- agda-frp-ltl: a library for functional reactive programming, typed using linear-time temporal logic.
- The Iowa Agda Library: a concrete library focused on verified functional programming; username "guest" and password "guest" if requested.
- ooAgda: Interactive and object-oriented programming in Agda including GUIs using coinductive types.
- agdARGS: a library for hierarchical command line interfaces, by Guillaume Allais.
- agdarsec: a library of total parser combinators, by Guillaume Allais.
- Binary: a certified library for operations with binary natural numbers, suggested as an optimization-extension-replacement for the Bin part in Standard library, by Sergei Meshveliani.
- agda-real: a formalisation of the real numbers, including certified approximation by rationals and a formal topology, by Peter Bruin.
- agda-ring-solver: a fast and easy-to-use solver for ring equalities with a reflection-based interface, by Donnacha Oisín Kidney.
- cubical-algebra: a formalisation of some algebraic constructions in Cubical Agda, by Peter Bruin.
Agda code hosting
- Agda Github community, a home for Agda repositories on Github.
- Martin-Löf type theory, by Peter Dybjer.
- Sequent calculi, by Yoshiki Kinoshita.
- Implementing some functions and theorems in the book “Types and Programming Languages” by Benjamin Pierce, by David Norberg.
- Various developments related to codata and coinduction (darcs repository).
- Simple equational reasoning examples, by Stevan Andjelkovic and Ola Holmström.
- Slides about how we used Agda for logic related coursework. Code: Natural deduction, Enumerable sets and Primitive Recursive Functions, by Stevan Andjelkovic and Ola Holmström.
- Decision procedures embedded into Agda (first steps), by Karim Kanso and Anton Setzer.
- Running a classical proof with choice in Agda, by Martin Escardo and Paulo Oliva.
- A proof of Yoneda lemma (outcome of Agda Implementors Meeting XIV), by Yoshiki Kinoshita.
- Intuitionistic Ramsey Theorem, an interpretation of Ramsey's Theorem, by Thierry Coquand.
Part of joint work on termination analysis, submitted for ITP 2012, by Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt.
- A formalization of Free Groups. Theories (also a darcs repo), Accompagning blog entry.
- Constructive proofs of Higman’s lemma implemented in Agda, by Sergei Romanenko.
- A simple supercompiler formally verified in Agda, by Sergei Romanenko.
- Staged multi-result supercompilation (a model in Agda), by Sergei Romanenko.
- DoCon-A, a library for a certain initial part of computer algebra and list processing,with full proofs in Agda, by Sergei Meshveliani.
- Sqrt 2 is not rational, by Ikegami Daisuke, revised by Sergei Romanenko. (The original proof in Agda1/Alfa is due to Thierry Coquand.)
- Luau Prototyping by the Roblox PL team.
Some of the papers using Agda also come with source code.