Computer facilities for Isabelle data handling

M. A. Kramer, W. A. Love, Richard J. Miller, M. Zeller · 1977

The analysis of data produced by Isabelle experiments will need a large system of computers. Included in the array should be a substantial computer system at each Isabelle intersection in use. These systems must include enough computer power to keep experimenters aware of the status of the experiment. This will require at least one very fast sophisticated processor in the system, the size depending on the experiment. Other features of the intersection systems must be a good, high speed graphic display, ability to record data on magnetic tape at 500 to 1000 KB, and a high-speed link to a central computer. The operating system software must support multiple interactive users. A substantially larger capacity computer system, shared by the six intersection region experiments, must be available with good turnaround for experimenters while Isabelle is running. The computer mainframes should ideally be compatible members of the same family of computers. A very large computation load will be generated by the post experiment data reduction. Much of this may have to be run at lower priority. A computer support group will be required to maintain the computer system and to provide and maintain software common to all experiments. Such software support may include providing a compatible compiler. Special superfast computing hardware or special function processors constructed with microprocessor circuitry may be necessary both in the data gathering and data processing work. Thus, both the local and central processors should be chosen with the possibility of interfacing such devices in mind.

Read the paper · More papers on PaperTik