Elamur Research⌕
☰
home / papers / 2000 / From LCF to HOL: a short history

From LCF to HOL: a short history

Paper · 2000 · Mike Gordon

Summary

Mike Gordon's historical essay traces how the LCF approach to interactive theorem proving grew into the HOL proof assistant, and it credits Robin Milner as the central figure. The story begins with Stanford LCF (1972), a checker for Dana Scott's logic of computable functions. It kept complete proof objects in memory and allowed only a fixed set of backward subgoaling commands. Edinburgh LCF fixed both weaknesses. Theorems became values of an abstract data type built only from axioms and inference rules, so strict typing guaranteed soundness without storing proofs. The new language ML let users write their own proof strategies (tactics) and combinators over them (tacticals). Cambridge LCF, developed mainly by Larry Paulson in collaboration with Gérard Huet, added conversions, a derived simplifier, discrimination nets and full predicate calculus. Gordon's hardware-verification work, inspired by CCS, led through LCF LSM to HOL. HOL keeps LCF's syntax but interprets types as ordinary sets instead of Scott domains. The essay is valuable as a first-hand account of design choices behind modern proof assistants and the ML language family.

Key points

  • Edinburgh LCF originated the "LCF approach": theorem security comes from an abstract type plus ML's strict typechecking, and ML gained exception handling so that failing tactics could be handled.
  • During the Paulson–Huet collaboration, an ML compiler made LCF roughly 20 times faster than the interpreted version. Cambridge LCF was finished around 1985 and later ported to Standard ML by Mikael Hedlund, as documented in Paulson's 1987 book Logic and Computation.
  • LCF LSM, a stopgap system for the Logic of Sequential Machines, was used to verify the toy Tamarack microprocessor. RSRE also used the LSM notation to specify the Viper processor.
  • HOL is distributed with polished libraries and with less strictly checked "contributions". These cover reals, n-bit words, group theory, UNITY and Hoare logics, Boyer–Moore heuristics and parts of the Standard ML definition.
  • By the time of writing, Tom Melham's HOL bibliography listed nearly 400 publications and 30 dissertations. Nine HOL Users Workshops had been held, and a HOL2000 initiative had been launched.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 worksComputer Science Applications · 184 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Mike Gordon. 2000. From LCF to HOL: a short history. Proof, Language, and Interaction (MIT Press), 169–185.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{gordon2000lcf,
  title = {{From LCF to HOL: a short history}},
  author = {Mike Gordon},
  booktitle = {Proof, Language, and Interaction (MIT Press), 169–185},
  year = {2000},
  doi = {10.7551/mitpress/5641.003.0012},
  url = {https://doi.org/10.7551/mitpress/5641.003.0012}
}

References

