idris-awesomeness

• Formally verified category theory library
• "Purely Functional Data Structures", by Chris Okasaki
• How to Keep Your Neighbours in Order PDF
• Quicksort in Idris
• Various data structures for use in the Idris Language.
• Various common utilities for use in Idris
• Implementation of 2-3 trees in Idris
• Collection of Idris tests and demonstration programs

HTTP API

• kolgut-api : Schema-safe http api using Idris+Rust

Parser Combinators

• lightyear: Parser combinators for Idris
• A simple Parser Combinator library in Idris

DevOps

• idringen : a project manage tool for Idris

Package Managers

• Inigo

Blogs/Tutorials

• Lightning Intro to Functional Programming and Dependent Types with Idris
• An Interactive Introduction to Dependent Types with Idris

Courses

• The Implementation of Idris 2

Papers

• Elaborator Reflection: Extending Idris in Idris
• Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation
• Chris Okasaki: Purely Functional Data Structures
• A tutorial implementation of a dependently typed lambda calculus
• Conor McBride: Dependently Typed Functional Programs and their Proofs
• Philip Wadler: Theorems for free!
• David Raymond Christiansen: Practical Reflection and Metaprogramming for Dependent Types
• David Raymond Christiansen: Looking Outward: When Dependent Types Meet I/O
• A Dependently Typed Library for Static Information-Flow Control in Idris - GitHub
• Dependent Types: Level Up Your Types by Marco Syfrig
• Software Foundations

---

https://eb.host.cs.st-andrews.ac.uk/writings/fi-cbc.pdf
https://github.com/idris-hackers/software-foundations
https://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf
https://eb.host.cs.st-andrews.ac.uk/drafts/dsl-idris.pdf
https://eb.host.cs.st-andrews.ac.uk/drafts/effects.pdf
https://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf
https://www.idris-lang.org/drafts/sms.pdf
https://ziman.functor.sk/