Par (⅋) is an experimental concurrent programming language. It's an attempt to bring the expressive power of linear logic into practice.

A Typst-friendly static Zettelkasten site generator.

An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax

The select-then-update surround plugin for Kakoune.

Interactive JSON filter using jq

A special-purpose processor for pure, non-strict functional languages

Rust implementation of stack graphs

Demo for dependent types + runtime code generation

Command line csv viewer

PKM for the LSP

A plain text note-taking assistant

A Language with Dependent Data and Codata Types

ldd as a tree

Submit pull requests for individual, amendable, rebaseable commits to GitHub

A very fast linker for Linux

Lean theorem proving interface which feels like pen-and-paper proofs.

An engine for displaying slips, the next-gen version of slides

A new way to see and navigate directory trees : https://dystroy.org/broot

Cut-elimination by Semantic Means

Interpreter for λ̅μμ̃-calculus of Herbelin and Curien (for educational purposes).

Large World Model -- Modeling Text and Video with Millions Context

Lean documentation authoring tool

Nix (shell) expression for working on GHC

💥 Blazing fast terminal file manager written in Rust, based on async I/O.

Making typst documents with Nix

whiteboard SDK / infinite canvas SDK

Attempt to prove semantic preservation (forward simulation) for a simple compiler.

A prototype programming language with polymorphic reachability types that track freshness, sharing and separation.