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)