What are the most popular libraries in the Idris ecosystem?
Number | Name | Description | Stars |
---|---|---|---|
1 | idris-lang/Idris-dev | A Dependently Typed Functional Programming Language | 2213 |
2 | mmhelloworld/idris-jvm | JVM bytecode backend for Idris | 216 |
3 | idris-hackers/software-foundations | Software Foundations in Idris | 174 |
4 | puffnfresh/iridium | xmonad with the X11 abstracted and configured with Idris | 169 |
5 | lenary/idris-erlang | Erlang Backend for Idris Compiler | 161 |
6 | ziman/lightyear | Parser combinators for Idris | 159 |
7 | idris-hackers/idris-demos | Collection of Idris tests and demonstration programs | 138 |
8 | idris-hackers/idris-koans | Koans are small lessons on the path to enlightenment. The aim of the Idris Koans project is to provide an easy learning environment in Idris. Your insight will be derived by encountering failing code and fixing them so that they type check. | 129 |
9 | timjb/quantities | Type-safe physical computations and unit conversions in Idris ⚖ 🌡 ⏲ 🔋 📐 | 117 |
10 | KesterTong/idris2048 | 2048 in Idris | 110 |
11 | edwinb/idris-php | Yes, really... | 108 |
12 | owickstrom/idris-vimscript | Compile Idris to Vimscript, like you always wanted. | 103 |
13 | idris-hackers/idris-crypto | Implementation of cryptographic primitives using Idris | 92 |
14 | bamboo/idris-cil | A Common Intermediate Language backend for Idris. | 88 |
15 | ziman/idris-py | Python backend for Idris (generates Python source, not bytecode). | 80 |
16 | edwinb/TypeDD-Samples | Sample code from "Type Driven Development with Idris" | 78 |
17 | edwinb/Blodwen | A little toy... | 62 |
18 | idris-hackers/idris-java | Java Code Generator for Idris | 62 |
19 | idris-hackers/IdrisScript | FFI Bindings to interact with the unsafe world of JavaScript | 61 |
20 | stedolan/idris-malfunction | Experimental Malfunction backend for Idris | 60 |
21 | david-christiansen/idris-type-providers | Type provider library for Idris | 59 |
22 | jfdm/idris-containers | Various data structures for use in the Idris Language. | 56 |
23 | joaomilho/awesome-idris | 𝛌 Awesome Idris resources | 55 |
24 | SimonJF/IdrisNet2 | A proper network library for Idris, now that I know what I'm doing. | 54 |
25 | fmota/HoTT-Idris | HoTT in Idris | 51 |
26 | idris-hackers/idris-llvm | Idris LLVM codegen factored out | 48 |
27 | ToJans/idris101 | Learning project by a group of people interested in learning the Idris language | 47 |
28 | mietek/idris-bash | GNU bash backend for Idris | 46 |
29 | bamboo/IdrisUnityPlayground | Experiments in Idris / Unity integration. | 45 |
30 | david-christiansen/IdrisAtGalois2015 | Slides and exercises for the Idris course taught at Galois | 44 |
31 | david-christiansen/idris-quickcheck | A port of QuickCheck to Idris | 44 |
32 | goldfirere/effects | A Haskell translation of Idris's original algebraic effects library | 39 |
33 | joom/hezarfen | a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features | 38 |
34 | edwinb/SDL-idris | SDL bindings package for idris | 36 |
35 | be5invis/idris-codegen-es | Optimized JS codegen for Idris | 34 |
36 | edwinb/States | State machines in Idris | 33 |
37 | idris-hackers/iQuery | Idris Lib to interact with the DOM and Browser API for the JavaScript backend | 32 |
38 | vmchale/recursion_schemes | Recursion schemes for Idris | 31 |
39 | david-christiansen/IdrisSqlite | Effectful bindings for SQLite (forked from IdrisWeb) | 29 |
40 | idris-lang/idris-emptycg | An empty code generator, to be used as a starting point for any new back ends. | 29 |
41 | puffnfresh/bam-idris-blog | Static blog generator in Idris. | 29 |
42 | pheymann/specdris | A test framework for Idris | 29 |
43 | stepcut/idris-blink | A simple Idris program to blink the LED on an Arduino | 28 |
44 | rbarreiro/idrisjs | Js libraries for idris | 28 |
45 | melted/idris-chez | An idris backend compiling to chez scheme | 24 |
46 | totalscript/totalscript | Explore what a powerful type system can do. | 24 |
47 | uwap/idris-http | An HTTP library for idris | 24 |
48 | japesinator/tarts | Timing attack resistant type systems | 24 |
49 | idris-hackers/idris-posix | System POSIX bindings for Idris. | 22 |
50 | idris-hackers/idris-cph-exercises | Exercises from the Idris lecture series presented at the ITU Copenhagen on March 11--15, updated to work with latest Idris releases. | 21 |
51 | edwinb/WS-idr | Yes, it is what you think it is | 21 |
52 | gergoerdi/icfp-bingo-2017-idris | ICFP Bingo 2017 (Idris edition) | 21 |
53 | bravit/idris-cs-hse | «Функциональное программирование с зависимыми типами на языке Idris» — мини-курс на ФКН ВШЭ | 21 |
54 | reynir/Verified | A collection of proofs for some idris class instances - NOT MAINTAINED | 20 |
55 | andyarvanitis/IdrisObjCExperiment | 19 | |
56 | ctford/flying-spaghetti-monster | An Idris type provider for communicating type-checkable protocols. | 19 |
57 | idris-hackers/idris-lens | 19 | |
58 | gallais/idris-tparsec | TParsec - Total Parser Combinators in Idris | 19 |
59 | QuentinDuval/IdrisReducers | Transducers for Idris: a library for composable algorithmic transformation. | 19 |
60 | vindaloo-thesis/examples | Code samples inspiring language design | 18 |
61 | BlackBrane/probability | Probabilistic computation in Idris | 17 |
62 | QuentinDuval/IdrisPipes | A library for composable and effectful production, transformation and consumption of streams of data in Idris | 17 |
63 | FranckS/RingIdris | Ring solver for Idris | 17 |
64 | sbp/idris-bi | Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq | 17 |
65 | ziman/bibdris | BibTeX database management in Idris | 17 |
66 | jfdm/idris-config | Parsers for various configuration files written in Idris. | 16 |
67 | domdere/fp-in-idris | Functional Programing in Scala (in Idris) [Idris] | 16 |
68 | google/idris-protobuf | A partial implementation of Protocol Buffers in Idris | 16 |
69 | steshaw/tdd-with-idris | Working through Type-Driven Development with Idris | 16 |
70 | ruippeixotog/quicksort | Quicksort implemented by me in different languages | 15 |
71 | david-christiansen/derive-all-the-instances | Work on type class deriving with elaboration reflection | 15 |
72 | andyarvanitis/idris-golang | 15 | |
73 | japesinator/Idris-Bifunctors | A small bifunctor library for idris | 15 |
74 | davidfstr/idris-insertion-sort | Provably correct implementation of insertion sort in Idris. | 14 |
75 | jystic/idris-vba | Visual Basic for Applications (VBA) backend for Idris | 14 |
76 | MaxOw/Idris-WebGL | WebGL bindings for Idris. | 13 |
77 | puffnfresh/stl-idris | Code from my StrangeLoop 2014 Idris presentation. | 13 |
78 | idris-hackers/idris-free | Free Monads and useful constructions to work with them | 13 |
79 | sellout/Idris-CPDT | A translation of Certified Programming with Dependent Types to Idris. | 13 |
80 | exercism/idris | Exercism exercises in Idris. | 12 |
81 | ziman/idris-benchmarks | Some benchmarks for Idris | 12 |
82 | edwinb/Eff-new | New version of Effects library with dependent states | 12 |
83 | vmchale/permutations | Provides a type-safe way of working with permutations in Idris | 12 |
84 | lambda-11235/FarRP | An arrowized FRP library for Idris with static safety guarantees. | 12 |
85 | ziman/idris-ocaml | OCaml back end for Idris | 12 |
86 | jmitchell/idris-elixir | Idris backend targeting Elixir (Work in progress) | 12 |
87 | david-christiansen/idris-code-highlighter | A semantic highlighter for Idris code | 12 |
88 | jonsterling/ETT-Playground | Experiments in Extensional & Observational Type Theory | 11 |
89 | idris-hackers/idris-bot | An IRC bot connected to an Idris REPL | 11 |
90 | Heather/Idris.Yaml | Idris YAML lib | 11 |
91 | andyarvanitis/idris-cplusplus | Experimental C++11 backend for Idris | 11 |
92 | zjhmale/idringen | a project manage tool for Idris | 11 |
93 | programminglanguagesclub/elemental-magicks | Idris + Ur/Web development of a perfect information, fair, deterministic turn based strategy game, built with dependent types! | 11 |
94 | gonzaw/extensible-records | Extensible records for Idris | 11 |
95 | trillioneyes/idris-pong | A browser Pong game, taking advantage of Idris's ability to compile to javascript. | 11 |
96 | david-christiansen/idris-utils | Various Idris utility libraries. No guarantees. Some may end up in the stdlib someday, while others may be useless. | 11 |
97 | jfdm/idris-xml | A simple XML module for Idris. | 11 |
98 | jaredloomis/Idris-HoTT | Homotopy Type Theory in Idris | 10 |
99 | sellout/Iaia | A recursion scheme library for Idris. | 10 |
100 | pbl64k/gpif-idris | Translation of Agda code in A. Löh and J. P. Magalhães Generic Programming with Indexed Functors to Idris. | 10 |
101 | SimonJF/IdrisNet | Verified networking using dependent types | 10 |
102 | ChShersh/idris-patricia | 🔮 🌋 Implementation of immutable map from integer keys to values based on patricia tree. Basically persistent array. | 10 |
103 | ziman/text | Text framework for Idris | 10 |
104 | justjoheinz/idris-httpclient | A http client for Idris based on libcurl | 10 |
105 | BlackBrane/xquant | Dependently-typed structures for quantum physics in Idris | 9 |
106 | raichoo/31C3Slides | 31C3 Slides | 9 |
107 | JakobBruenker/curses-idris | Curses bindings package for Idris | 9 |
108 | bravit/csd-utwente | Certified Software Development with Dependent Types in Idris | 9 |
109 | HuwCampbell/idris-lens | van Laarhoven lenses for Idris | 9 |
110 | bmsherman/blog | 9 | |
111 | eckart/gl-idris | 9 | |
112 | timjs/idris-clean | A priliminary backend for Idris that compiles to Clean. | 8 |
113 | mankyKitty/idris-webgl | Experimentation with Idris and WebGL via JavaScript FFI | 8 |
114 | jfdm/idris-testing | Testing Utilities for Idris programs. | 8 |
115 | raichoo/strangegroup-idris-June2014 | Code I presented in a demo at Strange Group | 8 |
116 | idris-hackers/idris-algebra | This is an attempt at painting as many bikesheds as possible with a typeclass hierarchy for idris reflecting "Algebra" | 7 |
117 | puffnfresh/idris-partiality | The partiality monad in Idris. | 7 |
118 | nicolabotta/SeqDecProbs | 7 | |
119 | eckart/SDL2-idris | SDL2 Bindings for the Idris programming language | 7 |
120 | Trundle/idris-go | A Go backend for Idris | 7 |
121 | chop-lang/chop | A rapid prototyping language inspired by Haskell, Idris, and Rust | 7 |
122 | dysinger/khartes | An Experiment with Both Haskell & Idris JS FFI interface to AWS | 7 |
123 | edwinb/ConcIO | Concurrent IO language with Uniqueness Types | 7 |
124 | rodrigogribeiro/idrisregexp | Regular expression matching in Idris | 7 |
125 | japesinator/Idris-Profunctors | A small profunctor library for idris | 7 |
126 | avsm/Idris | A language with dependent types | 7 |
127 | eraserhd/Idris-json | Formally verified JSON parser | 7 |
128 | RyanGlScott/levitation | Following along with the paper "The Practical Guide to Levitation" by Ahmad Salim Al-Sibahi | 6 |
129 | jameshaydon/idris-graphql | Idris GraphQL | 6 |
130 | mietek/idris-js | Toy JavaScript backend for Idris | 6 |
131 | superfunc/tp | Strongly Typed Paths for Idris | 6 |
132 | jmars/Records | Dependently Typed Extensible Records with Prototypal Inheritance | 6 |
133 | trillioneyes/idris-toys | An eclectic collection of beginner Idris code | 6 |
134 | GuglielmoS/sfidris | Examples and exercises of Software Foundations in Idris | 6 |
135 | tauli/idris-monadic-parser | 6 | |
136 | soimort/idris-commonmark | Idris wrapper for jgm's Markdown parser | 6 |
137 | Termina1/tlhydra | Idris parser and serializer/deserealizer for TL language | 6 |
138 | ziman/ttstar | Dependently typed core calculus with erasure | 6 |
139 | jameshaydon/smproc | A well-typed symmetric-monoidal category of concurrent processes | 6 |
140 | puffnfresh/idris-workshop | Small collection of Idris exercises | 6 |
141 | ppzzppz/Type-Driven-Development-with-Idris | 译读 Type Driven Development with Idris | 6 |
142 | A1kmm/http4idris | An experimental HTTP framework for Idris | 6 |
143 | Heather/Control.Eternal.Idris | tiny idris library | 6 |
144 | ahmadsalim/desc-n-crunch | Desc'n crunch: Descriptions, levitation, and reflecting the elaborator. | 6 |
145 | yurrriq/idris-logic | Propositional logic tools, inspired by the Coq standard library. | 5 |
146 | reynir/idris-ffi-example | A minimal example of the Idris C FFI | 5 |
147 | raichoo/IdrisCSVExample | CSV Example using Type Providers | 5 |
148 | MathiasVP/idris-regex | Verified implementation of Brzozowski derivatives in Idris | 5 |
149 | palladin/idris-snippets | Collection of Idris snippets | 5 |
150 | ostera/tap-idris | 🍻 A simple TAP producer and consumer/reporter for Idris | 5 |
151 | danilkolikov/categories | Category Theory | 5 |
152 | ziman/idris-bytes | FFI-based byte buffers for Idris | 5 |
153 | polasek/idris-scientific | Exploring the potential use of dependent types in scientific programming. | 5 |
154 | QuentinDuval/IdrisBowlingKata | A type safety challenge in Idris: encoding the rules of Bowling inside the type system | 5 |
155 | timjb/idris-pfds | Purely functional data structures in Idris | 5 |
156 | be5invis/idris-dict | A Dict k v in Idris | 5 |
157 | berewt/UnionType | UnionType in Idris | 5 |
158 | mukeshtiwari/Idris | Codes related to Idris | 5 |
159 | brainrape/idris-libuv-example | code example for using Idris with a libuv-based async C runtime | 5 |
160 | bamboo/idris-hamt | Idris Hash Array Mapped Trie | 5 |
161 | pa-ba/alacarte-idris | Data Types a la Carte in Idris | 5 |
162 | taktoa/spim-compiler | A compiler from a simple imperative language to SPIM, a dialect of MIPS assembly (WIP) | 5 |
163 | KesterTong/idris-finite-math | Math related to finite set and vectors, in Idris | 5 |
164 | cb372/idris-for-scala-devs | 5 | |
165 | avieth/ParsingWithProofs | Applicative/monadic parsing with dependent types | 4 |
166 | stallmanifold/idris-nanoparsec | A minimal and simple string based parser combinator library written in Idris. | 4 |
167 | hzelenka/idris-proofs | 4 | |
168 | eeue56/idris-hangman | Example of hangman in Idris | 4 |
169 | joom/idris-microKanren | Simple microKanren implementation in Idris. | 4 |
170 | jfdm/idris-protocol-examples | Examples of using the Idris Protocols package for stuff. | 4 |
171 | BartAdv/idris-yampa | Idris implementation of Yampa FRP library as described in Reactive Programming through Dependent Types. WIP | 4 |
172 | domdere/logic-idris | proposition combinators in [Idris] | 4 |
173 | writeoncereadmany/idris-dimensions | Dimensions library in Idris | 4 |
174 | mietek/scott-encoding | TODO | 4 |
175 | jfdm/idris-argparse | A simple argument parser written in Idris. | 4 |
176 | jdublu10/pacman | A proof that Idris is pacman complete | 4 |
177 | LightAndLight/idris-tictactoe | TicTacToe using dependent types | 4 |
178 | TimRichter/CId | a little category theory in Idris | 4 |
179 | david-christiansen/Brainfun | A Brainf**k interpreter in Idris | 4 |
180 | davidwlewis/Oz | Hardware Description Language embedded in Idris | 4 |
181 | imuli/flow | musings on programming with directed acyclic graphs. | 3 |
182 | ctford/Idris-Elba-Dev | A Whitespace-Based Dependently Typed Functional Programming Language | 3 |
183 | adelbertc/programming-in-idris | Following Idris tutorial, also playing around. | 3 |
184 | CarstenKoenig/DOS2016_IdrisWorkshop | Materialien und Infos für meinen Workshop auf dem Developer Open Space 2016 in Leipzig | 3 |
185 | eckart/cairo-idris | Idris Bindings for libcairo | 3 |
186 | clayrat/think-bayes-idris | Think Bayes in Idris | 3 |
187 | CoderPuppy/idris-depling | 3 | |
188 | runKleisli/verified-integer-gaussian-elimination | Idris package looking to define, implement, and verify naiive Gaussian elimination over the integers in some system of linear algebra. | 3 |
189 | gergoerdi/brainfuck-idris | Brainfuck interpreter in Idris | 3 |
190 | andyarvanitis/idris-generic | 3 | |
191 | eeue56/advent-of-code-2016 | 3 | |
192 | ostera/idris-coda | A collection of Idris packages | 3 |
193 | forestbelton/cooper | Presburger arithmetic solver in Idris | 3 |
194 | Heather/Synthia | pseudo package manager | 3 |
195 | domdere/validation-idris | Port of the Validation Library to Idris | 3 |
196 | BartAdv/idris-sodium | A simple Idris implementation of Sodium FRP library, following TypeScript port. WIP | 3 |
197 | Heather/idris-unicode | :let syntax [a] "→" [b] = a -> b :let syntax λ {x} . [body] = \ x => body | 3 |
198 | archaeron/idris-fiamma | Generate HTML from idris | 3 |
199 | statebox/dstbx | http://statebox.org dependently typed statebox (heavy WIP) | 3 |
200 | jdevuyst/idris-data | Experiments in implementing functional data structures in Idris | 3 |
201 | trillioneyes/dyn-universe | Fun with "Dynamic" Typing: An Introduction to Universes | 3 |
202 | tixxit/idris-curses | Idris bindings to ncurses | 3 |
203 | ezrosent/FLK-Semantics | Writing out small-step and big-step operational semantics for the FLK language in Idris | 3 |
204 | ezrosent/TAPL-idris | Examples of some TAPL examples in the idris language | 3 |
205 | danilkolikov/setoids | Idris proofs for extensional equalities | 3 |
206 | edwinb/sodium-idris | Idris bindings for libsodium | 3 |
207 | wyn/incremental | synchronous clocked dataflow in Idris - WIP | 3 |
208 | wyn/type-driven-dev | exercises from Edwin Brady book 'Type Driven Development with Idris' | 3 |
209 | aatxe/cube.idr | An implementation of the Lambda Cube in Idris. | 3 |
210 | zeitraffer/idris-cats | some category theory in Idris language | 3 |
211 | tapeinosyne/idris-microKanren | μKanren in Idris | 3 |
212 | wspk/SimpleTypes | Implementation and verification of the Simply Typed Lambda Calculus using Idris | 3 |
213 | pigworker/ConorLearnsIdris | being a scratch space for my teething troubles and tiny triumphs | 3 |
214 | idris-hackers/idris-array | primitive flat arrays containing Idris values | 3 |
215 | shlevy/lambductive | A lambda calculus with tarski universes, pi types, and self-referential expressions | 2 |
216 | ericqweinstein/wyvern | A little web server written in Idris. | 2 |
217 | JinWuZhao/idriscanvas | idris FFI binding for html5 canvas 2d api | 2 |
218 | xnning/type-driven-develop | 2 | |
219 | jwvg0425/IdrisPractice | Idris Practice | 2 |
220 | deweyvm/idris-sdl2 | 2 | |
221 | zjhmale/idris-lsp | 2 | |
222 | pierrebeaucamp/idris-dom | An Idris library to interact with the DOM | 2 |
223 | bgoodspeed/idris-strings | String (word) representations and proof for Idris | 2 |
224 | edwinb/ConcProc | Concurrent process DSL | 2 |
225 | jfdm/idris-grl | An implementation of the Goal Requirements Language in Idris. | 2 |
226 | Risto-Stevcev/idris-heyting-algebra | Interfaces for heyting algebras and verified bounded join and meet semilattices | 2 |
227 | MrChico/Smarter-contract-lang | 2 | |
228 | jaredloomis/Idris-DOM | Idris wrapper over some of the JavaScript DOM, with a FRP module included. | 2 |
229 | mmn80/idris-loader | Dynamic loading of Idris modules | 2 |
230 | yurrriq/learning-idris | Messy/old Idris notes that don't belong elsewhere. | 2 |
231 | eklavya/tomladris | TOML parser for Idris | 2 |
232 | danielwaterworth/vm-playground | Fun making virtual machines, probably won't come to much. | 2 |
233 | gallais/idris-tmustache | Total Logic-Less Templating Library | 2 |
234 | missingfaktor/tydd-with-idris-notes | Notes I jot down as I work through the book "Type-Driven Development with Idris" | 2 |
235 | walkie/GameTheory-Idris | A behavioral game theory library in Idris. | 2 |
236 | bgoodspeed/idris-benchmarks | Benchmark programs for Idris | 2 |
237 | vmchale/composition | Composition extras for Idris | 2 |
238 | jheiling/idris-electron | Electron bindings for idris | 2 |
239 | dckc/togl | a Theory of Graphs (by Meredith) | 2 |
240 | HuwCampbell/optparse-idris | Minimal port of optparse-applicative to idris | 2 |
241 | joe9/idris-to-9frontc | Translate Idris programs to 9front native C programs | 2 |
242 | rodrigogribeiro/monoid-prover | A reflective tactic for proving monoid equalities in Idris | 2 |
243 | trillioneyes/idris-canvas | Idris bindings to and abstractions over the JavaScript Canvas API | 2 |
244 | gavlegoat/simulation | An electronic circuit simulator using Idris | 2 |
245 | mcgordonite/idris-binary-rationals | An idris rational number type built from paths in the Stern Brocot tree | 2 |
246 | justjoheinz/idris-optics | 2 | |
247 | japesinator/Broadhead | Arrow-based parser combinators | 2 |
248 | ostera/asdf | 🐛 Random code snippets | 2 |
249 | QuentinDuval/IdrisExperiments | 2 | |
250 | icasperzen/ucph-msc-thesis-dpdt | Masters Thesis - Differential Privacy + Dependent Types | 2 |
251 | paulkoerbitz/idfXt | An Xmonad clone written in Idris | 2 |
252 | Heather/Bikini | Bad experiment | C++ Syntax Wrapper |
253 | HaskellDC/Meetup-Materials | 2 | |
254 | eckart/glfw-idris | GLFW bindings for Idris | 2 |
255 | yurrriq/advent-of-idris | My Idris (and Haskell) solutions to the 2016 Advent of Code. | 2 |
256 | portnov/idris-misc | 2 | |
257 | LeifW/idris-xml-simple | Simple XML ADT for Idris | 2 |
258 | trillioneyes/idris-directory | 2 | |
259 | bgoodspeed/idris-misc | Miscellaneous Idris functions/types/etc | 2 |
260 | jfdm/sif-lang | A Requirements Oriented DSL for design pattern specification. | 2 |
261 | yurrriq/the-power-of-pi | Implementations of ideas in The Power of Pi. | 2 |
262 | janschultecom/idris-refined | 2 | |
263 | sergei-romanenko/idris-samples | A collection of samples in Idris | 2 |
264 | emptyflash/ivor | The steam powered Idris package manager | 2 |
265 | esmooov/newmod | 2 |
Inspired by awesome repo rxjs-ecosystem. Thanks Nick