Craig Alan Feinstein (Aug 02 2026 at 19:16): Craig Alan Feinstein (Aug 02 2026 at 19:16):Can anyone recommend books which explain the theory behind formal proof checking?
Ant S. (Aug 03 2026 at 19:52):I would suggest reading Robin Milner's paper on LCF, but these slides seem pretty good
Ant S. (Aug 03 2026 at 19:54):If you are not yet at a point where you may find papers comfortable to read (that's OK), https://dl.acm.org/doi/10.5555/34057 is a really good book. I mostly read it for the section on domain theory.
Ant S. (Aug 03 2026 at 19:55):That's more of a historical note on proof checking, but knowing the LCF philosophy is never a bad thing
Ant S. (Aug 03 2026 at 19:55):(I mean, I say this on the Isabelle zulip)
Ant S. (Aug 03 2026 at 19:56):(@isabelle people if I've said something super wrong feel free to correct me lol)
Craig Alan Feinstein (Aug 04 2026 at 13:19):Thank you, Craig
Ant S. (Aug 04 2026 at 17:43):Hi Craig,
https://www.sciencedirect.com/science/chapter/handbook/abs/pii/B9780444516244500046
I found this as well. Might be useful. All 3 authors are notable for their work in theorem proving.
Chris Anto Fröschl (Aug 04 2026 at 17:59):There is also a reference book about to be released at https://link.springer.com/book/9783031851896
You can find a draft chapter at https://arxiv.org/abs/2009.09541
Lukas Stevens (Aug 04 2026 at 18:15):For a hands-on introduction to the construction of LCF-style proof assistants see The Handbook of Practical Logic and Automated Reasoning.
Craig Alan Feinstein (Aug 04 2026 at 23:14):Thank you all. So far the John Harrison book looks most like what I’m looking for since its examples seem like basic logic and math.
Last updated: Aug 05 2026 at 21:11 UTC