# Agda

## 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.
- Cube solver for Cubical Agda
- agda2hs - Compiling Agda code to readable Haskell.
- Don't worry (about writing Haskell), be happy (writing Agda instead) (2022)
- Luau type checker - Partial implementation of Luau type checker in Agda for machine verification.
- Total parser combinators and parsing of mixfix operators in Agda
- ucat - Univalent categories, displayed categories, and fibrations.
- STLC-related snippets in Agda
- Agda2Dedukti - Agda proof assistant to an encoding of its logic in the lambda-pi calculus modulo rewriting, implemented in Dedukti and Lambdapi.
- Experiments with preordered set models of (directed) type theories
- Formalization of Regular Languages in Agda
- Improving Agda Interaction
- Formalization of 2LTT in Agda
- Semi-Simplicial Types in Agda
- Agda Cubical Experiments
- Komachi - Parser library in Agda, with coinductive machines and automatic differentiation.
- Flipper - Reversible programming in Agda.
- Two formalizations of Löb's Theorem
- Felix - Agda category theory library for denotational design.
- Completeness for categories of generalized automata - Bicategories of automata, completeness of F-automata in monoidal categories.
- Abstract representation of scopes in Agda
- Risotto: Architecture Mapping Proofs in Agda
- Interpreter and compiler for a procedural language (fragment of C) in Agda
- Weak 1-Categories in Agda
- stdlib-meta - Meta-programming utilities for Agda.
- Inline, type safe X86-64 assembly programming in Agda
- Multicategories in Cubical Agda
- The "Is Something" Pattern in Agda (2023) (Lobsters)