Edinburgh Research Explorer

An ML Editor based on Proofs-as-Programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Documents

http://ase-conferences.org/ase/past/ase99/
Original languageEnglish
Title of host publicationAutomated Software Engineering, 1999. 14th IEEE International Conference on.
Pages166 - 173
DOIs
StatePublished - Oct 1999
EventAutomated Software Engineering, 1999. 14th IEEE International Conference on. - Cocoa Beach, FL, United States
Duration: 12 Oct 199915 Oct 1999

Conference

ConferenceAutomated Software Engineering, 1999. 14th IEEE International Conference on.
CountryUnited States
CityCocoa Beach, FL
Period12/10/9915/10/99

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

Event

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

12/10/9915/10/99

Cocoa Beach, FL, United States

Event: Conference

Download statistics

No data available

ID: 6321673