• DocumentCode
    1957287
  • Title

    Realizability for constructive theory of functions and classes and its application to program synthesis

  • Author

    Tatsuta, Makoto

  • Author_Institution
    Dept. of Math., Kyoto Univ., Japan
  • fYear
    1998
  • fDate
    21-24 Jun 1998
  • Firstpage
    358
  • Lastpage
    367
  • Abstract
    This paper gives a q-realizability interpretation for Feferman´s constructive theory T0 of functions and classes by using a set completion program without doubling variables, and proves its soundness. This result solves an open problem proposed by Feferman in 1979. Moreover by using this interpretation we can prove a program extraction theorem for T0, which enables us to use constructive sets of T0 for program synthesis
  • Keywords
    programming theory; type theory; constructive theory; program extraction theorem; program synthesis; q-realizability interpretation; set completion program;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
  • Conference_Location
    Indianapolis, IN
  • ISSN
    1043-6871
  • Print_ISBN
    0-8186-8506-9
  • Type

    conf

  • DOI
    10.1109/LICS.1998.705671
  • Filename
    705671
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1957287