Proofs-as-programs as a framework for the design of an analogy-based ML editor

Jon Whittle, Alan Bundy, Richard Boulton

Research output: Contribution to journalArticleResearchpeer-review

2 Citations (Scopus)


CYNTHIA is a transformation-based editor for a functional subset of ML that lies somewhere between a structure editor and a framework for formal program development. Users construct programs from existing code by applying editing commands that make a semantic analysis of the program's behaviour, e.g., whether it is terminating. All analysis is done using the Oyster system, which is an implementation of proofs-as-programs. We concentrate on identifying analyses that can be done fully automatically (e.g., using a decision procedure) and hence can be hidden from the user. As a result, CYNTHIA represents progress towards a goal of program editors that make an intelligent analysis of their code, but in a way that requires no extra input from the programmer.

Original languageEnglish
Pages (from-to)403-421
Number of pages19
JournalFormal Aspects of Computing
Issue number3-5
Publication statusPublished - 1 Dec 2002
Externally publishedYes


  • Functional programming
  • Programming environments
  • Theorem proving

Cite this