Logical manifestations of topological concepts, and other things, via the univalent point of view.

Claude Code skill that removes signs of AI-generated writing from text

Models of dependent type theory

Artifact and extended version of Direct Foundations for Compositional Programming

Your Personal AI super intelligence. Private, Simple and extremely powerful.

10 papers that all PhD students in programming languages ought to know, for some value of 10

Neural network learns to play snake in a terminal, built in Rust with Ratatui

A git client based on the IntelliJ platform

Minecraft AI with LLMs+Mineflayer

HoTTEST Summer School materials

📚 A collection of resources about normalization-by-evaluation

An always-running agent, but is trustworthy and secure.

Two-Level Type Theory

Agda-style equational reasoning in Haskell

OmX - Oh My codeX: Your codex is not alone. Add hooks, agent teams, HUDs, and so much more.

A collection of notes I made during OPLSS25.

Cubical Type Theory in Scala 3 — port of Mortberg's cubicaltt

Claude Code is an agentic coding tool that lives in your terminal, understands your codebase, and helps you code faster by executing routine tasks, explaining complex code, and handling git workflo…

AI-assisted Lean project automation with DAG blueprints, proof orchestration, and multi-agent coding/proving workflows.

The open source coding agent.

AI Agent Assistant & development framework that integrates lots of IM platforms, LLMs, plugins and AI feature, and can be your openclaw alternative. ✨

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Turn GitHub Copilot into OpenAI/Anthropic API compatible server. Usable with Claude Code!

Your own personal AI assistant. Any OS. Any Platform. The lobster way. 🦞

A Bowtie for a Beast (Artifact)