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

Application of type theory and linear logic for Programming Languages

Research Project

Project/Area Number 07044093
Research Category

Grant-in-Aid for international Scientific Research

Allocation TypeSingle-year Grants
SectionJoint Research
Research InstitutionKeio University

Principal Investigator

OKADA Mitsuhiro  Keio University, Professor, 文学部, 教授 (30224025)

Co-Investigator(Kenkyū-buntansha) HAYASHI Susumu  Kobe University, 工学部, 教授 (40156443)
TAKAHASHI Masako  Tokyo Institute of Technology, 理学部, 助教授 (00015588)
OHORI Atsushi  Kyoto University, 数理解析研究所, 助教授 (60252532)
HAGIYA Masami  Tokyo University, 理学部, 教授 (30156252)
SATO Masahiko  Kyoto University, 工学部, 教授 (20027387)
PARIGOT Michel  Universite Paris VII
HUET Gerard  INRIA,France
JOUANNAUD Jean-Pierre  Universite Paris XI,L.R.I.
CURIEN Pierre-Luis  Ecole Normale Superiuer-Paris
GIRARD Jan-Yves  CNRS Mathematics Instutute-Marseille
Project Period (FY) 1995 – 1996
Project Status Completed (Fiscal Year 1996)
Budget Amount *help
¥10,200,000 (Direct Cost: ¥10,200,000)
Fiscal Year 1996: ¥5,100,000 (Direct Cost: ¥5,100,000)
Fiscal Year 1995: ¥5,100,000 (Direct Cost: ¥5,100,000)
KeywordsType Theory / Linear Logic / Constructive Proof / Programming Languages / Program Verification / Program Semantics / Concurrency / Intuitionistic Logic / Proof Theory / 直観主義理論 / プログラム言語
Research Abstract

Type THeory is provides an ideal formal framework for program verification and systematic program development utililzing the logical mechanism. On the other hand, linear logic provides the framework for expressing computational resources and concurrent computation. Therefore, it seems very promising to combine these two theories in order to design a powerful and new programming language and its program development tools. For this purpose, we have investigated the theoretical foundations for this combined formal framework, linear type language.
In particular, we established verious important semantics theories for the linear type language. For example, phase semantics is extended to a dynamic phase semantics in which cut-elimination and normalization proofs can be performed. Phase semantics is also extended to higher order linear type languages. Girard introduced Light Linear Logic, which is considered an impotant sybsystem of linear logic since it characterized the polynomial time computation in a purely logical way. We applied our phase semantics theory to Light Linear Logic and established phase semantic characterization of the important concepts used in Light Linear Logic. The coherence semantics has also been very much improved. For example, Coherence Banach Space Semantics, which is a promising denotational semantics for the linear type language, was developped when the French team leader, J-Y.Girard, visited our group in Japan. Various important computation models for the linear type language have been proposed in our project research. In particular, the reduction paradigm and the proof-search paradigm were studied from the programming paradigm and the proof- search paradigm were studied from the programming languages point of view.

Report

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

    (46 results)

All Other

