Sciweavers

Share
KBSE
1999
IEEE

An ML Editor Based on Proofs-As-Programs

10 years 8 months ago
An ML Editor Based on Proofs-As-Programs
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 CYNTHIA 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.
Jon Whittle, Alan Bundy, Richard J. Boulton, Helen
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where KBSE
Authors Jon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe
Comments (0)
books