Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #939 | |
|---|---|
| Title: | An ML Editor Based on Proofs-as-Programs |
| Authors: | Whittle,JN; Bundy,A; Boulton,R; Lowe,H |
| Date: | Jan 1999 |
| Presented: | Submitted to the 16th conference on Automated Deduction |
| Keywords: | |
| Abstract: | CYNTHIA is a novel editor for the functional programming language ML in which early function definition is represented as the proof of a smiple 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 o9f 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. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}