Philip Zucker

awesome-egraphs. An awesome list of e-graph resources

344

knuckledragger. A Low Barrier Proof Assistant

169

z3_tutorial. Jupyter notebooks for tutorial on the Z3 SMT solver

169

FlapPyBird-MPC. Model Predictive Control of a Flappy Bird Clone using Mixed Integer Programming

80

egglog0. Datalog + Egg = Good

66

nand2coq. Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).

59

duckegg. An experiment in using DuckDB for a datalog / egg

27

pcode2c. Convert low ghidra pcode to verifiable C

24

cart_pole. A physical and virtual cartpole

24

fib-anyon. An implementation of Fibonacci Anyons in Haskell

22

prologsolvers. Copies of prolog solvers for use from python

21

ad-lens. Automatic Differentiation using Pseudo Lenses. Neat.

21

eggmt. Egraphs Modulo Theories

20

lens-algebra. Type level algebraic "proofs" using lens combinators

19

snakelog. A Datalog Framework for Python

18

rel. Explorations in relations and the algebra of programming

17

philzook58.github.io. My Blog

16

datalog-book. A book about datalog

13

z3-rise4fun. Z3 tutorials from the rise4fun website

10

not-bad-ccc. Another tact on compiling to categories without a plugin

10

EGraphs.jl. Julia

8

Knuckledragger.jl. Julia Semi-Automated Proof Assistant

7

egraphs2024-talk. HTML

7

basic-ass-shit. Simple Examples to show Haskell can do normal stuff too

6

cvxpy-helpers. some helper routines for modelling MIP in cvxpy

5

Rel.jl. Experiments for categories and relation algebra in Julia

5

shit-ccc. Compiling to Categories the bad way

5

purescript-functor-vector. Vector operations heavily based in Functor composition

5

egg-bench. SMT

5

thoughtbooks. Jupyter Notebook

4

ConvexCat. Experiments

4

souffle-egg. Shell

3

egglogpy. Experiment in egglog python api

3

bap-notes. My notes on BAP (Binary Analysis Platform)

3

wp-lens. Concolic Weakest Precondition as a Lens ¯\_(ツ)_/¯

3

egglog0-talk. TeX

2

search. doinking around with search stuff. Nothin to see here.

2

egglog-z3. Z3 sort for egglog

2

Metatheory.jl. General purpose metaprogramming and algebraic computation library for the Julia programming language

2

learnxinyminutes-docs. Code documentation written as code! How novel and totally my idea!

2

staged-fun. Tinkering around with staged metaprogramming

2

souffle-z3. C++

2

bap-primus-js. OCaml

2

typelevel-rational. Type level rationals and intervals

2

purescript-propel. Purescript bindings to Propel tensor library

2

TrajOpt. Trajectory Optimization Using Pytorch

2

lambda-egglog. Exploring egraphs as ground completion with an eye towards lambdas and theories

1

res-rs. Rust

1

arip. Automated Reasoning in Python

1

emt-egraphs2025. TeX

1