This file contains Imps Update announcements -- in reverse chronological order Date: Thu, 15 May 1997 16:17:42 -0400 (EDT) From: "William M. Farmer" To: imps@linus.mitre.org, parnas@qusunt.crl.McMaster.CA, clt@sail.stanford.edu, mumford@abel.math.harvard.edu Return-Receipt-To: farmer Subject: Release of IMPS 2.0 CC: farmer@linus.mitre.org, guttman@linus.mitre.org, jt@linus.mitre.org Content-Type: text Content-Length: 3699 We are pleased to announce the release of IMPS 2.0, a new version of IMPS written in Common Lisp that runs on Unix platforms. IMPS 2.0 should work with most versions of Common Lisp; we support Allegro CL, CLISP, CMU Common Lisp, and GCL. We have successfully run IMPS 2.0 with these versions of Common Lisp on SunOS, Sun Solaris, and Linux. IMPS 2.0 runs under the X Window System and has a new XEmacs interface. The older IMPS 1.2 is written in the T programming language and runs only on Sun 4 SPARCstations. IMPS 2.0 was created by Javier Thayer Fabrega by producing an emulation of the T programming language in Common Lisp. IMPS 1.2 is no longer being developed or supported. Converting from IMPS 1.2 to IMPS 2.0 should be easy in most cases because the IMPS Main Theory Library is exactly the same for both IMPS 1.2 and IMPS 2.0. A brief description of IMPS 2.0 and details for obtaining IMPS 2.0 are given below. William M. Farmer The MITRE Corporation Joshua D. Guttman 202 Burlington Road F. Javier Thayer Fabrega Bedford, MA 01730-1420 USA =========================================================================== IMPS 2.0 A. What IMPS Is IMPS is an Interactive Mathematical Proof System developed by W. M. Farmer, J. D. Guttman, and F. J. Thayer Fabrega at The MITRE Corporation. It is intended to provide organizational and computational support for traditional mathematical techniques and styles of practice. The system consists of a library of mathematics (represented as a network of axiomatic theories linked by theory interpretations) and a collection of tools for exploring, applying, extending, and communicating the mathematics in the library. The IMPS system is available without fee via anonymous ftp (under the terms of a public license) at math.harvard.edu. IMPS 2.0, which is written in Common Lisp, runs on Unix platforms with at least 16 or more MB physical memory. It runs under the X Window System and has an Emacs-based interface. (The older IMPS 1.2, which is written in the T programming language, runs only on Sun 4 SPARCstations and is now considered to be obsolete.) B. IMPS WWW Home Page There is a World Wide Web home page for IMPS at ftp://math.harvard.edu/imps/imps_html/imps.html It includes links to a hypertext presentation of the IMPS Main Theory Library. The presentation allows one to explore the definitions, theorems, proofs, theories, interpretations, etc. in the Main Theory Library by going, for example, from the name of a constant used in a proof to the constant's definition or from the proof of a theorem to the specification of the theory in which the theorem was proved. C. How to Get IMPS via the IMPS WWW Home Page Connect to the IMPS home page and select "How to Get IMPS". D. How to Get IMPS via FTP Ftp to math.harvard.edu as anonymous and cd to the directory named "imps". This directory will contain a directory named "doc" and several files. "README" is a file explaining how to install IMPS, report bugs, etc. "imps-2.0.tar.gz" is a compressed tar file of the IMPS system. And "public-license" contains the license for using IMPS. To get a copy of the IMPS system, type binary get README get imps-2.0.tar.gz The directory "doc" contains several papers on IMPS in compressed LaTeX dvi including the IMPS manual and a full IMPS bibliography. E. IMPS Mailing List To subscribe to the IMPS Mailing List, send your name and e-mail address to imps-request@linus.mitre.org We strongly urge that all users of IMPS subscribe to the IMPS Mailing List. F. Questions Please send questions by e-mail to imps-request@linus.mitre.org. From: "William M. Farmer" Date: Thu, 2 May 1996 16:07:26 -0400 To: imps@linus.mitre.org Return-Receipt-To: farmer@linus.mitre.org Subject: IMPS ftp site is up and running Content-Type: text Content-Length: 225 The IMPS ftp site and Web page have been reactivated. As before, the address of the ftp site is math.harvard.edu and the URL of the Web page is file://math.harvard.edu/imps/imps_html/imps.html . William M. Farmer From: "William M. Farmer" Date: Thu, 4 Apr 1996 12:55:50 -0500 To: imps@linus.mitre.org Return-Receipt-To: farmer@linus.mitre.org Subject: IMPS ftp site is disabled Content-Type: text Content-Length: 748 The Harvard math department ftp server, where the IMPS Web page and ftp site are located, has recently been disabled. (The Harvard site was being used by a horde of "net-surfing adolescent hooligans" for storing and trading their own files.) We are not sure when it will be up and running again. In the mean time, if anyone would like to obtain a copy of the IMPS system, we would be happy to ftp it directly to a local ftp site. William Farmer The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420 USA farmer@mitre.org Joshua Guttman The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420 USA guttman@mitre.org Javier Thayer Fabrega Mitretek Systems, 25 Burlington Mall Road, Burlington, MA 01803 USA jt@mitre.org From: "William M. Farmer" Date: Wed, 12 Apr 1995 17:03:21 -0400 To: imps@linus.mitre.org Return-Receipt-To: farmer@linus.mitre.org Subject: New IMPS papers The following papers (in compressed dvi format) have been added to the imps/doc directory at math.harvard.edu: 1. W. M. Farmer "A general method for safely overwriting theories in mechanized mathematics systems" 2. W. M. Farmer, J. D. Guttman, F. J. Thayer F\'abrega "Contexts in mathematical reasoning and computation" 3. W. M. Farmer, J. D. Guttman, F. J. Thayer F\'abrega "The IMPS bibliography" 4. W. M. Farmer, F. J. Thayer F\'abrega "Formal numerical program analysis" 5. F. J. Thayer F\'abrega "An approach to process algebra using IMPS" William Farmer The MITRE Corporation Joshua Guttman 202 Burlington Road Javier Thayer F\'abrega Bedford, MA 01730-1420 USA ============================================================================== From: "William M. Farmer" Date: Tue, 19 Jul 1994 16:22:30 -0400 To: imps@linus.mitre.org Return-Receipt-To: farmer@linus.mitre.org Subject: New Version of IMPS A new version of IMPS (Version 1.2) is now available via anonymous ftp at math.harvard.edu. Version 1.2 differs from Version 1.1 in the following ways: 1. A bug in the Extensionality primitive inference procedure has been corrected. 2. A bug in the implementation of the def-bnf form has been corrected. 3. Some new material has been added to the IMPS initial theory library. 4. A large number of minor modifications and additions have been made to the logical and deductive machinery, the user interface, and the manual. William Farmer The MITRE Corporation Joshua Guttman 202 Burlington Road, A118 Javier Thayer Bedford, MA 01730-1420 USA ============================================================================== From: "William M. Farmer" Date: Tue, 12 Apr 1994 11:19:59 -0400 To: imps@linus.mitre.org Return-Receipt-To: farmer@linus.mitre.org Subject: New version of IMPS; new IMPS papers A. New Version of IMPS A new version of IMPS is now available via anonymous ftp at math.harvard.edu. The new version corrects a bug in the mechanism for backchaining which caused bound variables to be sometimes incorrectly renamed. The backchaining mechanism is used by the 3 backchain and 3 simplification primitive inferences. In some fairly rare situations the bug could lead to an unsound inference. The bug fix -- which changes some variable names -- caused a handful of the 1100 proof scripts in the theory library to fail. All of these proof scripts were easily fixed. We discovered no false theorems that were proved by means of the an unsound inference caused by the bug. B. New IMPS Papers The following three papers (in both dvi and ps formats) have been added to the imps/doc directory at math.harvard.edu: 1. W. M. Farmer "Interpretations in simple type theory" 2. W. M. Farmer, J. D. Guttman, M. E. Nadel, F. J. Thayer "Proof script pragmatics in IMPS" 3. J. D. Guttman "A simple virtual memory scheme formalized in IMPS" William Farmer The MITRE Corporation Joshua Guttman 202 Burlington Road, A118 Javier Thayer Bedford, MA 01730-1420 USA ============================================================================== Return-Path: From: "William M. Farmer" Date: Fri, 10 Dec 1993 16:22:48 -0500 To: imps@linus.mitre.org Return-Receipt-To: farmer@linus.mitre.org Subject: IMPS Version 1.1 A new version of IMPS (Version 1.1) is now available via anonymous ftp at math.harvard.edu. Version 1.1 differs from Version 1.0 in the following ways: 1. Free Software Foundation GNU Emacs 19 is now supported (see the README file at math.harvard.edu). The current support for GNU Emacs 18 and Lucid GNU Emacs 19 will be preserved, but future improvements to the user interface will only be made for Free Software Foundation GNU Emacs 19. 2. The IMPS User's Manual has been updated and extended. 3. There is new machinery for working with theory library files and proof scripts. 4. Several minor bugs have been corrected. 5. A few additions have been made to the IMPS initial theory library. Please mail information about bugs or problems with using IMPS to imps-bugs@linus.mitre.org Other questions can be mailed to imps-request@linus.mitre.org To send a message to all the members of the Mailing List, use the address imps@linus.mitre.org William Farmer The MITRE Corporation Joshua Guttman 202 Burlington Road, A118 Javier Thayer Bedford, MA 01730-1420 USA