What are the most popular libraries in the Agda ecosystem?
| Number | Name | Description | Stars |
|---|---|---|---|
| 1 | agda/agda | Agda is a dependently typed programming language / interactive theorem prover. | 474 |
| 2 | liamoc/learn-you-an-agda | Learn you an Agda (and achieve enlightenment) | 288 |
| 3 | HoTT/HoTT-Agda | Development of homotopy type theory in Agda | 227 |
| 4 | agda/agda-stdlib | The Agda standard library | 161 |
| 5 | groupoid/infinity | Cubical Base Library | 155 |
| 6 | pigworker/CS410-17 | being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde | 127 |
| 7 | copumpkin/categories | Categories parametrized by morphism equality, in Agda | 106 |
| 8 | larrytheliquid/Lemmachine | REST'ful web framework in Agda | 97 |
| 9 | wenkokke/sf | Introduction to programming language theory in Agda. | 87 |
| 10 | agda/agda-frp-js | ECMAScript back end for Functional Reactive Programming in Agda | 72 |
| 11 | jstolarek/why-dependent-types-matter | Companion code for "Why Dependent Types Matter" paper. | 61 |
| 12 | pigworker/CS410-14 | being the materials for CS410 Advanced Functional Programming in the 2014-15 session | 55 |
| 13 | UlfNorell/agda-prelude | Programming library for Agda | 54 |
| 14 | dlicata335/hott-agda | 54 | |
| 15 | UlfNorell/agda-summer-school | Summer school on programming in Agda | 51 |
| 16 | scott-fleischman/agda-from-nothing | A workshop on learning Agda with minimal prerequisites. | 41 |
| 17 | scmu/foundations-harper | Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages. | 41 |
| 18 | pigworker/CS410-15 | being the materials for CS410 Advanced Functional Programming in the 2015/16 session | 40 |
| 19 | spire/spire | The Spire Programming Language | 40 |
| 20 | pedagand/typechecker-evolution | The Evolution of a Typechecker | 38 |
| 21 | jyp/nano-Agda | Tiny type-checker with dependent types | 37 |
| 22 | scott-fleischman/greek-grammar | Modeling Ancient Greek Grammar | 34 |
| 23 | Saizan/miller | Miller/pattern unification in Agda | 33 |
| 24 | agda/agda-ocaml | OCaml backend for Agda | 32 |
| 25 | Saizan/cubical-demo | 32 | |
| 26 | agda/agda-frp-ltl | An implementation of Functional Reactive Programming | 32 |
| 27 | effectfully/OTT | Observational Type Theory as an Agda library | 32 |
| 28 | sstucki/system-f-agda | A formalization of the polymorphic lambda calculus extended with iso-recursive types | 31 |
| 29 | wouter-swierstra/Brainfuck | A Brainfuck interpreter written in Agda | 29 |
| 30 | siddharthist/CoverTranslator | A tool for formally verifying Haskell code in Agda | 29 |
| 31 | rodrigogribeiro/agda-software-foundations | Porting of software foundations book to Agda | 28 |
| 32 | algebraic-graphs/agda | The theory of algebraic graphs formalised in Agda | 27 |
| 33 | pigworker/CS410-13 | being the notes and materials for CS410 in the 2013/14 academic session | 26 |
| 34 | pigworker/Pivotal | 25 | |
| 35 | scmu/aopa | Algebra of Programming in Agda: Dependent Types for Relational Program Derivation | 25 |
| 36 | felixwellen/DCHoTT-Agda | Differential cohesion in Homotopy Type Theory by an axiomatized infinitesimal shape modality | 25 |
| 37 | pcapriotti/agda-base | Base library for HoTT in Agda | 23 |
| 38 | konn/equational-reasoning-in-haskell | Agda-style equational reasoning in Haskell | 23 |
| 39 | pigworker/Bi71 | being a bidirectional reformulation of Martin-Löf's 1971 type theory | 23 |
| 40 | wenkokke/AutoInAgda | Proof automation – for Agda, in Agda. | 22 |
| 41 | gallais/generic-syntax | A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs | 22 |
| 42 | gallais/agdarsec | Total Parser Combinators in Agda | 21 |
| 43 | agda/agda-system-io | Bindings to Haskell's IO monad which respect Agda's semantics | 21 |
| 44 | ZongzheYuan/HaltingProblem | The proof of undecidability of halting problem, using the model -- WHILE language. | 21 |
| 45 | pigworker/Samizdat | being bits and pieces I'm inclined to leave lying around | 20 |
| 46 | favonia/homotopy | My old Agda code for Homotopy Type Theory. (Halted. See HoTT/HoTT-Agda for the new one.) | 20 |
| 47 | gallais/potpourri | Where my everyday research happens | 20 |
| 48 | sergei-romanenko/agda-simple-scp | A simple supercompiler formally verified in Agda | 19 |
| 49 | UlfNorell/x86-agda | Inline, type safe X86-64 assembly programming in Agda | 19 |
| 50 | wenkokke/SubstructuralLogicsInAgda | Implementation of several substructural logics in Agda. | 18 |
| 51 | bobatkey/sorting-types | Typed DSLs for sorting | 18 |
| 52 | mietek/hilbert-gentzen | Agda formalisation of IPC, IS4, ICML, and ILP | 18 |
| 53 | pigworker/EGTBS | being the introduction to co-de-Bruijn metasyntax | 17 |
| 54 | pcapriotti/agda-categories | Category theory and algebra | 17 |
| 55 | mietek/formal-logic | Formalisation of some logical systems | 17 |
| 56 | InitialTypes/Club | Organization and planning for the Initial Types Club | 17 |
| 57 | gallais/aGdaREP | Implementing grep in Agda | 17 |
| 58 | ezyang/lr-agda | Logical relations proof in Agda | 17 |
| 59 | pigworker/Totality | being the programs and code for a paper about general recursion | 15 |
| 60 | mr-ohman/logrel-mltt | A Logical Relation for Martin-Löf Type Theory in Agda | 15 |
| 61 | martinescardo/TypeTopology | Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view. | 15 |
| 62 | jmchapman/Relative-Monads | Relative Monad Library for Agda | 15 |
| 63 | freebroccolo/agda-prelude | A simple prelude for Agda | 15 |
| 64 | CodaFi/Agda-Metaprogramming | Dependently Typed Metaprogramming Exercises | 14 |
| 65 | ericfinster/opetopes-in-agda | Formalization of Opetopes and Opetopic Sets in Agda | 14 |
| 66 | dlicata335/cart-cube | Cartesian Cubical Type Theory | 14 |
| 67 | AndrasKovacs/system-f-omega | System F-omega normalization by hereditary substitution in Agda | 14 |
| 68 | jonsterling/agda-zipper-machine | An abstract machine using indexed containers and their zippers | 14 |
| 69 | dorchard/effects-as-sessions | Formalised embedding of an imperative language with effect system into session-typed pi calculus. | 14 |
| 70 | HoTT/M-types | A formalization of M-types in Agda | 14 |
| 71 | pigworker/SSGEP-DataData | being the materials for "Datatypes of Datatypes" at the Summer School on Generic and Effectful Programming, Oxford | 13 |
| 72 | effectfully/STLC | Dependently typed Algorithm M and friends | 13 |
| 73 | fredefox/cat | A formalization of category theory in cubical Agda | 13 |
| 74 | siddharthist/write-yourself-a-scheme-in-agda | Like "Write Yourself a Scheme in 48 Hours", but in Agda | 13 |
| 75 | yoricksijsling/ornaments-thesis | My master thesis about generic programming and ornaments | 13 |
| 76 | gergoerdi/universe-of-syntax | A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need. | 12 |
| 77 | gallais/type-scope-semantics | A self-contained repository for the paper Type and Scope Preserving Semantics | 12 |
| 78 | gallais/typing-with-leftovers | Self-contained repository for the eponymous paper | 12 |
| 79 | agda/ooAgda | Interactive and object-oriented programming in Agda using coinductive types | 12 |
| 80 | JacquesCarette/pi-dual | Collaborative work on reversible computing | 12 |
| 81 | VictorCMiraldo/agda-rw | This is the place where (more or less) stable releases of my RW library will be published. | 11 |
| 82 | effectfully/Eff | Experiments with effect systems | 11 |
| 83 | inc-lc/ilc-agda | Machine-checked Agda formalization for the ILC project | 11 |
| 84 | jmchapman/Big-step-Normalisation | Agda formalisations of some big-step normalization proofs | 11 |
| 85 | bitonic/hakyll-agda | Hakyll support for Agda literate files | 11 |
| 86 | plum-umd/cgc | Constructive Galois connections | 11 |
| 87 | hazelgrove/agda-popl17 | Mechanization of Hazelnut, as submitted to POPL 2017 | 11 |
| 88 | pigworker/CS410-16 | being the lecture materials and exercises for the 2016/17 session of Advanced Functional Programming at Strathclyde | 11 |
| 89 | pigworker/Ohrid-Agda | being my notes and exercises for the Types Summer School in Ohrid, (FYRO) Macedonia, July 2017 | 10 |
| 90 | effectfully/Cubes | A dependently typed type checker for a TT with intervals. | 10 |
| 91 | mietek/imla2017 | Agda formalisation of NbE for λ□ | 10 |
| 92 | jonsterling/constructive-sheaf-semantics | I'm putting Palmgren's Constructive Sheaf Semantics into Agda. Defines sheaves via Grothendieck pretopologies. | 10 |
| 93 | sebastiaanvisser/ghc-goals | Collect type information about Agda like goals in Haskell code. | 10 |
| 94 | scott-fleischman/agda-from-nothing-2017 | Agda from Nothing: Order in the Types | 10 |
| 95 | dysinger/agda-haskell-c-ffi-layer-cake | Demostration of FFI from Agda -> Haskell -> C in one project | 10 |
| 96 | sto0pkid/CategoryTheory | Category Theory in Agda | 10 |
| 97 | freebroccolo/agda-cubical-sets | Cubical Set(oid)s in Agda | 10 |
| 98 | jespercockx/cubes | An implementation of (some fragment of) cubical type theory using rewrite rules, based on a talk given by Conor McBride at the 23rd Agda's Implementor's Meeting. | 10 |
| 99 | jonsterling/agda-brouwerian-mathematics | some "modernized" brouwerian mathematics, inspired by Hancock, Ghani & Pattinson | 9 |
| 100 | crypto-agda/agda-nplib | Proposed extensions to Agda standard's library | 9 |
| 101 | pigworker/LibAgda | 9 | |
| 102 | ahmadsalim/well-typed-agda-interpreter | A well typed interpreter for the simply-typed lambda calculus written in Agda | 9 |
| 103 | williamdemeo/ial | Iowa Agda Library | 9 |
| 104 | bitonic/ny-haskell-agda | Code and slides form my talk at NY Haskell | 8 |
| 105 | gallais/agda-presburger | Deciding Presburger arithmetic in agda | 8 |
| 106 | jesyspa/master-thesis | 8 | |
| 107 | gergoerdi/syntactic-stlc | Syntactic evaluation of STLC (incl. proof of normalization a la Software Foundations) | 8 |
| 108 | effectfully/Generic | A library for doing generic programming in Agda | 8 |
| 109 | DSLsofMath/FLABloM | Functional Linear Algebra with Block Matrices | 8 |
| 110 | kdxu/InferAgda | 8 | |
| 111 | taktoa/wasm-agda | A typechecker for WebAssembly, written in Agda (WIP) | 8 |
| 112 | robsimmons/agda-lib | A standard library for Agda | 8 |
| 113 | quchen/agda-learning | Stuff I’m writing to learn Agda. | 8 |
| 114 | Blaisorblade/Agda-playground | My Agda experiments | 7 |
| 115 | bch29/agda-holes | Agda programming with holes | 7 |
| 116 | wjzz/agda-DTP-examples | 7 | |
| 117 | IanOrton/cubical-topos-experiments | Agda code for experimenting with internal models of cubical type theory | 7 |
| 118 | heades/cut-fill-agda | Agda sources used in my paper with Valeria de Paiva | 7 |
| 119 | bitonic/agdastuff | Assorted Agda code. | 7 |
| 120 | mietek/agda-introduction | Mirror of Conor McBride’s Agda course materials (January 2011) | 7 |
| 121 | gallais/agdARGS | Dealing with Flags and Options | 7 |
| 122 | sergei-romanenko/staged-mrsc-agda | Staged multi-result supercompilation (a model in Agda) | 7 |
| 123 | mietek/haskell-exchange-2015 | Materials for my Haskell eXchange 2015 talk | 7 |
| 124 | jonsterling/agda-abt | Abstract binding trees in Agda | 7 |
| 125 | freebroccolo/nbe | Normalization by evaluation in Agda | 7 |
| 126 | jonsterling/agda-effectful-forcing | Constructive and formal proof of Brouwer's Bar Theorem & Monotone Bar Induction Principle for System T-definable functionals. | 7 |
| 127 | YouyouCong/type-preserving-cps | Type-preserving CPS translation for simply- and dependently-typed lambda calculi | 7 |
| 128 | agda/agda-finite-prover | Library for proving propositions quantified over finite sets | 7 |
| 129 | effectfully/random-stuff | 7 | |
| 130 | sstucki/pts-agda | A formalization of Pure Type Systems (PTS) in Agda | 6 |
| 131 | myuon/agda-cate | Category Theory in Agda | 6 |
| 132 | effectfully/Beauty-and-the-Beast | A toy supercompiler for STLC with numbers and lists | 6 |
| 133 | AndrasKovacs/stlc-nbe | Correctness of normalization-by-evaluation for STLC | 6 |
| 134 | IanOrton/decomposing-univalence | Agda code to accompany the paper "Decomposing the Univalence Axiom" | 6 |
| 135 | freebroccolo/agda-grothendieck-yoga | Grothendieck's Yoga of Six Operations | 6 |
| 136 | nfjinjing/chu2 | Chu2 Agda Web Server Interface | 6 |
| 137 | joom/regexp-agda | 6 | |
| 138 | UlfNorell/category-theory-experiments | 6 | |
| 139 | msullivan/godels-t | Formalization of a bunch of properties of Godel's System T in agda | 6 |
| 140 | sergei-romanenko/agda-samples | A collection of samples in Agda | 6 |
| 141 | scott-fleischman/agda-travis | Example repo for building Agda files with Travis CI | 6 |
| 142 | konn/sdg-agda | Synthetic Differential Geometry in Agda | 6 |
| 143 | copumpkin/bitvector | Sequences of bits and common operations on them | 6 |
| 144 | vikraman/2DTypes | 6 | |
| 145 | gergoerdi/generic-syntax | Library implementation of "Generic description of well-scoped, well-typed syntaxes" | 6 |
| 146 | lives-group/time-complexity-verification | Formal verification of time complexity of some algorithms in Agda | 6 |
| 147 | josh-hs-ko/Thesis | Analysis and synthesis of inductive families | 6 |
| 148 | notogawa/sfja-agda | "Software Foundations" Agda challenge | 6 |
| 149 | SuprDewd/agda-translation-method | An Agda library for turning equations into bijections using the translation method | 5 |
| 150 | sergei-romanenko/agda-miscellanea | Experiments with Agda | 5 |
| 151 | Fuuzetsu/yi-agda | Agda mode for Yi | 5 |
| 152 | larrytheliquid/uAgda | [UNOFFICIAL FORK] Making uAgda work with ghc 7.4.1 | 5 |
| 153 | jonsterling/Agda-Sheaves | Sheaves in Agda (will be superseded by https://github.com/jonsterling/constructive-sheaf-semantics which has sheaves on a site) | 5 |
| 154 | asr/fotc | Agda formalisation of FOTC (First-Order Theory of Combinators). | 5 |
| 155 | GuillermoCalderon/ProjectiveGeometryInAgda | A formalization of Constructive Projective Geometry in Agda | 5 |
| 156 | jpvillaisaza/abel | Category theory applied to functional programming | 5 |
| 157 | gergoerdi/system-f-agda | System F | 5 |
| 158 | freebroccolo/agda-lambda-maps | 5 | |
| 159 | jonsterling/agda-bar-induction | 5 | |
| 160 | Saizan/parametric-demo | 5 | |
| 161 | joom/modal | Compilation of modal logic based functional language ML5 to JavaScript. | 5 |
| 162 | paulcc/ruby-refactoring | This is RASH (Ruby AnalysiS in Haskell) -- it's going to be all over your code! I aim to get it to do various static analyses, type checking, and refactoring on Ruby. It is being morphed from https://github.com/paulcc/minijava-compiler. Contributions welcome! I'm also very happy to explain things if people ask. (NOTE: I'd rather write this in Agda, but one step at a time...) | 5 |
| 163 | Fuuzetsu/agdoparsec | Agda implementation of what aims to model the behaviour of Haskell's Attoparsec library. | 5 |
| 164 | mietek/coquand | TODO | 5 |
| 165 | acalles1/setform | Set Theory Formalization in Agda | 5 |
| 166 | cartazio/system-lf | linear logic and system f have a baby | 5 |
| 167 | dima-starosud/Dynamic | 5 | |
| 168 | ernius/mergesort | Merge sort correctness proof | 5 |
| 169 | mietek/abel-chapman-extended | Extension of Abel-Chapman 2014 with products and coproducts | 5 |
| 170 | gallais/agda-sizedIO | IO using sized types and copatterns | 5 |
| 171 | jmchapman/restriction-categories | A formalisation of Restriction Categories in Agda | 5 |
| 172 | freebroccolo/agda-groupoids | Groupoids in Agda | 5 |
| 173 | wenkokke/FirstOrderUnificationInAgda | Implementation of McBride's "First-order unification by structural recursion" in Agda. | 5 |
| 174 | kino3/PiMLTT | Formalization of "Programming in Martin-Löf's Type Theory". | 5 |
| 175 | ice1000/Theorems | 🌐 Theorems that rule this multiverse | 5 |
| 176 | jonaprieto/agda-prop | A Library for Classical Propositional Logic in Agda | 4 |
| 177 | mchakravarty/accelerate-agda | Accelerate in Agda | 4 |
| 178 | mrkgnao/utt | The core type theory from the first chapter of Ulf Norell's (Agda) thesis | 4 |
| 179 | mr-ohman/intuitionistic-normalization | Implementation of Intuitionistic Model Constructions and Normalization Proofs in Agda | 4 |
| 180 | freebroccolo/agda-syntactic-duploids | An encoding of syntactic duploids | 4 |
| 181 | MatthewDaggitt/agda-routing | An Agda library for reasoning about network routing problems | 4 |
| 182 | freebroccolo/substitutions | Experiments with explicit substitutions and abstract machines | 4 |
| 183 | guillaumebrunerie/JamesConstruction | Formalization of the James construction in Agda | 4 |
| 184 | guillaumebrunerie/SmashProduct | An Agda proof of the fact that the smash product is a 1-coherent monoidal product (in progress) | 4 |
| 185 | UlfNorell/aim23-talk | 4 | |
| 186 | freebroccolo/agda-cube-category | 4 | |
| 187 | freebroccolo/agda-continuous-functions | 4 | |
| 188 | jbracker/polymonad-proofs | Agda proofs about polymonads | 4 |
| 189 | freebroccolo/algebraic-induction-recursion | 4 | |
| 190 | mathijsb/generic-in-agda | 4 | |
| 191 | mcmtroffaes/agda-proofs | 4 | |
| 192 | andreasabel/continuous-normalization | Evaluation of typed terms in Agda using the Delay monad. | 4 |
| 193 | freebroccolo/agda-ionads | 4 | |
| 194 | freebroccolo/agda-free-lambda-theories | 4 | |
| 195 | freebroccolo/agda-categories-with-families | 4 | |
| 196 | freebroccolo/container-calculus | Experiments with containers and λ-calculi | 4 |
| 197 | smfactor/UnitsAsTypes | Final Project for COMP360-1 Wesleyan University | 4 |
| 198 | freebroccolo/agda-geometric-sets | 4 | |
| 199 | AndrasKovacs/misc-stuff | Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell. | 4 |
| 200 | notogawa/agda-practical | for use agda as programming language | 4 |
| 201 | liamoc/agda-snippets | Library and tool to render the snippets in literate Agda files to hyperlinked HTML, leaving the rest of the text untouched. | 4 |
| 202 | hazelgrove/agda-tfp16 | Formalization of joint work submitted to TFP2016 (deprecated, see agda-popl17) | 3 |
| 203 | mietek/alt-artemov | WIP | 3 |
| 204 | agda/agda-web-uri | Simple bindings for parsing, processing and serializing URIs | 3 |
| 205 | larrytheliquid/agda-rb | 3 | |
| 206 | mietek/nbe-correctness | TODO | 3 |
| 207 | krtx/agda-handson | agda handson | 3 |
| 208 | L-TChen/PCF-Nominal | for FLOLAC'14 | 3 |
| 209 | freebroccolo/agda-signatures | 3 | |
| 210 | freebroccolo/agda-semigroupoids | 3 | |
| 211 | marco-vassena/gdiff3 | A data type generic diff3 algorithm | 3 |
| 212 | crypto-agda/explore | Big operators as exploration functions in Agda | 3 |
| 213 | larrytheliquid/plclub-expless | PL Club talk on Expressionless Weak-Head Normal Forms | 3 |
| 214 | patrikja/SeqDecProb_Agda | 3 | |
| 215 | umazalakain/fyp | My final year project at the University of Strathclyde | 3 |
| 216 | sergei-romanenko/chapman-big-step-normalization | Big-step normalization (formalized in Agda) | 3 |
| 217 | JLimperg/cats | Category Theory in Agda. Learning exercise, not for public consumption. | 3 |
| 218 | gallais/proof-search-ILLWiL | A self-contained repo for the ILLWiL paper | 3 |
| 219 | GallagherCommaJack/tt-provability | Systems for doing provability logic in type theory | 3 |
| 220 | freebroccolo/agda-groupoids-cosmoi | 3 | |
| 221 | scott-fleischman/agda-in-10-minutes | A 10-minute introduction to Agda | 3 |
| 222 | wouter-swierstra/TPT-2014 | Theory of Programming and Types, academic year 2014-2015 | 3 |
| 223 | effectfully/Big-Step-Normalization | 3 | |
| 224 | freebroccolo/sequent-calculus | 3 | |
| 225 | freebroccolo/agda-wander-magmas | A familial coinductive-recursive encoding of Penon-style ∞-magmas | 3 |
| 226 | effectfully/Ouroboros | 3 | |
| 227 | effectfully/Categories | Some basic category theory | 3 |
| 228 | juanbono/verified-fp-agda | Functional Verified Programming in Agda - Exercises | 3 |
| 229 | bgbianchi/sorting | Formalization of some sorting algorithms in Agda | 3 |
| 230 | andreasabel/ipl | Agda formalization of Intuitionistic Propositional Logic | 3 |
| 231 | AndrasKovacs/pny1-assignment | College assignment writing in which I ramble about type classes and dependent types. | 3 |
| 232 | freebroccolo/agda-kan-semisimplicial-setoids | 3 | |
| 233 | effectfully/blog | 3 | |
| 234 | hendrikmaarand/lambda-calculus | Formalisation of normalisation by evaluation for simply typed lambda calculus extended with natural numbers, lists, pairs, and streams. | 3 |
| 235 | UlfNorell/agda-cufp | CUFP tutorial 2014 | 3 |
| 236 | freebroccolo/agda-nerve | 3 | |
| 237 | jmchapman/categories | A category theory library for Agda | 3 |
| 238 | mcmtroffaes/AgdaTutorial | Git fork of http://hub.darcs.net/divip/AgdaTutorial | 3 |
| 239 | arianvp/types-and-statemachines | Research project about types and state machines, and their applications in HTTP | 3 |
| 240 | jornvanwijk/monotoneframeworks-agda | Implementation of monotone frameworks in Agda | 3 |
| 241 | ernius/formalmetatheory-nominal | Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory | 3 |
| 242 | sergei-romanenko/agda-Ramsey-theorem | Intuitionistic Ramsey theorem (a proof in Agda) | 3 |
| 243 | ernius/formalmetatheory-stoughton | We develop metatheory of the Lambda calculus in Constructive Type Theory, which is made possible by the use of an appropriate notion of substitution, due to A. Stoughton. | 3 |
| 244 | effectfully/ECC | A shallow embedding of Luo's ECC into Agda. | 3 |
| 245 | joaopizani/piware-agda | This repository has moved to https://gitlab.com/joaopizani/piware-agda | 3 |
| 246 | np/guarded-recursion | Guarded recursion in Agda | 3 |
| 247 | freebroccolo/computads | 3 | |
| 248 | np/NomPa | 3 | |
| 249 | freebroccolo/agda-groupoids-fibred | 3 | |
| 250 | thobaa/Algebra-of-Parallel-Programming-in-Agda | 3 | |
| 251 | ichistmeinname/DTDatastructures | Reimplementations of functional data structures (mostly as presented by Okasaki) in a dependently typed language | 3 |
| 252 | zaklogician/linear-constructive | Linear Logic for Constructive Mathematics, in Agda | 3 |
| 253 | sheganinans/Static-Dimensions | A statically typed dimensional analysis calculator written in Agda. | 3 |
| 254 | ayberkt/system-t-normalization | Normlization proof of System T in Agda. | 3 |
| 255 | jonsterling/agda-sheaf-semantics | here we go again | 3 |
| 256 | crypto-agda/protocols | Shallow embedding of Protocols using Agda dependent types | 3 |
| 257 | jonsterling/reflection-by-erasure | Reflection by Erasure, a neat trick to characterize terms as "sufficiently marked up realizers" in an intensional type theory, i.e. a theory of formal proof | 3 |
| 258 | ak3n/jolie-agda | Verified type checker for Jolie (http://jolie-lang.org) | 2 |
| 259 | BitFunctor/bitfunctor | Decentralized blockchain-based storage of the automatically-verifiably correct (certified) code as well as generalized blockchain platform | 2 |
| 260 | agda/agda-uhc | UHC backend for Agda | 2 |
| 261 | anasazi/patina-proof | Proofs about Patina, the Rust formalization | 2 |
| 262 | EdwardMorehouse/hott_groupoids | homotopy type theory in agda using path elimination and groupoids | 2 |
| 263 | freebroccolo/agda-polynomials | 2 | |
| 264 | JacquesCarette/TheoriesAndDataStructures | Showing how some simple mathematical theories naturally give rise to some common data-structures | 2 |
| 265 | freebroccolo/agda-globular-objects | 2 | |
| 266 | psygnisfive/TTInAgda | An implementation of the STLC in Agda, with raw terms, typing proofs, and indexed terms | 2 |
| 267 | VictorCMiraldo/msc-agda-tactics | A Repo for managing my Master's thesis files. | 2 |
| 268 | pcapriotti/hott-exercises | Solutions of the exercises of the HoTT book | 2 |
| 269 | freebroccolo/agda-cosmoi | 2 | |
| 270 | scott-fleischman/agda-digit | Ideas for digit encodings in Agda | 2 |
| 271 | piyush-kurur/sample-code | This repository contains a collection of sample programms in various languages mainly to serve as illustrations | 2 |
| 272 | UlfNorell/agda-tactics | 2 | |
| 273 | rolyp/proof-relevant-pi | 2 | |
| 274 | gallais/agda-pretty-notgreedy | Port of Bernardy's Functional Pearl: A Pretty But Not Greedy Printer | 2 |
| 275 | glangmead/hott_cmu80818 | Companion code to CMU course on Homotopy Type Theory | 2 |
| 276 | scott-fleischman/exercises-vfpa | Exercises from Verified Functional Programming in Agda by Aaron Stump | 2 |
| 277 | hbasold/CoindDepTypes | 2 | |
| 278 | williamdemeo/agda-fresh | basics | 2 |
| 279 | andrejtokarcik/agda-semantics | An executable formal semantics of Agda in K | 2 |
| 280 | canndrew/malk-agda | Attempt at a formalised implementation of a dependent type theory | 2 |
| 281 | freebroccolo/agda-semigroupoids-old | 2 | |
| 282 | zmthy/recursive-types | An Agda encoding of a language with recursive types. | 2 |
| 283 | metaborg/mj.agda | https://metaborg.github.io/mj.agda/ | 2 |
| 284 | mckeankylej/avl | 2 | |
| 285 | ssomayyajula/cubism | Excursions in cubical type theory | 2 |
| 286 | sabauma/agda-relation-algebra | Relational algebra implementation in Agda with simple bindings to SQLITE | 2 |
| 287 | jonsterling/agda-cubical-sets | 2 | |
| 288 | scmu/mds | Code and Proofs Related to the Paper "Functional Pearl: Finding a Densest Segment" | 2 |
| 289 | rodrigogribeiro/generic | Being a place where rodrigogribeiro study generic programming based on universes on dependently typed languages | 2 |
| 290 | mckeankylej/hmap | 2 | |
| 291 | heades/Agda-LLS | An Implementation of Various Linear Logics in Agda | 2 |
| 292 | DSLsofMath/ValiantAgda | Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda | 2 |
| 293 | sborrazas/agda-tutorial | My solutions for the Agda tutorial http://people.inf.elte.hu/divip/AgdaTutorial/Index.html | 2 |
| 294 | nachivpn/cat | Category theory proofs in Agda | 2 |
| 295 | ssomayyajula/HoTT | Project on homotopy type theory @ Indiana University | 2 |
| 296 | serendependy/J-in-Agda | Sketch of J arrays and function rank in Agda | 2 |
| 297 | doofin/hott-examples | examples in Homotopy type theory | 2 |
| 298 | freebroccolo/agda-computads | 2 | |
| 299 | jozefg/regex | an exercise in decision procedures in Agda | 2 |
| 300 | fferreira/NbE | Exploring Normalization by Evaluation | 2 |
| 301 | zmthy/automating-gradual-typing | Define your language under an abstracted functor and get different type systems as a result: an Agda exercise | 2 |
| 302 | glguy/ord | An exploration of a variant of ordinals in Agda | 2 |
| 303 | jonsterling/agda-nominal-sets | 2 | |
| 304 | zaklogician/monads-are-not | Monads are not just monoids in the category of endofunctors. | 2 |
| 305 | freebroccolo/rules-as-polynomials | Rules as Polynomials | 2 |
| 306 | freebroccolo/agda-operads | 2 | |
| 307 | freebroccolo/agda-codes | Notes and experiments in Agda related to sets, codes, numerics, etc. | 2 |
| 308 | JonFowler/theoryofreach | Agda accompaniment for the paper theory of reach | 2 |
| 309 | shayan-najd/Embedding-By-Normalisation | Supporting Material for the paper "Embedding-By-Normalisation" | 2 |
| 310 | jonsterling/choice-sequences | 2 | |
| 311 | pigworker/EWSCS14 | being the lecture material and exercises for the Estonian Winter School | 2 |
| 312 | pedagand/agda-datalib | Datatype-generic programming library in/for Agda | 2 |
| 313 | hazelgrove/hazelnut-dynamics-agda | mechanization paired with https://github.com/hazelgrove/hazelnut-dynamics | 2 |
| 314 | freebroccolo/agda-syntactic-groupoids | 2 | |
| 315 | mietek/constructive-provability-logic | Mirror of Rob Simmons’ CPL system | 2 |
| 316 | freebroccolo/agda-plots | Tringali's Plots in Agda | 2 |
| 317 | sstucki/f-omega-int-agda | F-omega with interval kinds mechanized in Agda | 2 |
| 318 | freebroccolo/agda-groupoids-enriched | 2 | |
| 319 | AndrasKovacs/SemanticsWithApplications | Formal semantics in Agda. | 2 |
| 320 | heades/law | The Lawvere Categorical Logic Library | 2 |
| 321 | jonsterling/Diaconescu-TT | An Agda proof of Diaconescu's Theorem for Constructive Type Theory using Setoids | 2 |
| 322 | larrytheliquid/thesis | 2 | |
| 323 | pigworker/MGS14 | being the lecture code and exercises for Dependently Typed Programming at Midlands Graduate School 2014, in Nottingham | 2 |
Inspired by awesome repo rxjs-ecosystem. Thanks Nick