Rust Macros for managing names and binders in abstract syntax trees

My config files

Comment and trivia parsing and formatting for Rust LALR parsers

A toy compiler for NumPy array expressions that uses e-graphs and MLIR

(triton + cuda-oxide + mlx) GPU kernels for building transformers over Clifford algebras

Code-golfing a typed System-Fω circular self-interpreter

Toy implementation of Polynomial Functors: A Mathematical Theory of Interaction

Minimal examples of crates useful for compiler development

A menagerie of cute implementations of modern typechecking algorithms

A functional language with algebraic effects, multishot continuations, and native codegen

Layout-sensitive lexer adapter for logos + lalrpop grammars

From Zero to QED: An informal introduction to formality with Lean 4

Homebrew formula for Prism

doing quantitative type theory for the lolz

README.md

Minimal observational type theory in Rust

A tiny implementation of two-level type theory

A tiny dependent type kernel and elaborator

A reference implementation of GPT-2 in Python, for teaching ML compilers

Buchberger and F4 algorithms for computing Gröbner basis for systems of multivariate polynomials

Bootstrapping Prism

Implementation of Butler-Portugal algorithm for tensor canonicalization in Rust

A minimal e-graph implementation in Rust.

Minimal implementation of generalized Clifford algebra library in Lean 4

Maranget's matrix algorithm for pattern match exhaustiveness and reachability

Generalized Clifford algebra explorer

Formal model of strategy dominance in 2-player Caverna board game

Lemmas for proving properties about Lists