The Foundation of a Generic Theorem Prover (1989) [pdf] (arxiv.org)

See also “Designing a Theorem Prover” https://arxiv.org/pdf/cs/9301110

And chapter 10 of ML for the working programmer, freely available at https://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html

[flagged]

Great paper for exploring the foundations of Isabelle. It's a shame the rest of the literature needed to properly understand Isabelle is scattered amongst many papers.

What are the limits of a generic implementation?

The individual object calculi are already complicated, when does the meta-logic reach its limits?