---
title: "From LCF to HOL: a short history — paper by Gordon (2000)"
description: "Mike Gordon's historical essay traces how the LCF approach to interactive theorem proving grew into… 49 references, cited by 4 papers here."
authors: ["Mike Gordon"]
year: 2000
venue: "Proof, Language, and Interaction (MIT Press), 169–185"
source: "https://www.cl.cam.ac.uk/archive/mjcg/"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/gordon-2000-lcf-hol-short-history/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/gordon-2000-lcf-hol-short-history/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2000](https://md.research.elamur.ai/free/en/papers/2000/) / From LCF to HOL: a short history

# From LCF to HOL: a short history

**Authors:** Mike Gordon · **Year:** 2000 · **Venue:** Proof, Language, and Interaction (MIT Press), 169–185 · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.7551/mitpress/5641.003.0012) · [PDF](https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf) · [OpenAlex](https://openalex.org/W3151527711)

**Citations:** 118 citations (OpenAlex, 2026-10-14) · [4](https://md.research.elamur.ai/free/en/papers/gordon-2000-lcf-hol-short-history/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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.*

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works · [🖥️ Computer Science Applications](https://md.research.elamur.ai/free/en/shelves/computer-science/computer-science-applications/) · 184 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/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.

```bibtex
@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}
}
```

- [← previous RSTTool 2.4 - A markup Tool for Rhetorical Structure Theory](https://md.research.elamur.ai/free/en/papers/donnell-2000-rsttool-2-4-markup-tool/)
- [next → English Senseval: Report and Results](https://md.research.elamur.ai/free/en/papers/kilgarriff-2000-english-senseval-report-results/)
- [↑ back to papers of 2000](https://md.research.elamur.ai/free/en/papers/2000/)

## 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](https://scholar.google.com/scholar?q=Graham+Birtwistle+and+P%2E+A%2E+Subrahmanyam%2C+editors%2E+Current+Trends+in+Hardware+Verification+and+Automated+Theorem+Proving%2E+Springer%2C+1989%2E)
2. R. J. Boulton. Lazy techniques for fully expansive theorem proving. Formal Methods in System Design, 3(1/2):25–47, August 1993. [find](https://scholar.google.com/scholar?q=R%2E+J%2E+Boulton%2E+Lazy+techniques+for+fully+expansive+theorem+proving%2E+Formal+Methods+in+System+Design%2C+3%281%2F2%29%3A25%E2%80%9347%2C+August+1993%2E)
3. E. Charniak, C. K. Riesbeck, and D. V. McDermott. Artificial Intelligence Programming. Lawrence Erlbaum Associates, 1980. [find](https://scholar.google.com/scholar?q=E%2E+Charniak%2C+C%2E+K%2E+Riesbeck%2C+and+D%2E+V%2E+McDermott%2E+Artificial+Intelligence+Programming%2E+Lawrence+Erlbaum+Associates%2C+1980%2E)
4. A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5:56–68, 1940. [find](https://scholar.google.com/scholar?q=A%2E+Church%2E+A+formulation+of+the+simple+theory+of+types%2E+The+Journal+of+Symbolic+Logic%2C+5%3A56%E2%80%9368%2C+1940%2E)
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](https://scholar.google.com/scholar?q=Avra+Cohn%2E+A+proof+of+correctness+of+the+VIPER+microprocessor%3A+The+first+level%2E+In+Graham+Birtwistle+and+P%2E+A%2E+Subrahmanyam%2C+editors%2C+VLSI+Specification%2C+Verification+and+Synthesis%2C+pages+27%E2%80%9371%2E+Kluwe)
6. Avra Cohn. Correctness properties of the Viper block model: The second level. In Birtwistle and Subrahmanyam [1], pages 1–91. [find](https://scholar.google.com/scholar?q=Avra+Cohn%2E+Correctness+properties+of+the+Viper+block+model%3A+The+second+level%2E+In+Birtwistle+and+Subrahmanyam+%5B1%5D%2C+pages+1%E2%80%9391%2E)
7. Avra Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127–139, 1989. [find](https://scholar.google.com/scholar?q=Avra+Cohn%2E+The+notion+of+proof+in+hardware+verification%2E+Journal+of+Automated+Reasoning%2C+5%282%29%3A127%E2%80%93139%2C+1989%2E)
8. R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986. [find](https://scholar.google.com/scholar?q=R%2E+L%2E+Constable+et+al%2E+Implementing+Mathematics+with+the+Nuprl+Proof+Development+System%2E+Prentice%2DHall%2C+1986%2E)
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](https://scholar.google.com/scholar?q=Thierry+Coquand+and+Ge%CC%81rard+Huet%2E+Constructions%3A+A+higher+order+proof+system+for+mechanizing+mathematics%2E+In+Bruno+Buchberger%2C+editor%2C+EUROCAL+%E2%80%9985%2C+volume+203+of+Lecture+Notes+in+Computer+Science%2C+pag)
10. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988. [find](https://scholar.google.com/scholar?q=Thierry+Coquand+and+Ge%CC%81rard+Huet%2E+The+calculus+of+constructions%2E+Information+and+Computation%2C+76%3A95%E2%80%93120%2C+1988%2E)
11. M. J. C. Gordon. LCF LSM: A system for specifying and verifying hardware. Technical Report 41, University of Cambridge Computer Laboratory, 1983. [find](https://scholar.google.com/scholar?q=M%2E+J%2E+C%2E+Gordon%2E+LCF+LSM%3A+A+system+for+specifying+and+verifying+hardware%2E+Technical+Report+41%2C+University+of+Cambridge+Computer+Laboratory%2C+1983%2E)
12. M. J. C. Gordon. Proving a computer correct. Technical Report 42, University of Cambridge Computer Laboratory, 1983. [find](https://scholar.google.com/scholar?q=M%2E+J%2E+C%2E+Gordon%2E+Proving+a+computer+correct%2E+Technical+Report+42%2C+University+of+Cambridge+Computer+Laboratory%2C+1983%2E)
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](https://scholar.google.com/scholar?q=M%2E+J%2E+C%2E+Gordon%2E+Why+higher%2Dorder+logic+is+a+good+formalism+for+specifying+and+verifying+hardware%2E+In+Milne+and+Subrahmanyam+%5B33%5D%2C+pages+153%E2%80%93177%2E)
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](https://scholar.google.com/scholar?q=M%2E+J%2E+C%2E+Gordon+and+T%2E+F%2E+Melham%2C+editors%2E+Introduction+to+HOL%3A+a+theorem%2Dproving+environment+for+higher%2Dorder+logic%2E+Cambridge+University+Press%2C+1993%2E)
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](https://scholar.google.com/scholar?q=M%2E+J%2E+C%2E+Gordon%2C+R%2E+Milner%2C+and+C%2E+P%2E+Wadsworth%2E+Edinburgh+LCF%3A+A+Mechanised+Logic+of+Computation%2C+volume+78+of+Lecture+Notes+in+Computer+Science%2E+Springer%2DVerlag%2C+1979%2E)
16. B. T. Graham. The SECD Microprocessor: A Verification Case Study. Kluwer, 1992. 27 [http://lal.cs.byu.edu/lal/hol2000/hol2000.html](http://lal.cs.byu.edu/lal/hol2000/hol2000.html) [↗](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](https://scholar.google.com/scholar?q=Jim+Grundy%2E+A+window+inference+tool+for+refinement%2E+In+Clifford+Bryn+Jones%2C+B%2E+Tim+Denvir%2C+and+Roger+C%2E+F%2E+Shaw%2C+editors%2C+Proceedings+of+the+5th+Refinement+Workshop%2C+Workshops+in+Computing%2C+pages+230%E2%80%93)
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](https://scholar.google.com/scholar?q=E%2E+L%2E+Gunter%2E+Doing+algebra+in+simple+type+theory%2E+Technical+Report+MS%2DCIS%2D89%2D38%2C+Dept%2E+of+Computer+and+Information+Science%2C+Moore+School+of+Engineering%2C+University+of+Pennsylvania%2C+June+1989%2E)
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](https://scholar.google.com/scholar?q=F%2E+K%2E+Hanna+and+N%2E+Daeche%2E+Specification+and+verification+using+higher%2Dorder+logic%3A+a+case+study%2E+In+Milne+and+Subrahmanyam+%5B33%5D%2C+pages+179%E2%80%93213%2E)
20. John Harrison. Constructing the real numbers in HOL. Formal Methods in System Design, 5:35–59, 1994. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+Constructing+the+real+numbers+in+HOL%2E+Formal+Methods+in+System+Design%2C+5%3A35%E2%80%9359%2C+1994%2E)
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](https://scholar.google.com/scholar?q=John+Harrison%2E+A+mizar+mode+for+HOL%2E+In+Joakim+von+Wright%2C+Jim+Grundy%2C+and+John+Harrison%2C+editors%2C+Theorem+Proving+in+Higher+Order+Logics%3A+9th+International+Conference%2C+TPHOLs%E2%80%9996%2C+volume+1125+of+Lectu)
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](https://scholar.google.com/scholar?q=John+Harrison+and+Laurent+The%CC%81ry%2E+Extending+the+HOL+theorem+prover+with+a+computer+algebra+system+to+reason+about+the+reals%2E+In+Joyce+and+Seger+%5B28%5D%2C+pages+174%E2%80%93184%2E)
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](https://scholar.google.com/scholar?q=J%2E+Herbert%2E+Case+study+of+the+Cambridge+Fast+Ring+ECL+chip+using+HOL%2E+Technical+Report+123%2C+Computer+Laboratory%2C+University+of+Cambridge%2C+UK%2C+1988%2E)
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](https://scholar.google.com/scholar?q=Formal+Methods+in+System+Design%2C+volume+3%2C+number+1%2F2%2E+Special+issue+on+Higher+Order+Logic+Theorem+Proving+and+its+Applications%2C+August+1993%2E)
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](https://scholar.google.com/scholar?q=Formal+Methods+in+System+Design%2C+volume+5%2C+number+1%2F2%2E+Special+issue+on+Higher+Order+Logic+Theorem+Proving+and+its+Applications%2C+July%2FAugust+1993%2E)
26. The Computer Journal, volume 38, number 2. Special issue on Higher Order Logic Theorem Proving and its Applications, 1995. [find](https://scholar.google.com/scholar?q=The+Computer+Journal%2C+volume+38%2C+number+2%2E+Special+issue+on+Higher+Order+Logic+Theorem+Proving+and+its+Applications%2C+1995%2E)
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](https://scholar.google.com/scholar?q=G%2E+Birtwistle+J%2E+Joyce+and+M%2E+J%2E+C%2E+Gordon%2E+Proving+a+computer+correct+in+higher+order+logic%2E+Technical+Report+100%2C+University+of+Cambridge+Computer+Laboratory%2C+1986%2E)
28. Jeffrey J. Joyce and Carl Seger, editors. volume 780 of Lecture Notes in Computer Science, UBC, Vancouver, Canada, 1993. Springer-Verlag. [find](https://scholar.google.com/scholar?q=Jeffrey+J%2E+Joyce+and+Carl+Seger%2C+editors%2E+volume+780+of+Lecture+Notes+in+Computer+Science%2C+UBC%2C+Vancouver%2C+Canada%2C+1993%2E+Springer%2DVerlag%2E)
29. T. F. Melham. Automating recursive type definitions in higher order logic. In Birtwistle and Subrahmanyam [1], pages 341–386. [find](https://scholar.google.com/scholar?q=T%2E+F%2E+Melham%2E+Automating+recursive+type+definitions+in+higher+order+logic%2E+In+Birtwistle+and+Subrahmanyam+%5B1%5D%2C+pages+341%E2%80%93386%2E)
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](https://scholar.google.com/scholar?q=T%2E+F%2E+Melham%2E+A+package+for+inductive+relation+definitions+in+hol%2E+In+Proceedings+of+the+1991+International+Workshop+on+the+HOL+Theorem+Proving+System+and+its+Applications%2C+pages+32%E2%80%9337%2E+IEEE+Computer+)
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](https://scholar.google.com/scholar?q=T%2E+F%2E+Melham%2E+The+HOL+logic+extended+with+quantification+over+type+variables%2E+Formal+Methods+in+System+Design%2C+3%281%2F2%29%3A7%E2%80%9324%2C+August+1993%2E)
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](https://scholar.google.com/scholar?q=Thomas+F%2E+Melham+and+Juanito+Camilleri%2C+editors%2E+Higher+Order+Logic+Theorem+Proving+and+Its+Applications%3A+7th+International+Workshop%2C+LNCS+859%2E+Springer%2C+September+1994%2E)
33. G. Milne and P. A. Subrahmanyam, editors. Formal Aspects of VLSI Design. North-Holland, 1986. [find](https://scholar.google.com/scholar?q=G%2E+Milne+and+P%2E+A%2E+Subrahmanyam%2C+editors%2E+Formal+Aspects+of+VLSI+Design%2E+North%2DHolland%2C+1986%2E)
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](https://scholar.google.com/scholar?q=R%2E+Milner%2E+Logic+for+computable+functions%3B+description+of+a+machine+implementation%2E+Technical+Report+STAN%2DCS%2D72%2D288%2C+A%2EI%2E+Memo+169%2C+Stanford+University%2C+1972%2E)
35. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348–375, December 1978. [find](https://scholar.google.com/scholar?q=R%2E+Milner%2E+A+theory+of+type+polymorphism+in+programming%2E+Journal+of+Computer+and+System+Sciences%2C+17%283%29%3A348%E2%80%93375%2C+December+1978%2E)
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](https://scholar.google.com/scholar?q=R%2E+Milner+and+R%2E+Weyhrauch%2E+Proving+compiler+correctness+in+a+mechanized+logic%2E+In+Bernard+Meltzer+and+Donald+Michie%2C+editors%2C+Machine+Intelligence+7%2C+pages+51%E2%80%9370%2E+Edinburgh+University+Press%2C+1972%2E)
37. Robin Milner. Communication and Concurrency. Prentice-Hall, 1989. [find](https://scholar.google.com/scholar?q=Robin+Milner%2E+Communication+and+Concurrency%2E+Prentice%2DHall%2C+1989%2E)
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](https://scholar.google.com/scholar?q=Monica+Nesi%2E+A+formalization+of+the+process+algebra+CCS+in+higher+order+logic%2E+Technical+Report+278%2C+University+of+Cambridge%2C+Computer+Laboratory%2C+December+1992%2E)
39. L. C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983. [find](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson%2E+A+higher%2Dorder+implementation+of+rewriting%2E+Science+of+Computer+Programming%2C+3%3A119%E2%80%93149%2C+1983%2E)
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](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson%2E+Logic+and+Computation%3A+Interactive+Proof+with+Cambridge+LCF%2C+volume+2+of+Cambridge+Tracts+in+Theoretical+Computer+Science%2E+Cambridge+University+Press%2C+1987%2E)
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](https://scholar.google.com/scholar?q=L%2E+C%2E+Paulson%2E+Isabelle%3A+The+next+700+theorem+provers%2E+In+P%2E+Odifreddi%2C+editor%2C+Logic+and+Computer+Science%2C+pages+361%E2%80%93386%2E+Academic+Press%2C+1990%2E)
42. Lawrence C. Paulson. Verifying the unification algorithm in LCF. Science of Computer Programming, 5:143–170, 1985. [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson%2E+Verifying+the+unification+algorithm+in+LCF%2E+Science+of+Computer+Programming%2C+5%3A143%E2%80%93170%2C+1985%2E)
43. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828. [find](https://scholar.google.com/scholar?q=Lawrence+C%2E+Paulson%2E+Isabelle%3A+A+Generic+Theorem+Prover%2E+Springer%2C+1994%2E+LNCS+828%2E)
44. K. Petersson. A programming system for type theory. Technical Report 21, Department of Computer Science, Chalmers University, Göteborg, Sweden, 1982. [find](https://scholar.google.com/scholar?q=K%2E+Petersson%2E+A+programming+system+for+type+theory%2E+Technical+Report+21%2C+Department+of+Computer+Science%2C+Chalmers+University%2C+Go%CC%88teborg%2C+Sweden%2C+1982%2E)
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](https://scholar.google.com/scholar?q=E%2E+Thomas+Schubert%2C+Phillip+J%2E+Windley%2C+and+James+Alves%2DFoss%2C+editors%2E+Higher+Order+Logic+Theorem+Proving+and+Its+Applications+8th+International+Workshop%2C+LNCS+971%2E+Springer%2C+September+1995%2E)
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](https://scholar.google.com/scholar?q=Dana+S%2E+Scott%2E+A+type%2Dtheoretical+alternative+to+ISWIM%2C+CUCH%2C+OWHY%2E+Theoretical+Computer+Science%2C+121%3A411%E2%80%93440%2C+1993%2E+Annotated+version+of+the+1969+manuscript%2E)
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](https://scholar.google.com/scholar?q=Konrad+Slind%2E+Function+definition+in+higher+order+logic%2E+In+Theorem+Proving+in+Higher+Order+Logics%2C+9th+International+Conference%2C+TPHOLs%E2%80%9996%2C+number+1125+in+Lecture+Notes+in+Computer+Science%2C+Turku%2C+Fi)
48. Joakim von Wright, Jim Grundy, and John Harrison, editors. volume 1125 of Lecture Notes in Computer Science, Turku, Finland, 1996. Springer-Verlag. [find](https://scholar.google.com/scholar?q=Joakim+von+Wright%2C+Jim+Grundy%2C+and+John+Harrison%2C+editors%2E+volume+1125+of+Lecture+Notes+in+Computer+Science%2C+Turku%2C+Finland%2C+1996%2E+Springer%2DVerlag%2E)
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](https://scholar.google.com/scholar?q=P%2E+J%2E+Windley%2E+The+practical+verification+of+microprocessor+designs%2E+In+Proceedings+of+the+1991+International+Workshop+on+the+HOL+Theorem+Proving+System+and+its+Applications%2C+pages+32%E2%80%9337%2E+IEEE+Compute)

*Updated 3 November 2026*