Ciao is a modern Prolog implementation that builds up from a logic-based simple kernel designed to be portable, extensible, and modular.

NES emulator in <5000 bytes of C

A Rocq version of the miniF2F dataset

An updated version of miniF2F with lots of fixes and informal statements / solutions.

A toy example of a verified compiler.

Online compiler for HIP and NVIDIA® CUDA® code to WebGPU

[Mirror] Stepping stones to a better Emacs experience

Inspirational Mapping

import a twitter archive into bsky

Prolog, Datalog, languages, resources, and beyond!

Pretty display on a timeline of CS conference lists cross-referenced with calls for papers from WikiCFP

A lightweight keyboard for Android

A Low Barrier Proof Assistant

ICOT PIMOS operating system

⛓️ Simple verified compiler in Lean4. Lisp-like interpreter, simulated processor and correctness proofs.

Proof exercises in Lean4 and Isabelle/HOL

LLM training in simple, raw C/CUDA

Markdown file of the list and explanations of all mathlib4 tactics

Hitchhiker's Guide to Logical Verification (2023 Edition)

Microsoft MakeCode (PXT - Programming eXperience Toolkit)

Inference Llama 2 in one file of pure C

The CompCert formally-verified C compiler

Farbrausch demo tools 2001-2011

Web-based music player for a variety of video game and chiptune music formats.

This package includes ASP encodings of the Curriculum-Based Course Timetabling (CB-CTT) Problem.

Clingo on the web

Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs