Interactive Theorem-Proving
Occasional thoughts and updates about the world of interactive theorem-proving.
20 November 2012
Piotr Rudnicki has died
26 October 2012
And we're now using git, btw
Latest HOL4 released
The release notes are available there. There’s nothing hugely dramatic, but there are annoying bugs fixed, and some nice new examples to look at too.
Maybe the next release will be the dramatic change that will justify adoption of a new lake moniker...
26 January 2011
ITP 2011
Note the important paper submission details! (Abstracts due 13 February; full papers a week after that.)
23 March 2010
Robin Milner has died
...Robin Milner died on Saturday 20th March, in Cambridge, just three days after the funeral of his wife, Lucy.
There may well be notices at Cambridge and Edinburgh in due course.
See the Wikipedia page for more on his career. From the ITP perspective, he is famous for his work on the influential LCF system.
25 February 2010
Online Prover Repositories
Most, if not all, of the interactive theorem-proving systems used today are open source, meaning that their source-code is freely available. Not only can you read the source code yourself, but you can also write your own systems based on that code if you wish. In addition, some make their development repositories available for browsing. John Harrison recently announced that HOL Light now has its Subversion repository being hosted on Google Code, so I thought I’d provide links to those systems' repositories I know of.
Coq is on Subversion, at INRIA, at
svn://scm.gforge.inria.fr/svn/coq/
HOL4 is on Subversion, at Sourceforge, at
https://hol.svn.sourceforge.net/svnroot/hol/HOL
HOL4’s repository is also available via git, at github, at
git://github.com/mn200/HOL.git
HOL Light is on Subversion, at Google Code, at
http://hol-light.googlecode.com/svn/trunk/
-
Isabelle is on Mercurial, at Munich, at
http://isabelle.in.tum.de/repos/isabelle
Note that all of those URLs above are for use by the respective version-control systems’ initialisation and cloning commands; they will not necessarily work as targets for web-browsers.