Stories by philzook

Constrained Horn Clauses for Bap (2022)

Verifying Nand2Tetris Assembly with Constrained Horn Clauses (2021)

Egglog Examples: Pullbacks, Ski, Lists, and Arithmetic (2021)

Proving a Category Theory Theorem with Rust and Egraphs

Egglog: A Prolog Syntax for the Egg Egraph Library (2021)

An Interpreter of the Algebra of Programming in miniKanren

Making a “MiniKanren” using Z3Py

A Simple, Probably-Not-Exp-Time Disjoint Set in Coq

A Simplified E-graph Implementation

Formal Methods for the Informal Engineer 2021

Rewriting Monoidal Categories in the Browser with Egg

Progress on Automated Reasoning for Catlab with Metatheory.jl Egraphs

Translating My Z3 Tutorial to Coq

CEGARing Exponentials into Z3 with Intervals and Python Coroutines

Z3, the Word Problem, and Path Homotopy as Equality

Automated Propositional Sequent Proofs in the Browser with Tau Prolog

Developing Mathematical Software in C

Sketchy Exact Reals from Interval Arithmetic (2021)

Weakest Precondition with Z3Py

Modeling TLA+ in Z3Py

1
2