Libraries and other developments
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
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.
Some of the papers using Agda also come with source code.