High-performance code intelligence MCP server. Indexes codebases into a persistent knowledge graph — average repo in milliseconds. 158 languages, sub-ms queries, 99% fewer tokens. Single static bin…

MCP server for the Rocq prover

Automated Theorem Prover inspired by Aletheia. Claude Code for mathematicians.

The Lean Computer Science Library (CSLib)

AI agents running research on single-GPU nanochat training automatically

Quantum Toolbox in Julia

My solutions to C++ Primer(5th edition) exercises.

A few Mathematics Cheat Sheets I've made on LaTeX.

The compiler and interpreter for the high-level quantum programming language Qunity, based on compositional quantum control flow.

Agda lecture notes for the Functional Programming course at TU Delft

A work-in-progress core language for Agda, in Agda

Development of homotopy type theory in Agda

Categories parametrized by morphism equality, in Agda

Clowns to the left of me, jokers to the right

A slow-paced introduction to reflection in Agda. ---Tactics!

What I wish I knew when learning HoTT

Porting of software foundations book to Agda

Papers on aspects of Generalised Algebraic Theories, Contextual Categories and Mathematical Theory Of Data

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

Minimal implementations for dependent type checking and elaboration

OTT in Agda

Quasi-quoting library for agda

Course on Metaprogramming

An Agda formalization of System F and the Brown-Palsberg self-interpreter

Categories with families in HoTT

The category theory by example book

Theory and Applications of Lenses and Optics

A digital archive of category theory papers.

multi-stage relational programming for staged relational interpreters: running with holes, faster