Primary evidence
- Implementation and Applications of Scott's Logic for Computable FunctionsS1 · Primary research · Paper · 1972-01-01
Stanford LCF demonstrates interactive machine checking for Scott's Logic for Computable Functions
Stanford LCF let users state proof goals, decompose them into subgoals and apply simplification and inference commands while the machine checked the resulting formal derivations.
What happened?
Robin Milner's January 1972 publication described an implemented proof checker for Scott's Logic for Computable Functions and showed formal reasoning about recursively defined programs; later historical accounts identify this system as Stanford LCF, developed at Stanford in 1971–1972 with Richard Weyhrauch and Malcolm Newey.
Stanford LCF let users state proof goals, decompose them into subgoals and apply simplification and inference commands while the machine checked the resulting formal derivations. It predated the extensible ML metalanguage, abstract theorem type and programmable tactics that characterized Edinburgh LCF.
Why it matters
The system made interactive machine-assisted proof concrete and exposed limitations in memory use and fixed proof commands. Those limitations became design targets for Edinburgh LCF, which in turn shaped the trusted-kernel architecture of many later proof assistants.
Significance rationale: Stanford LCF implemented Dana Scott's Logic for Computable Functions as an interactive proof checker with subgoaling and simplification, establishing practical experience that directly motivated the later Edinburgh LCF architecture.
Historical context
Earlier developments
—
Later developments
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Computation only
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- The machine checked formal derivations and provided subgoaling and simplification support, while users supplied substantial proof direction.
- Human contribution
- Robin Milner, Richard Weyhrauch, Malcolm Newey and collaborators developed the Stanford LCF proof-checking system and its applications to reasoning about programs.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- stanford-lcf, lcf
- Organizations
- stanford-university
- Problems
- program-verification
- Methods
- proof-checking, interactive-theorem-proving, subgoaling, simplification, typed-lambda-calculus
Sources & artifacts
- Implementation and Applications of Scott's Logic for Computable FunctionsS1 · Primary research · Paper · accessed 2026-09-15
- From LCF to HOL: A Short HistoryS2 · Official institutional · Paper · accessed 2026-09-15
Verification history
- 1972-01-01 · Paper released · E2 · Research record
The ACM publication documents the implemented proof checker, while Mike Gordon's later historical account distinguishes Stanford LCF from its Edinburgh successor and describes the fixed-command and proof-storage limitations that motivated the redesign.
Corrections
- 2026-09-15
The record was narrowed from a generic LCF/trusted-kernel account to Stanford LCF. ML, the abstract theorem type and programmable tactics belong to the later Edinburgh LCF lineage rather than the 1972 Stanford system.