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

fYear

1999

fDate

36434

Firstpage

166

Lastpage

173

Abstract

C^YNTHIA 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^YNTHIA 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^YNTHIA at present is termination. C^YNTHIA has been successfully used in the teaching of ML in two courses at Napier University, Scotland. C^YNTHIA 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; C^YNTHIA; 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;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 1999. 14th IEEE International Conference on.

Conference_Location

Cocoa Beach, FL

Print_ISBN

0-7695-0415-9

Type

conf

DOI

10.1109/ASE.1999.802196

Filename

802196