On this page
Links The Power of Types in Idris (2019) Idris koans Awesome Idris linear - Profunctor optics for linear types.States - State machines in Idris.Blodwen - Prototype implementation of Idris 2.Idris 2 - Pre-alpha implementation of Idris 2, the successor to Idris.Edwin Brady - Idris 2 - Type-driven Development of Idris (2019) Software Foundations in Idris Typedefs - Programming language-agnostic, algebraic data type definition language, written in Idris.Linearity and Erasure in Idris 2 (2020) A game in a pure language (part 1): introduction and problems with Idris (2020) Linearity and Erasure in Idris 2 (2020) Collection of Idris snippets Elba - Package manager for Idris.Statebox's FSM-Oracle - Finite state machines as graphs.Idris 2: Quantitative Type Theory in Action (Web )Self-hosted Idris 2 Why is Idris 2 so much faster than Idris 1? (2020) (HN ) (Reddit )Scheme Workshop Keynote: Edwin Brady (2019) Type-Driven Development with Idris book (Updates required ) (Code )libc.idr - Bindings to the C standard library for Idris2.Edwin Brady Tells Us What's New in Idris 2 (2020) A simple Parser Combinator library in Idris (2020) Idris 2 Erlang - Erlang code generator for Idris 2. (HN )Inigo - Package manager for Idris 2 to help use and share Idris code.SPLV 2020 - Course notes and supporting code for the Scottish Programming Language and Verification summer school course on "The Implementation of Idris 2".Metaprogramming in Idris (2020) Idris, a language that will change the way you think about programming (2020) idris2-elab-util - Utilities and documentation for exploring idirs2's new elaborator reflection.idris2-sop - Idris port of Haskell's sop-core and generic-sop libraries.Session types in Idris2 Effectful Streaming For Idris Idris AOC (2020) Idrall - Dhall bindings for Idris.What Is A Package Set (2020) idris-ide-client - TypeScript library for communicating with an Idris IDE process.Interacting with Idris from Racket - Racket library for interacting with Idris over the IDE protocol.Idris Ecosystem - List of popular libraries in the Idris ecosystem.SAE (Solver of All Equations) - Idris 2 build tool and a package manager.Idris 2 Template Idris 2 LSP Idris 2 VSCode Extension Idris 2 Effect - Experimental effects library for Idris 2.Frex - Programming with equations using free extensions. (Web )Idris2-pkgs - Idris2 package repository for Nix.Idris version of Domain Modeling Made Functional Book Random proofs in Idris, Agda, and Coq Katla - LaTeX code listing generator for Idris2.ITT in Idris - Quantified dependent calculus with inference of all modalities, implemented in Idris 2.idris-data-frame - Data frames for Idris 2.Idris2GL - Graphics Library for Idris 2.TaPL implementation bits in Idris2 idris-collections - Verified data structures in Idris 2.idris2dart - Idris 2 code generator that outputs Dart code.Secrets of type driven program synthesis - Edwin Brady (2021) DepSec - Static Information-Flow Control in Idris.Idris WebAssembly CodeGen TyRE - Dependently-typed regex parser in Idris 2.idris2-eff - Extensible, stack safe effects for Idris2.Katla - LaTeX & HTML code listing generator for Idris2.Collie - Command line interface for Idris2 applications.idris2-streaming - IO streaming library for Idris2.Idris, make back end, in 15 minutes, reusable, concise sirdi - Simple package manager for Idris 2.Nix project template for Idris2 JavaScript projects idris2-nvim - Simple configuration and extra tools for NVIM + LSP + Idris2.Functional Programming in Idris 2 Idris2 TLS - Portable idris2 implementation of TLS.idris2-http - HTTP(s) client in idris.Idris2-Table - Table library for Idris 2.Skyro - Compiles programs written in Idris2 to Cairo and thereby enables high-level, pure functional programming for verifiable computation.idris2-prim - Axioms and Propositions for Primitive Types in Idris2.Yaffle - Core language and API for dependently typed languages.Tree Sitter grammar for Idris 2 Generating Idris2 code based on Dependent State Automata diagrams Idris2 Hashable - Interface for types that can be hashed.Idv - Idris Version Manager.TOML parser for Idris LightClick - Linearly typed orchestration language for Systems-on-a-Chip Designs that supports lightweight dependent types in the form of domain-specific indexed-types.tyttp - Type safe experimental web framework for Idris2 targeting nodeJS.Newtype, Generic Interface Deriving in Idris idris2-filepath - Unix style file paths in Idris2.