Reflections in Tree Calculus work differnt from lisp quote/unqote used here. It is a hunch, but I think Tree Calculus can implement this (if it is sound) (book pg 64 ff on quote), but not vice-versa.
As far as I know there is no Tree Calculus with (dependent) types, because types in Tree Calculus work different from main stream type theory (you internalize the type checker using reflection (see book pg 58), a bit like I did here with scheme: https://github.com/JanBessai/tcscheme).
As far as I know there is no Tree Calculus with (dependent) types, because types in Tree Calculus work different from main stream type theory (you internalize the type checker using reflection (see book pg 58), a bit like I did here with scheme: https://github.com/JanBessai/tcscheme).