Matthew McQuaid

language-garden. A garden of small programming language implementations 🪴

asai. 🩺 A library for compiler diagnostics

notty. Declarative terminal graphics for OCaml

smlnj. Standard ML of New Jersey

holbert. A graphical interactive proof assistant designed for education

stagedtt. 🪆 A Staged Type Theory

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

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

mugen. ♾️ A library for universe levels and universe polymorphism

staged. Staged compilation with dependent types

aya-dev. A proof assistant and a dependently-typed language

mitten_preorder. OCaml

smalltt. Demo for high-performance type theory elaboration

cooltt. 😎TT

elaboration-zoo. Minimal implementations for dependent type checking and elaboration

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

F0. A compiler for a functional programming language including many features