Idris tactics for (commutative) monoids

Univalence from scratch in Idris

OCaml backend for Idris2

A browser Pong game, taking advantage of Idris's ability to compile to javascript.

A TOML parser for Idris 2

Probabilistic music composition in Idris2

TaPL implementation bits in Idris2

Total lexer and parser for Idris2

Experiments with linear types

LightClick is a linearly typed orchestration language for Systems-on-a-Chip Designs that supports lightweight dependent types in the form of domain-specific indexed-types.

Malfunction backend for Idris 2

An implementation of "A Typed Approach to Parsing" in idris

Desc'n crunch: Descriptions, levitation, and reflecting the elaborator.

Adventures in being functional.

Data structure inspired by R's data frames.

A dependently-typed language with unboxed data.

A proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions.

A framework for Resource Dependent EDSLs in a Dependently Typed Language.

Reflecting simply-typed lambda calculus into Idris

Generic Packet Descriptions in Idris

Attempting to build type preserving lambda lifting

Declarative Hierarchical Command Line Interfaces