Simulator for the pioneering TX-2 computer

Sketchpad: Ivan Sutherland's pioneering drawing program

DuckDB is an analytical in-process SQL database management system

Distributed Systems Labs and Framework

Formalization of Wigderson's graph coloring algorithm in Coq

A document language for the browser

The essence of Rust.

A collection of tools for writing technical documents that mix Coq code and prose.

my phd thesis

Smart contract specification language

code accompanying a blog post about fuzzing a red-black tree implementation: http://blog.regehr.org/archives/896

Szalinski: A Tool for Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Eris distributed transactions

Adding linear types to Haskell in the style of Linear/Non-Linear (LNL) logic

Dafny is a verification-aware programming language

Jason Reed's Tiny LF, and some experiments in higher-order proof refinement logics using Jon Sterling Thought

A UCI (Universal Chess Interface) chess engine written in the Rust programming language

A basic library of algorithms and data structures (a la NJlib)

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!

Lean Theorem Prover

A LaTeX package for proof carrying papers

Convolutional Neural Networks

Harper's Modernized ALGOL in SML using multi-sorted nominal abstract binding trees

A small implementation of a proof refinement logic.

Bash script for simple generation of Coq project metadata files