Stars
A C function for solving 8-bit SAT problems using bit manipulation for brute force. Surprisingly fast.
Tactics for discharging Lean goals into SMT solvers.
An tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.
Current [2025·01] source repository for the Logoi 1) natural programming language, 2) minimalist tutorial & 3) hyperextensible/mouseless text editor.
A toy functional language based on modal type theory. Try it online: https://mtt-lang.github.io/mtt-web
An inductive logic programming system
A statically typed embedding of miniKanren in Haskell
LoTREC is an automated theorem prover for modal and description logic. It allows students and researchers in logic to define well-known and new exotic logics with Kripke's semantics, and to check t…
Restoration for TEMPEST images using deep-learning
Scripts for analyzing LiquidHaskell benchmark logs
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
A first-order concurrent automated theorem prover
A monad for interfacing with external SAT solvers
A monad for interfacing with external SMT solvers
Copies of prolog solvers for use from python
Agda formalisation of dual-context constructive modal logics.
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
A massively parallel, high-level programming language
Re-implementation of the TASO compiler using equality saturation