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

[082349872349872]

https://arxiv.org/pdf/cs/9301105

[zermelo44]

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.

[timmg → zermelo44]

Any suggestions for those papers?

[i_don_t_know]

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

[hackandthink]

What are the limits of a generic implementation?

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