Links

• ​Learn you an Agda​

• ​Introductions to Agda​

• ​Category Theory in Agda - Learning exercise.

• ​Categories - Categories parametrized by morphism equality, in Agda.

• ​Programming Language Foundations in Agda (2018)​

• ​(n,r)-categories in agda​

• ​Higher-Order Pattern Unification in Agda​

• ​Experimental library for Cubical Agda​

• ​Functional Reactive Programming with Agda​

• ​Agda standard library​

• ​Introduction to Agda (2011) - Daniel Peebles' Introduction to Agda, presented at Boston Haskell.

• ​Programming with Dependent Types Summer School​

• ​Agda Prelude - Alternative to the Agda standard library that focuses more on programming and type checking time performance.

• ​Introduction to Univalent Foundations of Mathematics with Agda (2019)​

• ​Agda from Nothing - Workshop on learning Agda with minimal prerequisites.

• ​Various new theorems in constructive univalent mathematics written in Agda​

• ​gen-cart - Unifying Cartesian Cubical Set Model.

• ​Generic - Library for doing generic programming in Agda.

• ​Learn the Agda basics in three 2-hour sessions​

• ​hilbert-gentzen - Agda formalisation of IPC, IS4, ICML, and ILP.

• ​potpourri - Where everyday Agda research of G. Allais happens.

• ​categories-agda library - Standard Category Theory library for Agda.

• ​Formalize all the things in Agda (2019)​

• ​Brutal [Meta]Introduction to Dependent Types in Agda (2013)​

• ​Verified Functional Programming in Agda (2016) (HN)

• ​Brutal [Meta]Introduction to Dependent Types in Agda (2013)​

• ​System F in Agda, for fun and profit (2019)​

• ​Engineering Proof by Reflection in Agda​

• ​AgdaBench - Benchmarking tool for compile-time performance of Agda programs.