tag:blogger.com,1999:blog-6607274989708559262024-03-14T02:44:26.576+11:00Interactive Theorem-ProvingOccasional thoughts and updates about the world of interactive theorem-proving. Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-660727498970855926.post-92122944738036898812012-11-20T11:12:00.001+11:002012-11-20T11:12:43.878+11:00Piotr Rudnicki has diedPiotr Rudnicki, a developer and proponent of the influential Mizar system, died on 17 November, aged 61.Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-43859317202792472232012-10-26T14:59:00.000+11:002012-10-26T14:59:10.794+11:00And we're now using git, btwThat latest release of HOL4 was built from our git repository at <a href="http://github.com/mn200/HOL.git"><span style="font-family: "Courier New",Courier,monospace;">github</span></a>. Working with git has been a real pleasure, and the github issue-tracker has wormed its way into our workflow as well. The <a href="http://hol.sourceforge.net/">sourceforge page</a> is still our public face.Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-16193586162360936402012-10-26T14:54:00.001+11:002012-10-26T14:54:10.734+11:00Latest HOL4 releasedHOL4’s latest version (Kananaskis-8) has been released. You can <a href="http://hol.sourceforge.net/">get it from Sourceforge</a>.<br />
<br />
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.<br />
<br />
Maybe the next release will be the dramatic change that will justify adoption of a new lake moniker...Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-57091004657996505242011-01-26T16:03:00.003+11:002011-01-26T16:06:37.568+11:00ITP 2011The next iteration of the interactive theorem-proving conference, ITP 2011, is in Nijmegen this year. See all the details at <a href="http://itp2011.cs.ru.nl/ITP2011/Home.html">the official web-page</a>.
<p>Note the important paper submission details! (Abstracts due 13 February; full papers a week after that.)Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-2705114691265527422010-03-23T09:07:00.003+11:002010-03-23T09:13:20.111+11:00Robin Milner has died<blockquote><p><q>...Robin Milner died on Saturday 20th March, in Cambridge, just three days after the funeral of his wife, Lucy.</q></blockquote>
<p>There may well be notices at Cambridge and Edinburgh in due course.
<p> See the <a href="http://en.wikipedia.org/wiki/Robin_Milner">Wikipedia page</a> for more on his career. From the ITP perspective, he is famous for his work on the influential LCF system.Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-70893451022564501192010-02-25T09:48:00.007+11:002010-02-25T10:13:54.374+11:00Online Prover Repositories<p>Most, if not all, of the interactive theorem-proving systems used today are <i>open source</i>, 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 <a href="http://www.cl.cam.ac.uk/users/jrh/hol-light/">HOL Light</a> now has its Subversion repository being hosted on Google Code, so I thought I’d provide links to those systems' repositories I know of.
</p><ul>
<li><p>Coq is on <a href="http://subversion.tigris.org/">Subversion</a>, at INRIA, at <code>svn://scm.gforge.inria.fr/svn/coq/</code>
</p></li><li><p>HOL4 is on Subversion, at Sourceforge, at <code>https://hol.svn.sourceforge.net/svnroot/hol/HOL</code>
<p>HOL4’s repository is also available <i>via</i> <a href="http://git-scm.com/">git</a>, at github, at <code>git://github.com/mn200/HOL.git</code></li>
<li><p>HOL Light is on Subversion, at Google Code, at <code>http://hol-light.googlecode.com/svn/trunk/</code>
</li><li> <p>Isabelle is on <a href="http://mercurial.selenic.com/">Mercurial</a>, at Munich, at <code>http://isabelle.in.tum.de/repos/isabelle</code>
</li></ul>
<p>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.</p>Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-55137172119649983442010-01-13T10:34:00.003+11:002010-01-13T10:35:40.975+11:00Call for Papers for ITP 2010There is a <a href="http://www.floc-conference.org/ITP-cfp.html">call for papers up now on the FLoC website</a>. The deadline for abstracts is 15 January. So get to it!Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com0tag:blogger.com,1999:blog-660727498970855926.post-85481461561343816942008-09-17T14:54:00.005+10:002008-09-17T15:05:42.362+10:00The conference of the same nameInteractive Theorem-Proving is not just the name of this web-log, but is also the name of a conference due to happen in 2010 as part of the <a href="http://homepages.inf.ed.ac.uk/bklin/FLoC2010/index.html">Federated Logic Conference (FLoC)</a> in Edinburgh. ITP will also continue as a separate conference subsequently.Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.comtag:blogger.com,1999:blog-660727498970855926.post-21361586661474237702008-09-16T10:23:00.000+10:002008-09-16T10:24:47.045+10:00Ex nihiloI’ve created this blog so as to give myself an OpenID. But I suppose it’s just possible I’ll become seduced by the whole interface and use it for more than just that.Anonymoushttp://www.blogger.com/profile/15513544237890974926noreply@blogger.com