Proposed extensions to Agda standard's library
Cryptographic Constructions in the Type Theory of Agda
Big operators as exploration functions in Agda
Shallow embedding of Protocols using Agda dependent types
Core bindings to run Agda code using NodeJS
Agda binding to bitcoinjs
The Agda standard library
Agda is a dependently typed programming language / interactive theorem prover.
Reflective proof tactics and metaprogramming for Agda.