---
title: "Program Synthesis from Natural Deduction Proofs"
authors:
  - "Shigeki Goto"
doi: ""
url: "https://ijcai.org/proceedings/1979/74"
pdf: "https://ijcai.org/proceedings/1979/0074.pdf"
venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence"
year: 1979
pages: ""
track: ""
keywords:
---

# Program Synthesis from Natural Deduction Proofs

Shigeki Goto

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

## Abstract

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 ~del's interpretation. An experimental program synthesizer NJL, which performs ~del's interpretation, is implemented in LISP. NJL takes natural deduction proofs as input and produces LISP programs.