Stanford LCF

Stanford LCF was the first implementation of Scott's LCF. It was produced at Stanford in the early 1970s.

Much of the information here comes from Gordon 2000.

Description

Gordon 2000 describes the system as follows:

Proofs are conducted by declaring a main goal (a formula in Scott’s logic) and then splitting it into subgoals using a fixed set of subgoaling commands (such as induction to generate the basis and step). Subgoals are either solved using a simplifier or split into simpler subgoals until they can be solved directly. Data structures representing formal proofs in Scott’s logic are created when proof commands are interpreted. These can consume a lot of memory.

Thus, Stanford LCF suffered from two serious technical deficiencies:

1. It stored entire formal proofs which it could check, thereby using far too much memory.
2. It had a fixed set of "proof commands" that could not easily be extended.

Starting in 1973, Milner sought to resolve these issues through the design and implementation of Edinburgh LCF.

The resolution of issue (1) in particular led to the articulation of the famous LCF architecture.

References

• The Stanford LCF system is described in

• Some historical information about Stanford LCF is available in section 2 of

@incollection{gordon_2000,
	title = {From {LCF} to {HOL}: a short history},
	url = {https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf},
	booktitle = {Proof, {Language}, and {Interaction}: {Essays} in {Honour} of {Robin} {Milner}},
	author = {Gordon, Mike},
	editor = {Plotkin, Gordon and Stirling, Colin P. and Tofte, Mads},
	year = {2000}
}