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

タイプ理論および線形論理の情報科学への応用に関する国際共同研究の企画

Research Project

Project/Area Number 09898005
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section企画調査
Research Field 計算機科学
Research InstitutionKeio University

Principal Investigator

岡田 光弘  慶應義塾大学, 文学部, 教授 (30224025)

Co-Investigator(Kenkyū-buntansha) 林 晋  神戸大学, 工学部, 教授 (40156443)
高橋 正子  東京工業大学, 理学部, 教授 (00015588)
大堀 淳  京都大学, 数理解析研究所, 教授 (60252532)
萩谷 昌己  東京大学, 理学研究科, 教授 (30156252)
佐藤 雅彦  京都大学, 工学部, 教授 (20027387)
Project Period (FY) 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 1997: ¥2,400,000 (Direct Cost: ¥2,400,000)
Keywords線形論理 / タイプ理論 / プログラミング言語 / 直観主義論理 / 理論情報科学 / 形式的検証 / 形式的仕様 / ソフトウェア開発
Research Abstract

われわれ共同研究チームは、論理学的手法に情報科学への応用、特にタイプ理論と線形論理の情報科学への応用に関する国際共同研究・国際学術交流の枠組を確立することを目指した。
(1)日本国内の本分野の大学間共同研究グループの基盤を広げ、本分野におけるわが国のさらなる国際的貢献を目指すとともに、(2)上記ヨーロッパ・プロジェクトグループ、北米プロジェクト・グループとの協議を通じて、日本の研究グループとヨーロッパ共同体研究ブロック、北米共同研究ブロックとの間での三者の研究協力の枠組みを作ることを本企画研究の第一の目標とした。
本研究チームは「タイプ理論と線形論理のプログラム言語理論への応用」に関するする国際共同研究の企画を行った。本年度に我々が本企画研究を通して企画した国際共同研究は平成10年度からの科学研究費国際共同研究として内定を受けた。
国際共同研究の企画のためにヨーロッパ共同体の相手側チームのリーダ達(G.Huet.J.P.Jouannaud.J-Y.Girard.H.Baretulregt.M.Drziuni.G.Plotkin.M.Kanovitch)や北米のNorth American Jumelageの相手側リーダー達(A.Scedrov.J.Mitehrll.P.I.ineolu.J.Ianubek.P.J.Scott)と特に充分な協議、打ち合わせを行い準備を進めた。

Report

(1 results)
  • 1997 Annual Research Report
  • Research Products

    (8 results)

All Other

All Publications (8 results)

  • [Publications] J.Y.Girard.M.Okada.A.Scedrov: "Linear Logie Special Issne" Theoretical Computer Science. (to appear). 0-0 (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Okada.K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic" J.Symbolic Logic. (to appear). 0-0 (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Sato: "Intuitionistic and Classical Natural Deduetion Systems with the Catch and Throw Rules" Theoretical Computer Science. (to appear). 0-0 (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] J.P.Jouannaud,M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. 173. 349-391 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Hamano-M.Okada: "A Relationship Among Gentzen's Proof Reduction.Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Kanovitch, M.Okada, A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Takahashi: "Types and Proofs" Mathematical Sciety of Japan, 000 (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] 大堀淳: "プログラミング言語の基礎理論" 共立出版, 272 (1997)

    • Related Report
      1997 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi