How the kernel works in a LCF theorem prover I heard that there is some mechanism in LCF-based theorem provers that only allows some functions to create values of type theorem. I believe these are based on abstract data types.

Could someone sketch in pseudo-code how does this work? (in case the above is correct)
If I recall correctly, this was chapter 5 or 6 of John Harrison's Handbook of Practical Logic and Automated Reasoning.

Jon Sterling wrote some notes for a recitation a year or two back, specifically for an LCF prover using sequent calculus.