49 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Graham Birtwistle and P. A. Subrahmanyam, editors. Current Trends in Hardware Verification and Automated Theorem Proving. Springer, 1989. find
  2. R. J. Boulton. Lazy techniques for fully expansive theorem proving. Formal Methods in System Design, 3(1/2):25–47, August 1993. find
  3. E. Charniak, C. K. Riesbeck, and D. V. McDermott. Artificial Intelligence Programming. Lawrence Erlbaum Associates, 1980. find
  4. A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5:56–68, 1940. find
  5. Avra Cohn. A proof of correctness of the VIPER microprocessor: The first level. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 27–71. Kluwer Academic Publishers, 1988. find
  6. Avra Cohn. Correctness properties of the Viper block model: The second level. In Birtwistle and Subrahmanyam [1], pages 1–91. find
  7. Avra Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127–139, 1989. find
  8. R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986. find
  9. Thierry Coquand and Gérard Huet. Constructions: A higher order proof system for mechanizing mathematics. In Bruno Buchberger, editor, EUROCAL ’85, volume 203 of Lecture Notes in Computer Science, pages 151–184, Berlin, 1985. Springer-Verlag. find
  10. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988. find
  11. M. J. C. Gordon. LCF LSM: A system for specifying and verifying hardware. Technical Report 41, University of Cambridge Computer Laboratory, 1983. find
  12. M. J. C. Gordon. Proving a computer correct. Technical Report 42, University of Cambridge Computer Laboratory, 1983. find
  13. M. J. C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Milne and Subrahmanyam [33], pages 153–177. find
  14. M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993. find
  15. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979. find
  16. B. T. Graham. The SECD Microprocessor: A Verification Case Study. Kluwer, 1992. 27 http://lal.cs.byu.edu/lal/hol2000/hol2000.html ↗
  17. Jim Grundy. A window inference tool for refinement. In Clifford Bryn Jones, B. Tim Denvir, and Roger C. F. Shaw, editors, Proceedings of the 5th Refinement Workshop, Workshops in Computing, pages 230–254, Lloyd’s Register, London, January 1992. BCS FACS, Springer-Verlag. find
  18. E. L. Gunter. Doing algebra in simple type theory. Technical Report MS-CIS-89-38, Dept. of Computer and Information Science, Moore School of Engineering, University of Pennsylvania, June 1989. find
  19. F. K. Hanna and N. Daeche. Specification and verification using higher-order logic: a case study. In Milne and Subrahmanyam [33], pages 179–213. find
  20. John Harrison. Constructing the real numbers in HOL. Formal Methods in System Design, 5:35–59, 1994. find
  21. John Harrison. A mizar mode for HOL. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, volume 1125 of Lecture Notes in Computer Science, pages 203–220, Turku, Finland, 1996. Springer-Verlag. find
  22. John Harrison and Laurent Théry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Joyce and Seger [28], pages 174–184. find
  23. J. Herbert. Case study of the Cambridge Fast Ring ECL chip using HOL. Technical Report 123, Computer Laboratory, University of Cambridge, UK, 1988. find
  24. Formal Methods in System Design, volume 3, number 1/2. Special issue on Higher Order Logic Theorem Proving and its Applications, August 1993. find
  25. Formal Methods in System Design, volume 5, number 1/2. Special issue on Higher Order Logic Theorem Proving and its Applications, July/August 1993. find
  26. The Computer Journal, volume 38, number 2. Special issue on Higher Order Logic Theorem Proving and its Applications, 1995. find
  27. G. Birtwistle J. Joyce and M. J. C. Gordon. Proving a computer correct in higher order logic. Technical Report 100, University of Cambridge Computer Laboratory, 1986. find
  28. Jeffrey J. Joyce and Carl Seger, editors. volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada, 1993. Springer-Verlag. find
  29. T. F. Melham. Automating recursive type definitions in higher order logic. In Birtwistle and Subrahmanyam [1], pages 341–386. find
  30. T. F. Melham. A package for inductive relation definitions in hol. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 32–37. IEEE Computer Society Press, August 1991. find
  31. T. F. Melham. The HOL logic extended with quantification over type variables. Formal Methods in System Design, 3(1/2):7–24, August 1993. find
  32. Thomas F. Melham and Juanito Camilleri, editors. Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, LNCS 859. Springer, September 1994. find
  33. G. Milne and P. A. Subrahmanyam, editors. Formal Aspects of VLSI Design. North-Holland, 1986. find
  34. R. Milner. Logic for computable functions; description of a machine implementation. Technical Report STAN-CS-72-288, A.I. Memo 169, Stanford University, 1972. find
  35. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348–375, December 1978. find
  36. R. Milner and R. Weyhrauch. Proving compiler correctness in a mechanized logic. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 7, pages 51–70. Edinburgh University Press, 1972. find
  37. Robin Milner. Communication and Concurrency. Prentice-Hall, 1989. find
  38. Monica Nesi. A formalization of the process algebra CCS in higher order logic. Technical Report 278, University of Cambridge, Computer Laboratory, December 1992. find
  39. L. C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983. find
  40. L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF, volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987. find
  41. L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990. find
  42. Lawrence C. Paulson. Verifying the unification algorithm in LCF. Science of Computer Programming, 5:143–170, 1985. find
  43. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828. find
  44. K. Petersson. A programming system for type theory. Technical Report 21, Department of Computer Science, Chalmers University, Göteborg, Sweden, 1982. find
  45. E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, editors. Higher Order Logic Theorem Proving and Its Applications 8th International Workshop, LNCS 971. Springer, September 1995. find
  46. Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121:411–440, 1993. Annotated version of the 1969 manuscript. find
  47. Konrad Slind. Function definition in higher order logic. In Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs’96, number 1125 in Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer Verlag. find
  48. Joakim von Wright, Jim Grundy, and John Harrison, editors. volume 1125 of Lecture Notes in Computer Science, Turku, Finland, 1996. Springer-Verlag. find
  49. P. J. Windley. The practical verification of microprocessor designs. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 32–37. IEEE Computer Society Press, August 1991. Mike Gordon October 31, 1996 find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/gordon-2000-lcf-hol-short-history/