Libraries and other developments

This page lists some Agda libraries and other developments written in Agda. All Agda users are strongly encouraged to add their own developments, including supporting reports/slides/documentation, to make them available to the community. 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.
• agda-frp-js: a library for functional reactive programming with a back end to JavaScript.
• 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.

Other developments

• 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.
  • Category.agda, Functor.agda, NaturalTransformation.agda, SetoidEqReasoning.agda, Setoids.agda, Yoneda.agda
• 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.