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