A modern, principled toy implementation of dependent type theory

Fast equality saturation in Haskell

Extensions to cubical for categorical logic/type theory

This repository contains companion software for the Colfax Research paper "Categorical Foundations for CuTe Layouts".

Experimental library for Narya

A tutorial on how Agda infers things

being bits and pieces I'm inclined to leave lying around

Staged compilation with dependent types

Trying to find the highest-scoring Boggle board with a mix of C++ and Python

CaDiCaL SAT Solver

A Low Barrier Proof Assistant

TeXpresso: live rendering and error reporting for LaTeX

Element Model Type Theory

OCaml - Oxidized!

Scriptable pattern editor and viewer for many families of cellular automata

A computer algebra system for research in combinatorial game theory

An experimental language exploring computation and meaning through term unification, with logic-agnostic types.

Eventually a practical 2-level TT-based compiler

Linear Types, Symmetric Monoidal Categories, and Tensors

Revamped version of Polititweet.org

Demo for dependent types + runtime code generation

A left adjointness assistant library