Tree Calculus

The draft of my book “Reflective Programs in Tree Calculus” is now available for comment at Some front-matter is available from

It may be of interest for two reasons:

  • all proofs have been verified in Coq, and
  • the subject matter will be of interest to those who care about foundations.

Tree calculus programs are combinations built from a single operator that satisfies three equations without side-conditions. As well as combinators, it supports reflective programs that: compute the size of programs; compute equality of programs; or self-interpret programs. There is also a combinational account of lambda-calculus and an embedding of it into tree calculus.