An important feature of the chdkr project, by comparison with prior support for reasoning in HOL is the aim to use HOL as an underlying abstract representation for declarative knowledge of all kinds, and to support an architecture for knowledge representation which is suitable for the entire body of declarative knowledge of the human race and its intelligent progeny.
This document is a first approach to turning that idea into a formal specification and implementation.
The story may be split into two parts.