My research and investigations

HOL4 and Moscow ML

Downloaded and installed Moscow ML. Able to start Moscow ML interactive mode.

Also downloaded and built HOL4, the theorem-prover running on top of Moscow ML. Very interesting.

The HOL4 documents, prepared by Micheal and Konrad, are excellent. Writing docos for an evolving system is always a challenge, but these materials are essential for newbies like me.


Comments on: "HOL4 and Moscow ML" (1)

  1. Michael Norrish said:

    I recommend using emacs to run HOL4, particularly if you are on Windows, because it will then be able to display the Unicode characters more nicely. (I can’t figure out how to get the standard shell to do UTF-8.)

    Alternatively, you may have to turn Unicode off, with the command set_trace "Unicode" 0;

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: