A friendly little systems language with first-class types. Very WIP! 🚧 🚧 🚧

Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!

A research project in path semantics, a re-interpretation of functions for expressing mathematics

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust

Dependently-typed row-polymorphic programming language, evolved from minitt-rs

Normalization by evaluation for Martin-Löf Type Theory with dependent records

(WIP) Dependently-typed programming language with Agda style dependent pattern matching

The Hash programming language compiler ⚡

Protobufs for functional programming

🍴 | Complete and Easy implementation in Rust

🧪 | Zu Theorem Prover

An experimental typechecker with dependent types, homogeneous path types, and cubical composition

Implementation of the first-order typed lambda calculus as a CLI proof system.

the rational proof assistant

learn Type Theory in Rust

Typing Haskell in Rust

🧪 | Zure is the remake of Zu but without rigid and unstable types