kirancodes.me
To Proof Maintenance & Beyond!
ASE 1999

An ML Editor Based on Proofs-As-Programs

Jon Whittle, Alan Bundy, Richard J. Boulton, Helen Lowe

PDFDOI 10.1109/ase.1999.802196dblp

Abstract

C/sup Y/NTHIA 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/sup Y/NTHIA 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/sup Y/NTHIA at present is termination. C/sup Y/NTHIA has been successfully used in the teaching of ML in two courses at Napier University, Scotland. C/sup Y/NTHIA is a convincing, real-world application of the proofs-as-programs idea.

BibTeX
@inproceedings{Whittle-al:ASE99,
  author    = {Jon Whittle and
               Alan Bundy and
               Richard J. Boulton and
               Helen Lowe},
  title     = {An {ML} Editor Based on {Proofs-As-Programs}},
  booktitle = {ASE},
  pages     = {166--173},
  publisher = {{IEEE} Computer Society},
  year      = {1999},
}

Related papers