Proposer:
Suggested Supervisors:
Principal goal of the project:
Description:
For his PhD project, Jon Whittle is building a "programming
by analogy" editor, called Cynthia, for ML. The user selects a
source program and edits it into the target program using a
collection of powerful editing commands. Cynthia monitors
properties of well-definedness and termination thoughout the edit
and warns the user about outstanding problems, eg ill-typed
expressions. Cynthia works by using a synthesis proof for the
source program and editing it into one for the target proof,
although the user is not aware of this. The synthesis proof works
from a weak specification, namely the target type
declaration. However, this is enough for Cynthia to be able to
check well-definedness and termination as well as syntactic
correctness. It is also the basis for some powerful editing
commands, eg major changes to the target program are made
automatically if the user changes the underlying types or the
pattern of any recursions. These editing commands can increase
user productivity as well as protect against a wide variety of
common errors. Initial evaluation on students of ML at Napier
University are very promising -- they like it.
The techniques on which Cynthia is based are not restricted to
ML -- or even to functional languages. In principle, they could
be applied to any typed language. It would be interesting to
adapt Cynthia to a logic programming language. Unfortunately,
Prolog is untyped, so is not immediately suitable. Godel is a
typed logic programming language, so is a candidate.
Geraint Wiggins built a proof editor, Whelk, for a logic
specifically designed to support proofs of the synthesis of
Prolog and Godel programs. This would be a good basis for the
project.
Resources Required:
Degree of Difficulty:
Background Needed:
References: