Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

The Caml Hump: HOL-light

HOL-light

HOL Light is a computer program to help users prove interesting mathematical theorems completely formally in higher order logic. It sets a very exacting standard of correctness, but provides a number of automated tools and pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and real analysis) to save the user work. It is also fully programmable, so users can extend it with new theorems and inference rules without compromising its soundness.
Homepage ]
Author:John Harrison.
Last modification date:22-May-2006
Version:2.20
Development status:Stable
Kind: Applications written in Caml :: Scientific software
License: Public Domain
Topic: Science :: Maths and Logic
Homepage:http://www.cl.cam.ac.uk/users/jrh/hol-light/