Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4

Natural language tactics to teach mathematics using Lean 4

A web browser that plays old world blues to build new world hope

The Kraken Programming Language

An experimental project to create an interactive programming language.

A course on homotopy theory and type theory, taught jointly with Jaka Smrekar

Fortran Package Manager (fpm)

Sioyek is a PDF viewer with a focus on textbooks and research papers

a small statically-linked linux system

A collection of resources for learning type theory and type theory adjacent fields.

Erlang build tool that makes it easy to compile and test Erlang applications and releases.

Typst package for drawing diagrams with arrows, built on top of CeTZ.

Share mathematics on the web with LaTeX and Markdown

The emacs knowledge graph, app for notes and structured data.

Show source files' TODOs (and FIXMEs, etc) in Magit status buffer

🦄 Modern Org Style

A scrollable-tiling Wayland compositor.

Emacs Mini-Buffer Actions Rooted in Keymaps

Arena based tree 🌲 structure by using indices instead of reference counted pointers

pix2tex: Using a ViT to convert images of equations into LaTeX code.

Execute actions based on text patterns, for Emacs

An open-source, customizable intermediate logic textbook

Project management tool for Emacs

Preview Typst code blocks in org-mode (not necessarily) buffers.

Easy self-referential struct generation for Rust.

A Testing Framework for Lean

Typst live preview minor mode for emacs

A verification toolchain for Rust programs

Interface with the rustc compiler for the purpose of program verification

Total parser combinators library for Lean4