Program synthesis through Gödel's interpretation

Shigeki Goto

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of Gödel's interpretation which is also called Dialectica interpretation. By the use of Gödel's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.

Original languageEnglish
Title of host publicationMathematical Studies of Information Processing - Proceedings of the International Conference
PublisherSpringer-Verlag
Pages302-325
Number of pages24
ISBN (Print)9783540095415
DOIs
Publication statusPublished - 1979 Jan 1
Externally publishedYes
EventInternational Conference on Mathematical Studies of Information Processing, 1978 - Kyoto, Japan
Duration: 1978 Aug 231978 Aug 26

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume75 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Conference on Mathematical Studies of Information Processing, 1978
CountryJapan
CityKyoto
Period78/8/2378/8/26

Fingerprint

Program Synthesis
Number theory
Figure
Computer program listings
Intuitionistic Logic
Transform
Interpretation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Goto, S. (1979). Program synthesis through Gödel's interpretation. In Mathematical Studies of Information Processing - Proceedings of the International Conference (pp. 302-325). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 75 LNCS). Springer-Verlag. https://doi.org/10.1007/3-540-09541-1_32

Program synthesis through Gödel's interpretation. / Goto, Shigeki.

Mathematical Studies of Information Processing - Proceedings of the International Conference. Springer-Verlag, 1979. p. 302-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 75 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Goto, S 1979, Program synthesis through Gödel's interpretation. in Mathematical Studies of Information Processing - Proceedings of the International Conference. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 75 LNCS, Springer-Verlag, pp. 302-325, International Conference on Mathematical Studies of Information Processing, 1978, Kyoto, Japan, 78/8/23. https://doi.org/10.1007/3-540-09541-1_32
Goto S. Program synthesis through Gödel's interpretation. In Mathematical Studies of Information Processing - Proceedings of the International Conference. Springer-Verlag. 1979. p. 302-325. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-09541-1_32
Goto, Shigeki. / Program synthesis through Gödel's interpretation. Mathematical Studies of Information Processing - Proceedings of the International Conference. Springer-Verlag, 1979. pp. 302-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{b29256594e064ff2b9406838cece4f35,
title = "Program synthesis through G{\"o}del's interpretation",
abstract = "This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of G{\"o}del's interpretation which is also called Dialectica interpretation. By the use of G{\"o}del's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.",
author = "Shigeki Goto",
year = "1979",
month = "1",
day = "1",
doi = "10.1007/3-540-09541-1_32",
language = "English",
isbn = "9783540095415",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "302--325",
booktitle = "Mathematical Studies of Information Processing - Proceedings of the International Conference",

}

TY - GEN

T1 - Program synthesis through Gödel's interpretation

AU - Goto, Shigeki

PY - 1979/1/1

Y1 - 1979/1/1

N2 - This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of Gödel's interpretation which is also called Dialectica interpretation. By the use of Gödel's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.

AB - This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of Gödel's interpretation which is also called Dialectica interpretation. By the use of Gödel's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.

UR - http://www.scopus.com/inward/record.url?scp=84867632620&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84867632620&partnerID=8YFLogxK

U2 - 10.1007/3-540-09541-1_32

DO - 10.1007/3-540-09541-1_32

M3 - Conference contribution

AN - SCOPUS:84867632620

SN - 9783540095415

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 302

EP - 325

BT - Mathematical Studies of Information Processing - Proceedings of the International Conference

PB - Springer-Verlag

ER -