H ? « ‹ ← → › »

Language peer sets for HOL:
United Kingdom↑
United Kingdom/1985↑
Designed 1985 ↑
1980s languages ↑
Fifth generation↑
Late Cold War↑

HOL(ID:1150/hol001)

Higher Order Logic 

alternate simple view
Country: United Kingdom
Designed 1985
Published: 1985

Higher Order Logic. A proof-generating system for higher order logic based on LCF.

HOL-88 written in ML, HOL-90 written in SML/NJ
Related languages
Cambridge LCF → HOL   Based on
HOL → HOL-88   Implementation
HOL → HOLCF   Evolution of
HOL → Isabelle/HOL   Derivation of
References:
  • Gordon, M.J.C. (1985) Gordon, M.J.C. "HOL: A Machine Oriented Formulation of Higher Order Logic", Report 68, Comp Lab U Cambridge (1985).
  • Gordon, M.J.C. et al, (1993) Gordon, M.J.C. et al, "Introduction to HOL", Cambridge U Press 1993 ISBN 0-521-441897
  • Wiedijk, Freek (1998) Wiedijk, Freek "The Fifteen Provers of the World" Abstract
  • Gordon M.J.C. (1999) Gordon M.J.C. "From LCF to HOL: A Short History" in Plotkin, Stirling and Tofte (eds) Proof, Language, and Interaction: Essays in the Honor of Robin Milner Abstract
    Resources
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder