---
title: "Towards a Mathematical Theory of Program Synthesis"
authors:
  - "Masahiko Sato"
doi: ""
url: "https://ijcai.org/proceedings/1979/166"
pdf: "https://ijcai.org/proceedings/1979/0166.pdf"
venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence"
year: 1979
pages: ""
track: ""
keywords:
---

# Towards a Mathematical Theory of Program Synthesis

Masahiko Sato

*Proceedings of the Sixth International Joint Conference on Artificial Intelligence*.

## Abstract

This paper attempts to set a theoretical foundation for Program Synthesis. A programming language Prog is introduced together with its interpretation in the semantic domain D. A formal system QFT, which is an extension of the Heyting arithmetic, is then introduced in order to express specifications formally. Roughly stated, the main result is: Given a QFT-proof of the specification ~x~zA[x,z], it is possible to construct a program p such that A[x,p[x]] is true in D for any input x. Moreover, a formal proof of ~xA[x,p[x]] can also be obtained. Since any program p in Prog always terminates, the above result establishes the total correctness of the synthesized program at the same time. Finally, it is shown that any program p in Prog can be faithfully simulated by means of LISP.