Tree calculus was discovered by Barry Jay. This repo is maintained by Johannes Bader and collects implementations and other resources.
- Book: Reflective Programs in Tree Calculus (Barry Jay, 2021)
- Rocq proofs can be found in the same repo
- Website with demos
- Paper: Typed Program Analysis without Encodings (Barry Jay, PEPM 2025)
- Recording of the talk
- Rocq proofs and slides can be found in the same repo
- Barry's blog
- Article: A visual introduction to tree calculus
- This repo: Implementations, tests, benchmarks and various pointers