How the kernel works in a LCF theorem prover
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.