The draft of my book “Reflective Programs in Tree Calculus” is now available for comment at https://github.com/barry-jay-personal/tree-calculus/blob/master/tree_book.pdf Some front-matter is available from https://github.com/barry-jay-personal/tree-calculus/blob/master/tweets_on_trees.pdf
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.