Selected Papers of Dana S. Scott

Convert variable-pitch fonts to monospace (useful for unicode and indentation-friendly programming)

Network Semantics

Webpages for the HOL4 website (currently at hol-theorem-prover.org)

a quick cursor jump mode for emacs

Theory of Context-Free Languages in HOL

a quick cursor jump mode for emacs

My C++ in HOL semantics

JSON parsing in SML (from SML/NJ's svn repo)

Password Gorilla manages passwords

Mechanization of "Unification in Linear Time and Space: A Structured Presentation" by Martelli and Montanari in HOL4.

Password Gorilla manages passwords

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

Moscow ML is a light-weight implementation of Standard ML (SML), a strict functional language widely used in teaching and research.