From rda@lemma-one.com Thu Oct 31 17:38:37 2002 Date: Thu, 31 Oct 2002 13:31:44 +0000 From: Rob Arthan To: czt-project@comlab.ox.ac.uk Subject: CZT: OpenProofPower Dear All, The following announcement may be of interest to members of the CZT list. Regards, Rob. ---------- Forwarded Message ---------- Subject: OpenProofPower Date: Wed, 30 Oct 2002 15:18:56 +0000 From: Rob Arthan To: info-hol@ultimate.cs.byu.edu I am pleased to announce that the ProofPower tools for specification and proof in HOL and Z are now freely available as open-source software under the GNU General Public License. For more information see: http://www.lemma-one.com/ProofPower/index/index.html If you just want to dive straight in and get the code, it's at: http://www.lemma-one.com/ProofPower/getting/OpenProofPower-2.6.1.tgz ProofPower (once known as ICL HOL) is mainly written in Standard ML and ANSI C. It includes the following five packages: PPDev - The ProofPower developer kit, mainly comprising SLRP, a simple light-weight table-driven parser generator for Standard ML. PPTex - An interface to TeX and LaTeX. See http://www.lemma-one.com/ProofPower/specs/specs.html for examples of the kind of documents it produces. PPXpp - An X Windows/Motif front-end that lets you work with proper mathematical symbols on the screen rather than ASCII mnemonics. PPHol - The HOL specification and proof development system. The ProofPower dialect of HOL has the same abstract logical system as HOL 4, HOL light and other descendants of Mike Gordon's Classic HOL. It supports a Z-like syntax so you can write specifications that look like mathematics rather than code. PPZed - The Z specification and proof development system. ProofPower-Z is semantically quite close to the new Z standard. The Z toolkit supplied includes a theory of real numbers. We build and test ProofPower on Linux PCs and on Sun Solaris Sparcs using either Poly/ML or Standard ML of New Jersey. There's some chance of getting it to run on other UNIX or UNIX-like systems for which a suitable Standard ML compiler is available. If you have any feedback on ProofPower or if you're interested in contributing to its development, please get in touch. Rob Arthan (rda@lemma-one.com) ------------------------------------------------------- ----------------------------------------------------------------------- This message is sent to the czt-project mailing list. To join, send an email to czt-project-request@comlab.ox.ac.uk containing the single line subscribe To unsubscribe, do the same, changing the message appropriately. To send a message to the list, write to czt-project@comlab.ox.ac.uk. The CZT home page is at: http://web.comlab.ox.ac.uk/oucl/work/andrew.martin/CZT/ -----------------------------------------------------------------------