An implementation of HOL built on ML by Mike Gordon <mjcg@cl.cam.ac.uk>.
Try this search on Wikipedia, OneLook, Google
