• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Theory of Constructive Programming

Research Project

Project/Area Number 08458068
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionKYOTO UNIVERSITY

Principal Investigator

SATO Masahiko  Kyoto Univ.Information Science Prof., 工学研究科, 教授 (20027387)

Co-Investigator(Kenkyū-buntansha) TAKEUTI Izumi  Kyoto Univ.Information Science.Instructor, 工学研究科, 助手 (20264583)
KAMEYAMA Yukiyoshi  Kyoto Univ.Information Science.Assoc.Prof.Instructor, 工学研究科, 助教授 (10195000)
TATSUTA Makoto  Kyoto Univ.Math.Assoc.Prof., 理学研究科, 助教授 (80216994)
Project Period (FY) 1996 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥7,300,000 (Direct Cost: ¥7,300,000)
Fiscal Year 1997: ¥2,600,000 (Direct Cost: ¥2,600,000)
Fiscal Year 1996: ¥4,700,000 (Direct Cost: ¥4,700,000)
KeywordsConstructive Programming / Catch / Throwcontrd / Type Theory / Catch / Throw機構
Research Abstract

This project had three large subjects, which are listed in the following.
The first was to construct logical systems corresponding to catch-throw mechanism. The investigators researched for characteristics and semantics of logical systems corresponding to catch/throw mechanism. As the result of that the investigators constructed the logical systems MJct and NKct, and proved that the logical systems NJct and NKct are conservative extensions of NJ and NK, respectively. The investigators also showed that these systems are useful for constructive programming. This subject was mainly developed by Sato and Kameyama.
The second was on realizability interpretations of untyped calculation theory. The investigations was aimed at giving realizability interpretations for logical systems with untyped calculus, and applying it to constructive programming. As the result of that, the investigators gave a realizability interpretation for logical system for a set theory. This realizability interpretation is very much improved as compared to the former ones, which used double variables. The investigators also gave a realizability interpretation for a system with co-induction, and showed an application of this realizability interpretation to constructive programming. This subject was mainly developed by Tatsuta.
The third was on constructivew logical systems for polymorphism. The investigators made a research pn parametricity of polymorphic calculation systems, such as SYstem F, second order lambda calculus. As the result of that, the investigators gave logical systems ; one of them is for parametric polymorphism of System F, and another is for cyclic structure. This subject was mainly developed by Takeuti.

Report

(3 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • Research Products

    (22 results)

All Other

All Publications (22 results)

  • [Publications] Masahiko Sato: "Classical Brouwer-Heyting-Kolmogorov Interpretation" Lecture Notes in Artificial Intelligence. 1316. 176-196 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Makoto Tatsuta: "Realizability of Monotone Coindudive Definitions and its Application to Program Synthesis" Lecture Notes in Computer Science. (発表予定).

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Makoto Tatsuta: "Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis" Proc.13th IEEE Symposium on Logicin Computer Science. 13(発表予定). (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Austalasian Theory Symposium. 20-3. 183-197 (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Izumi Takeuti: "An Axiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Izumi Takeuti: "A Type Theory for Cyclic Structure" Proc.3rd Fuji Int'l Symp.on Func.and Logic Programing. 3(発表予定). 207-226 (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Masahiko Sato: "Classical Brouwer-Heyting-Kolmogorov Interpretation" LectureNotes in Artificial Intelligence. 1316. 176-196 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Makoto Tatsuta: "Realizability of Monotone Coinductive Definitions and its Application to Program Synthesis" Lecture Notes in Computer Science. (to appear).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Makoto Tatsuta: "Realizability of Coinductive THeory of Functions and Classes and its Application to Program Synthesis" Lecture Notes in Computer Science. 13. (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Yoshiyuki Kameyama: "A Classical Catch/Throw Calculus with Tag Abstruction and its Strong Normalizability" Proc.4th Australasian Theory Symposium. 20-3. 183-197 (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Izumi Takeuti: "An Axiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Izumi Takeuti: "A Type Theory for Cyclic Structure" Proc.3rd Fuju Internationall Symposium in Functional and Logic Programming. 3. 207-226 (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Masahiko Sato: "Classical Brouwer-Heyting-Kolmogorov Interpretation" Lecture Notes in Artificial Intelligence. 1316. 176-196 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Makoto Tatsuta: "Realizability of Monotone Coinducfive Definitions and its Application to Program Synthesis" Lecture Notes in Computer Science. (発表予定).

    • Related Report
      1997 Annual Research Report
  • [Publications] Makoto Tatsuta: "Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis" Proc.13th IEEE Symposium on Logicin Computer Science. 13. (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Austalasian Theory Symposium. 20-3. 183-197 (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] Izumi Takeuti: "An Ayiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Izumi Takeuti: "A Type Theory for Cyclic Structure" Proc.3rd Fuji Int'l Symp.on Func.and logic Programing. 3(発表予定). (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] Masahiko Sato: "Intuitionistic and Classical Natural Deduction Systems with the Catch and the Throw Rules" Theoretical Computer Science. (発表予定).

    • Related Report
      1996 Annual Research Report
  • [Publications] 山中淳彦: "参照透明な代入をもつ純関数型言語" コンピュータ・ソフトウェア. (発表予定).

    • Related Report
      1996 Annual Research Report
  • [Publications] Mitsuru Tada: "The Fumction [9/m] in Sharply Bounded Arithmetic" Archive for Mathematical Logic. (発表予定).

    • Related Report
      1996 Annual Research Report
  • [Publications] Yukiyoshi Kameyama: "A New Formalation of the Catch/Throw Mechanisin" Proc.Int'l Workshop on Func. and Logic Progr.56-64 (1996)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi