Title :
An ML editor based on proofs-as-programs
Author :
Whittle, Jon ; Bundy, Alan ; Boulton, Richard ; Lowe, Helen
Author_Institution :
Recom Technol., NASA Ames Res. Center, Moffett Field, CA, USA
Abstract :
CYNTHIA 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 CYNTHIA 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 CY NTHIA at present is termination. CYNTHIA has been successfully used in the teaching of ML in two courses at Napier University, Scotland. CYNTHIA is a convincing, real-world application of the proofs-as-programs idea
Keywords :
ML language; computer science education; formal specification; functional programming; program diagnostics; text editing; utility programs; CYNTHIA; ML editor; Napier University; error feedback; function definition; functional programming language; high-level editing command sequences; program analysis; program editing; program extraction; programming courses; proof representation; proofs-as-programs; specification proofs; teaching; termination; Computer languages; Debugging; Error correction; Feedback; Functional programming; Informatics; NASA; Program processors; Programming environments; Read only memory;
Conference_Titel :
Automated Software Engineering, 1999. 14th IEEE International Conference on.
Conference_Location :
Cocoa Beach, FL
Print_ISBN :
0-7695-0415-9
DOI :
10.1109/ASE.1999.802196