All Publications (46 results)

  • [Publications] J-P.Jouannaud 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). 43- (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 岡田光弘(研究協力者 浜野正浩との共著): "A Direct Independence Proof of Buchholz's Hydra Game on Labeled Finite Trees" Archive for Mathematical Logic. (近刊). (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 岡田光弘(研究協力者 浜野正浩との共著): "A Relationship Among Gentzen's Proof Reduction,Rirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 高橋正子: "Parallel reduction in λ-calculus" Information and Computation. 118. 120-127 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 林晋: "TWO Extensions of PX Systems" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Jean-Yues Girard: "Coherent Barach Space" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] J-Y,Girard 岡田光弘 Andre Soedrov(共編): "Linear Logic (A special issue of Theoretical Computer Science)" Elsevier(オランダ)(近刊), 190 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 岡田光弘: "情報科学のための論理学" 産業図書(近刊), 273 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 大堀淳: "プログラム言語の基礎理論" 共立出版, 272 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] 林晋: "プログラミング検証理論" 共立出版, 211 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] J-Y,Girard(研究協力者Y,Lafonts L.Regnierとの共著): "Advances in Linear Logic" Cambridge University Press, 389 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] J-Y,Girard 岡田光弘 Andre Scedrov(共編): "Linear Logic,A special issue of Electronic Notes of Theoretical computer Science" Elsevier-EATCS(オランダ)(欧州理論情報学会), 256 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Jean-Pierre Jouannaud and Mitsuhiro Okada: "Abstract Data Type Systems" Theoretical Computer Science. (to appear). 43 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Mitsuhiro Okada (with Masahitro Hamano): "A Relationship Among Gentzen's Proof Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game" 43. 103-120 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Mitsuhiro Okada (with Masahiro Hamano): "A Direct Independence Proof of Buchholz's Hydra Game for Labeled Finite Trees" Archive for Mathematical Logic. (to appear). (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Susumu HAYASHI et al.: "Two Extensions of PX Systems" Electronic Notes of Theoretical Computer Science. 3. 12 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Jean-Yves Girard: "Coherent Banach Space" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Masako Tokahashi: "Parallel reduction in lambda calculus" Information and Computation. 118. 120-127 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Jean-Yves Girard-Mitsuhiro Okada-Andre Scedrov: Elsevier Science Publishing, The Netherlands (to appear). Linear Logic Special Issue, THeoretical Computer Science, 190 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Mitsuhiro Okada: Sangyo Tosto Publishing, Tokyo (to appear). Logic for Computer Science (in Japanese), 273 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Atsushi Ohori: Kyoritsu Tokyo, Tokyo. The Foundations of Programming Language Theory (in Japanese)., 272 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Susumu Hayashi: Kyoritsu Tosyo, Tokyo. Theory of Program Verification (in Japanese), 211 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Jean-Yves Girard (with Yves Lafont and L.Regnier): Cambridge University Press. Advances in Linear Logic, 389 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] Jean-Yves Girard-Mitsuhiro Okada-Andre Scedrov: Elsevier and EATCS (European Association for Theoretical Computer SCience).Linear Logic, A Special Issue of Electronic Notes of Theoretical Computer Science, 256 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1996 Final Research Report Summary
  • [Publications] J-P. Jouannaud 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岡田光弘(研究協力者浜野正浩との共著): "A Direct Independent Proof of Buchholz's Hydra Game on Lableled Finite Trees" Archive for Mathematical Logic. (近刊). (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岡田光弘(研究協力者浜野正浩との共著): "A Relationship Among Gentzen's Proof -Reduction, Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 105-120 (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 林晋: "Two Extensions of PX Systems" Electronic Notes of Theoretical Computer Science. 3. 12 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Jean-Yves Girard: "Coherent Banach Spaces" Electronic Notes of Theoretical Computer Science. 3. 13 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Jean-Yves Girard: "Denotational Completeness" Electronic Notes of Theoretical Computer Science. 3. 9 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] J-Y. Girard 岡田光弘 Andre Scedrove: "Linear Logic (Special Issue of Theoretial Computer Science)" Elsevier-EATCS(オランダ)(予定), 190 (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岡田光弘: "情報科学のための論理学" 産業図書(近刊)(予定), (1997)

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

    • Related Report
      1996 Annual Research Report
  • [Publications] J-Y. Girard(研究協力者Y. Lafont, L. Regnierとの共著): "Advances in Linear Logic" Cambridge University Press, 389 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] J-Y. Girard(研究協力者Y. Lafont, L. Regnierとの共編): "Advances in Linear Logic" Cambridge University Press, 389 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] J-Y. Girard 岡田光弘 Andre Scedrov(共編): "Linear Logic, A special issue of Electronic Notes of Theoretical Computer Science" Elsevier-EATCS(オランダ)(欧州理論情報学会), 256 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Jouannaud,Jean-Pierre 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] 岡田光弘(浜野と共著): "A Direct Proof of Buchholz's Hydra Game" Archiev for Mathematical Logic. (近刊). (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] Susumu Hayashi(林晋)and S.Kobayashi: "A new formalization of Feferman's system of functions and classes and its velation to Frege structure." International J. of Foundations of Computer Science.6(No.3). 187-202 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] M.Hagiya et al.: "Formalization of Planar Graphs" Proc.of Higher Order Theorem Proving and its Applications,Lecture Notes in Computer Science(Springer). 971. 369-384 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] M.Takahashi: "Parallel reduction in λ-calculus" Information and Computation. 118. 120-127 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 佐藤雅彦(亀山との共著): "自己反映的証明体系RPTの理論と実現" コンピュータソフトウエア. 12(2). 32-51 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 岡田光弘: "情報科学のための論理" 産業図書, 240 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] Girard,Jean-Yves 岡田光弘 Scedrov,Andre: "Special Issue on Linear Logic (ENTCS series)" Elsevier社(オランダ), 420 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] Girard,Jean-Yves(フランス側代表者): "Advances in Linear Logic" Cambridge University Press, 340 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] 林普: "プログラム検証論" 共立出版, 208 (1995)

    • Related Report
      1995 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi