Philip Zucker is a physics and computer science enthusiast documenting ideas and experiments in a lab-notebook-style blog, focused on functional programming, compilers, formal methods, and scientific computation.
22 articles from this blog
Explores cyclic terms, arenas, and flat equational systems in the context of e-graphs and formal reasoning.
Explores lifting e-graphs, a technique to handle variable binding in equality saturation by treating context as part of a term.
Using eprover's Knuth-Bendix completion to generate rewrite systems and integrating them with Knuckledragger via Prolog.
Explores dependent type theory semantics using Python frozensets, emphasizing the concept of 'family' as set-valued functions and judgements as mappings.
Explores functional combinators for lifting and lowering functions using The Dump Calculus, aimed at first-orderizing trivial functional manipulations for e-graphs.
Exploring thinning/lifting e-graphs for alpha equivalence using functional lifting combinators and Python examples.
Explores alpha-equivalent hash consing using thinnings (bitvectors) for efficient term sharing in lambda calculus and compiler analysis.
Explores advanced union-find data structures with annotations like offsets and thinnings for e-graphs and de Bruijn index manipulation.
Introducing Knuckledragger, a Python tool for refinement modeling and verification of RISC-V assembly code using symbolic execution.
Explores the concept of 'thinnings' as witness data for sublist relationships, connecting them to programming and lambda calculus.
An update on the Knuckledragger theorem prover project, covering kernel changes, AI experiments, symbolic union, and future development plans.
Exploring the use of SMT solvers and the SMT-LIB language as an intermediate representation (IR) for compiler design and optimization.
Introducing a Python library for seamless interoperability with the Lean theorem prover, allowing Lean functions to be called directly from Python code.
An exploration of Ground Lexicographic Path Ordering (LPO) for term rewriting systems, including a Python implementation and property tests.
Explores generalizing term operations like unification and rewriting to advanced structures like AC terms and rational terms, with Python examples.
Explores contextual union finds for rewriting under assumptions in egraph systems, comparing dense and sparse implementations.
A developer's enthusiastic recap of a specialized workshop on egraphs and compilers, covering technical discussions, potential collaborations, and project ideas.
Explores combining SMT solvers CVC5 and Z3 using the Nelson-Oppen method, focusing on theory combination and purification.
Explores asymmetric completion, a union-find algorithm variant for inequality reasoning, with Python implementation insights.
Introducing a Lean-like syntax parser for the Knuckledragger theorem prover to improve formula readability over verbose Python/Z3Py syntax.
