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.

• ​Unification in Agda (Code)

• ​Relational Algebra in Agda​

• ​Formal Verification of Authenticated, Append-Only Skip Lists in Agda​

• ​agda-language-server - Language Server Protocol for Agda.

• ​Mechanisation of Fitch-style Intuitionistic K in Agda​

• ​Agda lecture notes for the Functional Programming course at TU Delft​

• ​Formalization of some universal algebra in Agda​

• ​Well Typed Agda Interpreter​

• ​Typing the linear pi calculus in Agda​

• ​Abstract Binding Trees in Agda​

• ​Gradual Typing in Agda - Formalizations of Gradually Typed Languages in Agda.

• ​agda-algebras - The Agda Universal Algebra Library.

• ​system-f-agda - Formalization of the polymorphic lambda calculus extended with iso-recursive types.

• ​calf - Cost-aware logical framework, embedded in Agda.