Automatic program generation using sequent calculus
Talal Hamza Maghrabi, Forouzan Golshani · 1992
Program development can be made amenable to formal methods by using a logical framework. A logic specification, whose operational semantics is based on proof theory, provides an abstract and “implementation independent” definition of the problem, the data domains and the associated operators.