package coq-tree-calculus

This library accompanies the book Reflective Programs in Tree Calculus. In tree calculus, computations are given by natural trees, i.e. finitely-branching trees without labels. The functions, data structures, programs, inputs, outputs and values are all given by binary trees. The trees are built as combinations of a single operator. It has three evaluation rules, for leaves stems and forks. This is enough to support reflective programs such as a size function that can decide its own size, an equality program that can decide its own equality, and self-evaluators than can evaluate themselves. Since this does not require any meta-theory for, say, substitution, quotation, serialisation or Goedel numbers, it is simpler and more powerful than traditional models of computation.

The organisation of the proofs is shown in the _CoqProject file, with one or two files per chapter.