OCaml - Oxidized!

HOL Light formalization of finite time blowup for Navier-Stokes

now I have become apex, multiplexor of all

another .. multiplexer

The Pat mailbox-typed programming language

💥 Dutch for tree. Lean 4 formalisation of triage tree calculus.

Compiler for the Valen programming language

The Goose Programming Language

Autolith is a self-modifiable general purpose Lisp AI agent

Contains the code for the Bedwyr model checking system

The 1SubML programming language - unified module and value language, structural subtyping, global type inference, higher rank polymorphic types, existential types, higher kinded types (no partial a…

Write the rules. Explore every outcome.

Demo for high-performance type theory elaboration

OCaml-focused, custom nix-overlays

Proof nets for MLL

Yet Another deep embedding of Linear Logic in Rocq

Isabelle server for AI agents (MCP or command-based) using PIDE.

SAT by superposition HVM benchmark

A Lévy-optimal lambda calculus reducer with a backdoor to C

Aspiring universal programming language. Features: user-definable syntax and types + self-improving optimizer that creates provably correct, hardware-optimal programs from formal specification. Boo…

Small but complete dynamic Forth Interpreter/Compiler for and in WebAssembly

A statically-typed linear functional language with graded modal types for fine-grained program reasoning

Proofs in Coq for the book Reflective Programs in Tree Calculus

types for various combinatory systems, especialy tree calculi

The Twelf Programming Language

The Candle theorem prover (fork of the HOL Light sources)