@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ NAME: M E R I L L KEYWORDS: An Equational Reasoning System in Standard ML. ============================================== Brian Matthews, Dept of Computing Science, The University of Glasgow & Rutherford Appleton Laboratory. A preliminary version of MERILL is now available via anonymous ftp from the University of Glasgow. This system written in Standard ML, is a general purpose order-sorted equational reasoning system which: * Allows the user to declare their own object language. * Allows AC-rewriting and AC-unification of terms and equations. * Has several completion algorithms. * Is built on a hierarchy of types, known as Order-Sorting. This allows greater expressive is defining partial functions and error handling and also efficiency of rewriting. * Allows the user to try different termination methods. The system currently has a menu driven teletype interface. Future plans with this system include: extending the order-sorted paradigm to allow greater flexibility through a system of dynamic sorts; adding a tactic language to allow the user to set up and run equational reasoning tasks; the extension for more and more powerful termination methods; building a window based user-interface, using X-windows, to allow a greater ease of use of the system. A user manual in LaTeX dvi format is included in the release. This release is an early one, and I expect that there will be many errors! Please be patient with the system and please report to me if there are any errors, or suggestions for improving the design. Obtaining the system. --------------------- The system is available via anonymous ftp from the University of Glasgow, ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50) Sample session: $ ftp ftp.dcs.glasgow.ac.uk Connected to vanuata.dcs.glasgow.ac.uk. 220 vanuata FTP server (Version 6.12 Tue Oct 6 13:34:12 BST 1992) ready. Name (ftp.dcs.glasgow.ac.uk:bmm): anonymous 331 Guest login ok, send e-mail address as password. Password: 230 Guest login ok, access restrictions apply. ftp> cd pub/merill 250 CWD command successful. ftp> binary 200 Type set to I. ftp> get src.tar.Z 200 PORT command successful. 150 Opening BINARY mode data connection for src.tar.Z (288271 bytes). 226 Transfer complete. local: src.tar.Z remote: src.tar.Z 288271 bytes received in 25 seconds (11 Kbytes/s) ftp> close 221 Goodbye. ftp> quit $ Contact: Brian Matthews Dept of Computing Science Systems Engineering University of Glasgow Rutherford Appleton Laboratory Glasgow Chilton G12 8QQ Didcot Scotland, OXON OX11 0QX U.K. U.K. brian@dcs.glasgow.ac.uk bmm@inf.rl.ac.uk [Info source, date ] Brian Matthews, August 1995 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%