An ML editor based on proofs-as-programs

Abstract

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.