Automatic synthesis of recursive programs: The proof-planning paradigm

Alessandro Armando, Alan Smaill, Ian Green

Research output: Contribution to journalArticlepeer-review


We describe a proof method that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This method provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This method makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate it with parts of a substantial example—the synthesis of a unification algorithm
Original languageEnglish
Pages (from-to)329-356
Number of pages28
JournalAutomated Software Engineering
Issue number4
Publication statusPublished - 1999


Dive into the research topics of 'Automatic synthesis of recursive programs: The proof-planning paradigm'. Together they form a unique fingerprint.

Cite this