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].
[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:
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.
R. Milner. Logic for computable functions; description of a machine implementation. Technical Report STAN-CS-72-288, A.I. Memo 169, Stanford University, 1972. https://apps.dtic.mil/sti/citations/AD0785072
Gordon, Mike. 2000. ‘From LCF to HOL: A Short History’. In Proof, Language, and Interaction: Essays in Honour of Robin Milner, edited by Gordon Plotkin, Colin P. Stirling, and Mads Tofte. https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf.
@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}
}