jihoolang

A systems programming language that is as fast as C and memory-safe without lifetime annotations or a garbage collector.

A small Rust checker for explicit derivation certificates in many-sorted, first-order Horn theories. The caller supplies the theory and exact goals; the certificate supplies rule applications and references to earlier steps.

Compile-time proof checking experiments for jihoo: a Horn certificate kernel, general proofs and checked codecs