HOL (proof Assistant) - Members

Members

There are four HOL systems (sharing essentially the same logic) that are still maintained and developed.

  • The first, HOL4 stems from the HOL88 system, which was the culmination of the original HOL implementation effort, led by Mike Gordon. HOL88 included its own ML implementation, which was in turn implemented on top of Common Lisp. The implementations following HOL88 (HOL90, hol98 and HOL4) all used Standard ML as the implementation language. The hol98 system is tied to the Moscow ML implementation of Standard ML; HOL4 can be built with either Moscow ML or Poly/ML. Of these four systems, only HOL4 is being maintained and developed. All come with large libraries of theorem proving code. These implement extra automation on top of the very simple core code. HOL4 is BSD licensed.
  • The second current implementation is HOL Light. This started as an experimental "minimalist" version of HOL. Although it has subsequently grown into another mainstream HOL variant, its logical foundations remain unusually simple. HOL Light used to be implemented in Caml Light, but now uses OCaml. HOL Light is available under the new BSD license.
  • The third current implementation is ProofPower a collection of tools designed to provide special support for working with the Z notation for formal specification. 5 of the 6 tools are GNU GPL v2 licensed. The sixth (PPDaz) has a proprietary license.
  • The fourth is HOL Zero, a minimalist implementation focused on trustworthiness. HOL Zero is GNU GPL 3+ licensed

HOL is a predecessor of Isabelle.

Read more about this topic:  HOL (proof Assistant)

Famous quotes containing the word members:

    “The state of society is one in which the members have suffered amputation from the trunk, and strut about so many walking monsters,—a good finger, a neck, a stomach, an elbow, but never a man.”
    —Ralph Waldo Emerson (1803–1882)

    “A multitude of little superfluous precautions engender here a population of deputies and sub-officials, each of whom acquits himself with an air of importance and a rigorous precision, which seemed to say, though everything is done with much silence, “Make way, I am one of the members of the grand machine of state.””
    —Marquis De Custine (1790–1857)

    “The damned are in the abyss of Hell, as within a woeful city, where they suffer unspeakable torments, in all their senses and members, because as they have employed all their senses and their members in sinning, so shall they suffer in each of them the punishment due to sin.”
    —St. Francis De Sales (1567–1622)