Code repositories: Difference between revisions
Jump to navigation
Jump to search
m (add https://github.com/ccz181078/busycoq/tree/BB6/verify) |
(Link to Skelet) |
||
| Line 17: | Line 17: | ||
|A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs | |A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs | ||
|- | |- | ||
|Georgi Georgiev (Skelet) | |Georgi Georgiev ([[Skelet]]) | ||
|[https://skelet.ludost.net/bb/ Link] | |[https://skelet.ludost.net/bb/ Link] | ||
|See [[bbfind | |See [[bbfind]]. Wrapped via [https://gist.github.com/m1el/d514a353cccde531c298b725043404af bbfind-stdin by @wizord] | ||
|- | |- | ||
|@mxdys | |@mxdys | ||
Revision as of 19:31, 6 February 2025
| Creator | Link | Notes |
|---|---|---|
| bbchallenge | Link | Official bbchallenge deciders |
| @mxdys | Link | Coq proof of BB(5) = 47,176,870. See Coq-BB5. |
| @mei | Link | A hybrid Coq/Rust/OCaml repo implementing very fast deciders plus verified proofs |
| Georgi Georgiev (Skelet) | Link | See bbfind. Wrapped via bbfind-stdin by @wizord |
| @mxdys | Link | Coq proof of some deciders and some solved machines in BB(6) |
| Mateusz Naściszewski @Mateon1 | Link | Accelerated TM simulators in Python utilizing memoization (like HashLife) |
| Mateusz Naściszewski @Mateon1 | Link | Forward segment TM decider by @Mateon1 (variant of Halting Segment) |
| Mateusz Naściszewski @Mateon1 | Link | Closed Position Set (CPS) TM decider implementation |
| Mateusz Naściszewski @Mateon1 | Link | Closed Tape Language (CTL) SAT Solver; TODO dependencies still Discord posts |
| @savask | Link | Collection of deciders |
| @savask | Link | Closed Position Set (CPS), reverse-engineered from Skelet's bbfind program |
| @savask | Link | Decider for Bouncers |
| @savask | Link | Reproduction of @mxdys' RepWL_ES decider (repeated block decider) |
| @djmati1111 | Link | The first SAT-based Finite Automata Reduction (FAR) decider |
| Frans Faase | Link | An early Closed Tape Language (CTL) verifier |
| @Iijil | Link | Decider for Bouncers |
| @Iijil | Link | Bruteforce Closed Tape Language (CTL) decider |
| @Iijil | Link | Meet-in-the-Middle Weighted Finite Automata Reduction (MITMWFAR) decider |
| @Iijil | Link | 4-symbol to 2-symbol TM compiler |
| Jason Yuen @-d | Link | Some progress toward a FAR verifier checked by Lean |
| Matthew House @LegionMammal976 | Link | An accelerated Bigfoot simulator |
| Nathan Fenner @nathanf | Link | Formally verified deciders using Dafny |
| Nathan Fenner @nathanf | Link | Formally verified Closed Tape Language (CTL) verifier |
| Nathan Fenner @nathanf | Link | Closed Tape Language (CTL) decider |
| Nathan Fenner @nathanf | Link | Closed Position Set (CPS) simplification: uses less resources and is less strong |
| @nickdrozd | Link | |
| @star | Link | |
| Shawn Ligocki @sligocki | Link | |
| Tony Guilfoyle | Link | |
| Justin Blanchard @UncombedCoconut | Link | |
| Justin Blanchard @UncombedCoconut | Link | Finite Automata Reducion (FAR) decider |
| Justin Blanchard @UncombedCoconut | Link | Finite Automata Reducion (FAR) verifier |
| Pavel Kropitz @uni | Link | |
| Dan Briggs | Link | TM proofs/writing |