How the kernel works in a LCF theorem prover

Question

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)

Answer 1

Here are some thoughts and code from the kernel (file thm.ML in Isabelle/Pure) from Isabelle:

abstype thm = Thm of
 deriv *                        (*derivation*)
 {cert: Context.certificate,    (*background theory certificate*)
  tags: Properties.T,           (*additional annotations/comments*)
  maxidx: int,                  (*maximum index of any Var or TVar*)
  shyps: sort Ord_List.T,       (*sort hypotheses*)
  hyps: term Ord_List.T,        (*hypotheses*)
  tpairs: (term * term) list,   (*flex-flex pairs*)
  prop: term}                   (*conclusion*)
and deriv = Deriv of
 {promises: (serial * thm future) Ord_List.T,
  body: Proofterm.proof_body}
with

Also here is a quotation of from Paulson book on ML. About abstract datatypes he says:

A modular structure makes a program easier to understand. Better still, the modules ought to serve as interchangeable parts: replacing one module by an improved version should not require changing the rest of the. program. Standard ml's abstract types and functors can help us meet this objective too. A module may reveal its internal details. When the module is replaced, other parts of the program that depend upon such details will fail. ML provides several ways of declaring an abstract type and related operations, while hiding the type's representation.

So you cannot instantiate an abstract datatype you can use it (its fields + functions). The matter on how you implement this feature is very of dependent of the language. If you want to do it in the lambda-calculus, there should be something like that in Benjamin Pierce's TAPL book on the later chapters.

A nice reference for this is also here.

Answer 2

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.