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

Implementation of Constructive Programming Based on Classical Logic

Research Project

Project/Area Number 10480061
Research Category

Grant-in-Aid for Scientific Research (B)

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

Principal Investigator

SATO Masahiko  Kyoto University, Graduate School of Informatics, Professor, 情報学研究科, 教授 (20027387)

Co-Investigator(Kenkyū-buntansha) TAKEUTI Izumi  Kyoto University, Graduate School of Informatics, Research Associate, 情報学研究科, 助手 (20264583)
KAMEYAMA Yukiyoshi  Kyoto University, Graduate School of Informatics, Associate Professor, 情報学研究科, 助教授 (10195000)
Project Period (FY) 1998 – 1999
Project Status Completed (Fiscal Year 1999)
Budget Amount *help
¥4,600,000 (Direct Cost: ¥4,600,000)
Fiscal Year 1999: ¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 1998: ¥2,900,000 (Direct Cost: ¥2,900,000)
KeywordsClassical Logic / Constructive Programming / Type Theory / 算術 / キャッチ・スロー機構
Research Abstract

For the purpose of developing constructive programming based on classical logic, this research extended the functional programming language PAィイD2ctィエD2, which has catch/throw mechanism as exception processing, and made the following results.
The head investigator Sato studied the notion of binding variables, which is the important notion for predicate logic and functional programming language. As the result of this study, he proposed a calculus which do not have renaming of bind variables. This result was presented in the 4th international conference on Typed Lambda Calculi and Application in 1999, at L'Aquia, Italy.
The investigator Kameyama studied exception processing and partial contiunation in functional programming languages based on classical logic, and classified typical calculi with exception processing and partial continuation. He solved the problems of confluency and termination of such calculi. This results are to be published in 'Theoretical Computer Science'.
The investigator Takeuti studied the relation between parametric polymorphism and mathematical induction. Mathematical induction is an important method to prove theorems in systems of constructive programming. He showed that system of parametricity derives various forms of mathematical induction. This result was published in 'Fundamenta Informaticae'.

Report

(3 results)
  • 1999 Annual Research Report   Final Research Report Summary
  • 1998 Annual Research Report
  • Research Products

    (14 results)

All Other

All Publications (14 results)

  • [Publications] 佐藤 雅彦 他: "Explicit Enviroments"Lectare Notes in Conputer Science. 1581. 340-354 (1999)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 亀山 幸義 他: "Strong Normalizability of the Non-deterministic Catek/t*"Theoretical Computer Sciece. (掲載予定). (2000)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 亀山 幸義: "A Type System for Delimited Continnations"JSSST Workshop on Programming & Programming Languages. (掲載予定). (2000)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 竹内 泉: "An Axiomatic System of Parame Tricity"Fundamenta Informatical. 33. 397-432 (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] Sato Masahiko, Barstall Rod & Sakurai Taka-fumi: "Expicit Environment,"Proc. Typed Lambda Calcu-lus and Applications 1999, LNCS. vol.1581 Springer. 340-354 (1999)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] Kameyama Yukiyoshi & Sato Sato: "Strong Normalizability of the Non-deterministic Catch/Throw Calculi,"Theoretical Computer Science. (to appear).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] Kameyama Yukiyoshi: "A Type System for Delimited Continuations,"JSSST Workshop on Program-ming and Programming Lan-guages'2000, March. (2000)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] Takeuti Izumi: "An axiomatic system of parametricity,"Fundamenta Informaticae. 33. 397-432 (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1999 Final Research Report Summary
  • [Publications] 佐藤 雅彦 他: "Explicit Environments"Lecture Notes in Computer Science. 1581. 340-354 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] 亀山 幸義 他: "Strong Normalizability of the Non-deterministic Cateh/Thow caluculi"Theoretical Computer Science. (掲載予定). (2000)

    • Related Report
      1999 Annual Research Report
  • [Publications] 亀山 幸義: "A Type System for Delimited Continuations"JSSST Workshop on Programming & Programming Languages. (掲載予定). (2000)

    • Related Report
      1999 Annual Research Report
  • [Publications] 竹内 泉: "An Axiomatic System of Parametricity"Fundamenta Informatical. 33. 397-432 (1998)

    • Related Report
      1999 Annual Research Report
  • [Publications] 佐藤雅彦、桜井貴文、ロッド・バーストール: "Explicit Environments" Typed Lambda Calculus And Aplications. (発表予定). (1999)

    • Related Report
      1998 Annual Research Report
  • [Publications] 鴨浩靖・河邑紀子・竹内泉: "Hausdorff Dimension & Computational Complexity" INFORMATIK BERICHTE, Compulerity in Analysis Fern University. 235-8. 41-50 (1998)

    • Related Report
      1998 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi