On this page
Links Learn you an Agda (HN )Introductions to Agda Category Theory in Agda - Learning exercise.Categories - Categories parametrized by morphism equality, in Agda.Programming Language Foundations in Agda (Code )(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.Logical Relation for Martin-Löf Type Theory in Agda Programming with Proofs in Agda (2021) Functional Linear Algebra in Agda - Formalizing linear algebra in Agda by representing matrices as functions.agdarsec - Total Parser Combinators in Agda.Higher Categories in Agda - Experiments in Higher Category Theory in Agda.Programming with evidence - Tutorial series introducing Agda.Agda Formalization Semisimplicial types in Agda A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs (2018) (Agda Library )Tic Tac Toe, formalized in Agda Intrinsically-Typed Definitional Interpreters à la Carte ModTT in Agda Generic - Library for doing generic programming in Agda.Agda Playground Formalizing polynomials in groupoids Formalization in Agda of the Symmetry book Generic parallel algorithms in Agda Agda formalisation of second-order abstract syntax Agda CheatSheet - Basics of the dependently-typed functional language Agda.Agda Grammar for tree-sitter Agda-routing - Agda library for reasoning about asynchronous iterative algorithms and network routing problems.Formalisation of a temporal type system in Agda agda-metric-reals Categorical semantics of functional type theory with explicit substitutions, formalized in Agda generic-lr - AACMM's generic-syntax, but with QTT-style annotations.Initial Categories with Families - Formalization of categories with families (CwFs) defined as a generalized algebraic theory described in Internal Type Theory.Conceptual Mathematics - Proofs for the exercises for Lawvere and Schanuel's Conceptual Mathematics.agda-search - Search for identifiers in Agda codebases.Normalization by Evaluation, for combinators Cubes - Dependently typed type checker for a TT with intervals.OTT - Observational Type Theory as an Agda library.UALib - Agda Universal Algebra Library.Fair termination in Agda System F-omega normalization by hereditary substitution in Agda Quotient types in cubical Agda Verified (cubical) free monads Sikkel - Agda library that allows a user to program in multimode simple type theories.Axiomatic (ZF⁻-like) set theory Univalent classical mathematics in Cubical Agda Dependently typed Algorithm M and friends Experimenting on ornamentation in Agda via reflection Non-dependent and dependent lenses Meta Cedille - Minimalistic dependent type theory with syntactic metaprogramming.Fragment - Algebraic proof discovery in Agda.Theory of algebraic graphs formalized in Agda Formal verification of byzantine fault tolerant consensus in Agda Agda Synthetic Domain Theory Experiments with higher-order abstract syntax in Agda Linear.agda - Agda library for programming with separation logic, based on proof-relevant separation algebras.Review: A Very Elementary Introduction to Sheaves serre-finiteness Vehicle Formalization - Agda formalization of a core subset of the Vehicle language and a normalization procedure from the higher order language.Agda Generics - Library for datatype-generic programming in Agda.