Pinned Repositories
ad-lens
Automatic Differentiation using Pseudo Lenses. Neat.
cart_pole
A physical and virtual cartpole
duckegg
An experiment in using DuckDB for a datalog / egg
egglog0
Datalog + Egg = Good
fib-anyon
An implementation of Fibonacci Anyons in Haskell
FlapPyBird-MPC
Model Predictive Control of a Flappy Bird Clone using Mixed Integer Programming
lens-algebra
Type level algebraic "proofs" using lens combinators
nand2coq
Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
rel
Explorations in relations and the algebra of programming
z3_tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
philzook58's Repositories
philzook58/z3_tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
philzook58/egglog0
Datalog + Egg = Good
philzook58/duckegg
An experiment in using DuckDB for a datalog / egg
philzook58/pcode2c
Convert low ghidra pcode to verifiable C
philzook58/philzook58.github.io
My Blog
philzook58/snakelog
A Datalog Framework for Python
philzook58/knuckledragger
Semi-Automated Python Proof Assistant
philzook58/egglogpy
Experiment in egglog python api
philzook58/egraphs2024-talk
philzook58/egglog-rec
Rewriting engine competition benchmarks translated to egglog
philzook58/lambda-egglog
Exploring egraphs as ground completion with an eye towards lambdas and theories
philzook58/pyeprover
A simple repackaging of the E automated theorem prover for ease of installation and execution from python
philzook58/pyvampire
A simple repackaging of the Vampire automated theorem prover
philzook58/res-rs
philzook58/solvers
A solver dump
philzook58/compact-php
A proof of a finitary pigeon hole principle via compactness and the infinitary version, in Lean.
philzook58/datalog-asp-tut
Datalog / Answer Set Programming tutorial
philzook58/doodlescript
philzook58/egg-smol
philzook58/extraction-gym
benchmarking e-graph extraction
philzook58/holpy
Implementation of higher-order logic in Python
philzook58/holpy-wrapper
philzook58/mmverify.py
Metamath verifier in Python
philzook58/pypcode-z3
philzook58/PyRes
Pedagogical first-order prover in Python
philzook58/PyRes-wrapper
Wrapper to install PyRes as library and executables
philzook58/TPDB
The Termination Problem Database
philzook58/twee
An equational theorem prover based on Knuth-Bendix completion
philzook58/vr_experiments
philzook58/vscode-markdown-code-runner
Run code snippets in Markdown.