/ download

Download Horton

The sources for the version of Horton written in Java are maintained in Subversion. If you have a subversion client, you can check out the latest Horton sources by doing, for example,

$ svn co svn://svn.synchrona.org/erights/horton/horton/trunk horton

This Horton depends on Joe-E and the Waterken ref_send library. (The ref_send download includes the Joe-E libraries we need.) Horton should be compatible with the Waterken web server, and successfully operate in a distributed fashion, but we have not yet tested this.

Horton itself and the ref_send library all pass the Joe-E verifier, and so are in the object-capability-safe subset of Java.

The included Horton test case depends on Sash, a simple powerbox written in unsafe Java, in order to provide initial authorities to a Joe-E/Sash plugin. The Horton test is written as a Joe-E/Sash plugin. You can get the latest Sash by doing

$ svn co svn://svn.synchrona.org/erights/joe-e/sash/trunk sash

With the TortoiseSVN client, you can simply click on the svn: links above to check out these source trees.

A zip of a snapshot of the Horton and Sash sources no older than May 15. 2007 can be found at horton.zip.

A tutorial presentation by successive refinement of Horton in E can be found here.

The Horton paper in PDF.

Obtain the current LaTeX sources for the Horton paper by doing

$ svn co svn://svn.synchrona.org/erights/horton/horton-paper horton-paper

or download a snapshot no older than May 15, 2007 from horton-paper.zip.