Here is some of the literature used or browsed during the design and implementation of Belle.

LCF Implementations

Harrison, John and Konrad Slind. A Reference Version of HOL.
Harrison, John. HOL Done Right.
Paulson, Lawrence C. The Foundation of a Generic Theorem Prover.
Paulson, Lawrence C. Isabelle: The Next 700 Theorem Provers.
Paulson, Lawrence C. Designing a Theorem Prover.

General Programming

Aho, Alfred V., Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools.
Chitil, Olaf. Pretty Printing with Lazy Dequeues.
Hughes, John. The Design of a Pretty-printing Library.
Okasaki, Chris. Purely Functional Data Structures.

Miscellaneous

Baader, Franz and Tobias Nipkow. Term Rewriting and All That.
Huet, Gerard. A Unification Algorithm for Typed λ-Calculus.
Hurd, Joe. Predicate Subtyping with Predicate Sets.
Melham, Thomas F. The HOL Logic Extended with Quantification over Type Variables.
Nipkow, Tobias. Order-Sorted Polymorphism in Isabelle.
Nipkow, Tobias and Christian Prehofer. Type Reconstruction for Type Classes.
Wadler, Philip and Stephen Blott. How to make ad-hoc polymorphism less ad hoc.
Wenzel, Markus. Type Classes and Overloading in Higher-Order Logic.