dependent-types

A purely functional programming language with first class types

dependent types meets deep learning

Sucessor: https://github.com/thautwarm/Quick-Backend

Homotopy Type Theory proofs in Idris

Dependently typed core calculus with erasure

Port of Scala/Haskell Refined library to Idris

Velo is a tiny language (STLC + Hutton's Razor with Bools) to showcase & explore efficient verified implementations in Idris2.

Experiments in implementing functional data structures in Idris

Total Logic-Less Templating Library

Purely functional data structures in Idris

A library for static information-flow control in Idris

dependently typed Statebox (heavy WIP)

A compiler from a simple imperative language to SPIM, a dialect of MIPS assembly (WIP)

A programming-language & a proof-assistant based on *extensional* Dependent Type Theory

⚖️ A Lisp Parser in Idris

Verified directed graph rewriting with Idris

Tensor library with dependent types for compile-time guarantees

Universal chat extraction tool

Full Idris2 code used in the TyDe '24 paper "Type-level Property Based Testing"