A garden of small programming language implementations 🪴

🩺 A library for compiler diagnostics

Declarative terminal graphics for OCaml

Standard ML of New Jersey

A graphical interactive proof assistant designed for education

🪆 A Staged Type Theory

Spartan implementation of H.O.T.T.

🦠 An experimental elaborator for dependent type theory using effects and handlers

A simple implementation of XTT, "A cubical language for Bishop sets"

♾️ A library for universe levels and universe polymorphism

Staged compilation with dependent types

A proof assistant and a dependently-typed language

Demo for high-performance type theory elaboration

😎TT

Minimal implementations for dependent type checking and elaboration

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

A compiler for a functional programming language including many features