Program synthesis from natural deduction proofs
Shigeki Goto · International Joint Conference on Artificial Intelligence · 1979
There have already been many program synthesizers which are based on classical logic. There is, however, some evidence that intuitionistic logic is more suitable for computer programs. This paper presents a program synthesis method based on intuitionistic logic. The synthesizing method is essentially an application of Godel's interpretation. An experimental program synthesizer NJL, which performs Godel's interpretation, is implemented in LISP. NJL takes natural deduction proofs as input and produces LISP programs.