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)

Design, play with, and analyze sequent calculus proof systems.

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml

llm-powered theorem proving for isabelle/hol

🗑️ a paste bin.

wastebin is a pastebin 📝

universal pastebin server

Command line pastebin for sharing terminal output.

This implements a 64-bit version of vusec/vuzzer fuzzing tool.

Driller: augmenting AFL with symbolic execution!

An OCaml mutation tester

Verified compiler from LambdaBox to WebAssembly, C, Rust, and OCaml

The Ott tool for writing definitions of programming languages and calculi

Aproximate emulator for a subset of Felix-C-256 computer jobs with Assiris assembler

The main codex repository

🧮 Programming with pure lambda calculus

A small C compiler