The Twelf Programming Language

SML# compiler

A formalisation of Cartesian Frames, a perspective on embedded agency, in the HOL theorem prover.

Standard ML of New Jersey

Paper Tape is All You Need

Terminal-based but modern tetromino-stacking game that is customizable and cross-platform.

AI agents running research on single-GPU nanochat training automatically

Nyxt - the hacker's browser.

Vazirmatn is a Persian/Arabic font. وزیرمتن یک فونت فارسی/عربی است

The HOL Light theorem prover

A simple, rational music player for android

An automatic theorem prover for first order logic with equality

Checkpoint/Restore tool

get things from one computer to another, safely

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

Binary analysis in HOL

P4 formalization using Ott and HOL4

Interactive quizzes for Markdown

An introduction to programming language theory in Agda

A free Windows-compatible Operating System

The MaPLe compiler: efficient and scalable parallel functional programming

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

Tutorial for HOL

Metamath Zero specification language

Anki is a smart spaced repetition flashcard program

The Power of Prolog: Introduction to modern Prolog

Highly optimized Ternary Convolutional Layer for the ETH course "Advanced Systems Lab" in Spring 2024.