tiniest x86-64-linux emulator

nsync is a C library that exports various synchronization primitives, such as mutexes

Symbolic and Automatic Differentiation of Languages in Lean

An implementation of Shazam's song recognition algorithm.

The "Zen photon garden", an HTML5 raytracing art-toy.

High-performance, Reliable, and Parallel APL

A small and efficient home plant watering system.

BLAS-like Library Instantiation Software Framework

Vector class library, latest version

A Lean4 Formalization of Polynomial Functors

A Python framework for high performance GPU simulation and graphics

Specification and reference implementation for the OpenPBR Surface shading model

Tile primitives for speedy kernels

Formalization of derived categories in Lean/mathlib

A Rust/WASM implementation of homotopy.io

An attempt at formalizing facts on Euler products in Lean

Composable transformations of Python+NumPy programs: differentiate, vectorize, JIT to GPU/TPU, and more

An experimental proof assistant based on a type theory for synthetic ∞-categories.

Globular

Lecture notes on realizability

Research shading language IR

CoTracker is a model for tracking any point (pixel) on a video.

the origins of J

Stevan Apter-style trees in C++17

LLMs as Copilots for Theorem Proving in Lean

Lean4 Logic Formalization