Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm
作者:Alessandro Armando, Alan Smaill, Ian Green
摘要
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.
论文关键词:program synthesis, proof-planning, middle-out reasoning
论文评审过程:
论文官网地址:https://doi.org/10.1023/A:1008763422061