Abstract. C Y NTHIA is a transformation-based editor for a functional subset of ML that lies somewhere between a structure editor and a framework for formal program development. Users construct programs from existing code by applying editing commands that make a semantic analysis of the program's behaviour, e.g., whether it is terminating. All analysis is done using the Oyster system, which is an implementation of proofs-as-programs. We concentrate on identifying analyses that can be done fully automatically (e.g., using a decision procedure) and hence can be hidden from the user. As a result, C Y NTHIA represents progress towards a goal of program editors that make an intelligent analysis of their code, but in a way that requires no extra input from the programmer.

C/sup Y/NTHIA is a novel editor for the functional programming language ML in which each function definition is represented as the proof of a simple specification. Users of C/sup Y/NTHIA edit programs by applying sequences of high-level editing commands to existing programs. These commands make changes to the proof representation from which a new program is then extracted. The use of proofs is a sound framework for analysing ML programs and giving useful feedback about errors. Amongst the properties analysed within C/sup Y/NTHIA at present is termination. C/sup Y/NTHIA has been successfully used in the teaching of ML in two courses at Napier University, Scotland. C/sup Y/NTHIA is a convincing, real-world application of the proofs-as-programs idea.

The LCF system was the first mechanical theorem prover to be user-programmable via a metalanguage, ML, from which the functional programming language Standard ML has been developed. Paulson has demonstrated how a modular rewriting engine can be implemented in LCF. This provides both clarity and flexibility. This paper shows that the same modular approach (using higher-order functions) allows transparent optimisation of the rewriting engine; performance can be improved while few, if any, changes are required to code written using these functions. The techniques described have been implemented in the HOL system, a descendant of LCF, and some are now in daily use. Comparative results are given. Some of the techniques described, in particular ones to avoid processing parts of a data structure that do not need to be changed, may be of more general use in functional programming and beyond.