| title |
|---|
Agda |
- 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.