A verification toolchain for Rust programs

HoTT Book formalisations in Rzk.

A precise specification for "Rust lite / MIR plus"

Compiler for the Gren programming language

Scope Graph Implementation in Rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

Static recompilation of Majora's Mask (and soon Ocarina of Time) for PC (Windows/Linux)

Tool to statically recompile N64 games into native executables

Tool for RFCs

A simple demonstration of the Agda Reflection API

A monthly reading club where we read and discuss papers, books, and other writings pertaining to little languages.

Factor programming language

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses t…

Lecture notes for the lab sessions of the "Category Theory and its Applications" course 2024 @ Tallinn University of Technology

Superseded by https://github.com/circify/circ

(Cir)cuit (C)ompiler. Compiling high-level languages to circuits for SMT, zero-knowledge proofs, and more.

A Haskell library for converting LaTeX math to MathML.

Incremental bundler and build system optimized for JavaScript and TypeScript, written in Rust – including Turbopack and Turborepo.

Logic and Mechanized Reasoning

(early experiments toward) a version-control system for structured data

Using Forester, We are attempting to resurrect and grow the since deleted model theory wiki and give it a better foundation for future growth.

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

Mona Sans, a variable font from GitHub

Create string diagrams with LaTeX!

Logical Frameworks Class

Haskell's applicative functors are multi-category functors

Bidirectional Binding Signature and Bidirectional Type Synthesis, Generically

Declarative system configurations using nixOS, nix-darwin, and home-manager