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

Sheaf structure in higher-order computaton and logic

Research Project

Project/Area Number 24500025
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Fundamental theory of informatics
Research InstitutionHosei University

Principal Investigator

KURATA Toshihiko  法政大学, 経営学部, 教授 (40311899)

Co-Investigator(Kenkyū-buntansha) KOMORI Yuichi  千葉大学, 理学(系)研究科(研究院), 名誉教授 (10022302)
FUJITA Ken-etsu  群馬大学, 理工学研究院, 准教授 (30228994)
Co-Investigator(Renkei-kenkyūsha) KASHIMA Ryo  東京工業大学, 情報理工学(系)研究科, 准教授 (10240756)
Project Period (FY) 2012-04-01 – 2015-03-31
Project Status Completed (Fiscal Year 2014)
Budget Amount *help
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2014: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2013: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2012: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Keywords分配具象領域 / 高階逐次性 / 層論 / 分配具象領域の表現定理 / 具象領域 / 逐次アルゴリズム / 逆像層 / ゲーム意味論 / innocent戦略
Outline of Final Research Achievements

The structure of distributive concrete domains is known to model the machinery of sequential evaluation of higher-order programming languages, which is obtained by incorporating three technical conditions into a naive structure of models based on the well-known theory of domains. In this respect, we show that these three conditions are comparable with the structure of sheaves studied in mathematics, and actually obtain a both-way translation between distributive concrete domains and sheaves endowed with a domain theoretical feature.

Report

(4 results)
  • 2014 Annual Research Report   Final Research Report ( PDF )
  • 2013 Research-status Report
  • 2012 Research-status Report
  • Research Products

    (26 results)

All 2015 2014 2013 2012 Other

All Journal Article (15 results) (of which Open Access: 2 results,  Peer Reviewed: 9 results,  Acknowledgement Compliant: 1 results) Presentation (11 results) (of which Invited: 1 results)

  • [Journal Article] On sheaves categorically equivalent to distributive concrete domains2015

    • Author(s)
      倉田俊彦
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: 印刷中

    • Related Report
      2014 Annual Research Report
    • Open Access
  • [Journal Article] On styles of lambda2-terms --extended abstract--2015

    • Author(s)
      K. Fujita
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: 印刷中

    • Related Report
      2014 Annual Research Report
    • Open Access
  • [Journal Article] Reduction Rules for Intuitionistic λρ-calculus2015

    • Author(s)
      Ken-etsu Fujita, Ryo Kashima, Yuichi Komori, and Naosuke Matsuda
    • Journal Title

      Studia Logica

      Volume: 印刷中

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Existential type systems between Church and Curry style (type-free style)2014

    • Author(s)
      K. Fujita, A. Schubert
    • Journal Title

      Theoretical Computer Science

      Volume: 549 Pages: 17-35

    • DOI

      10.1016/j.tcs.2014.05.019

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Journal Article] A Simplified Proof of the Church-Rosser Theorem2014

    • Author(s)
      Yuichi Komori, Naosuke Matsuda & Fumika Yamakawa
    • Journal Title

      Studia Logica

      Volume: 102 Issue: 1 Pages: 175-183

    • DOI

      10.1007/s11225-013-9470-y

    • Related Report
      2013 Research-status Report 2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] A note on subject reduction in (→,∃)-Curry with respect to complete developments2014

    • Author(s)
      Aleksy Schubert & Ken-etsu Fujita
    • Journal Title

      Information Processing Letters

      Volume: 114-1,2 Pages: 72-75

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] ラムダ計算の型問題について --数学基礎論からプログラミング言語の構造へ--2014

    • Author(s)
      藤田 憲悦
    • Journal Title

      数学 岩波書店

      Volume: 第66巻 第1号 Pages: 78-89

    • NAID

      130006882589

    • Related Report
      2013 Research-status Report
  • [Journal Article] An axiomatization of ECTL2014

    • Author(s)
      Ryo Kashima
    • Journal Title

      Journal of Logic and Computation

      Volume: 24 Issue: 1 Pages: 117-133

    • DOI

      10.1093/logcom/ext005

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Sheaf-theoretical representation of concrete domains2013

    • Author(s)
      倉田俊彦
    • Journal Title

      京都大学数理解析研究所講究録 (RIMS共同研究 証明論と複雑性)

      Volume: 1832 Pages: 8-18

    • Related Report
      2013 Research-status Report
  • [Journal Article] λρ-calculus II2013

    • Author(s)
      Yuichi Komori
    • Journal Title

      Tsukuba Journal of Mathematics

      Volume: 37 Pages: 307-320

    • NAID

      120006582878

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Decidable structures between Church-style and Curry-style2013

    • Author(s)
      Ken-etsu Fujita & Aleksy Schubert
    • Journal Title

      Leibniz International Proceedings in Informatics (RTA 2013 -- Rewriting Techniques and Applications 24th International Conference)

      Volume: 21 Pages: 190-205

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] On fine structures between Church-style and Curry-style λ2-terms2013

    • Author(s)
      藤田憲悦
    • Journal Title

      京都大学数理解析研究所講究録 (RIMS共同研究 証明論と複雑性)

      Volume: 1832 Pages: 73-87

    • Related Report
      2013 Research-status Report
  • [Journal Article] Sheaf-Theoretical Representation of Concrete Domains2013

    • Author(s)
      倉田俊彦
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: -

    • Related Report
      2012 Research-status Report
  • [Journal Article] An axiomatization of ECTL2013

    • Author(s)
      Ryo Kashima
    • Journal Title

      Journal of Logic and Computation

      Volume: -

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] The undecidability of type related problems of the type-free style System F with finitely stratified polymorphic types2012

    • Author(s)
      K. Fujita, A. Schubert
    • Journal Title

      Information and Computation

      Volume: 218

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Presentation] On sheaves categorically equivalent to distributive concrete domains2014

    • Author(s)
      倉田俊彦
    • Organizer
      RIMS研究集会「証明論・計算論とその周辺」
    • Place of Presentation
      京都大学数理解析研究所(京都府京都市)
    • Year and Date
      2014-12-24 – 2014-12-26
    • Related Report
      2014 Annual Research Report
  • [Presentation] On styles of lambda2-terms2014

    • Author(s)
      K. Fujita
    • Organizer
      RIMS研究集会「証明論・計算論とその周辺」
    • Place of Presentation
      京都大学数理解析研究所(京都府京都市)
    • Year and Date
      2014-12-24 – 2014-12-26
    • Related Report
      2014 Annual Research Report
  • [Presentation] 分配具象領域と領域層の圏論的同等性に関する考察2014

    • Author(s)
      倉田俊彦
    • Organizer
      日本数学会秋季総合分科会
    • Place of Presentation
      広島大学(広島県東広島市)
    • Year and Date
      2014-09-25 – 2014-09-28
    • Related Report
      2014 Annual Research Report
  • [Presentation] Semilattice relevant logic について2014

    • Author(s)
      鹿島亮
    • Organizer
      日本数学会秋季総合分科会
    • Place of Presentation
      広島大学(広島県東広島市)
    • Year and Date
      2014-09-25 – 2014-09-28
    • Related Report
      2014 Annual Research Report
  • [Presentation] Sheaf-theoretical representation of concrete domains

    • Author(s)
      倉田俊彦
    • Organizer
      日本数学会2013年度秋季総合分科会
    • Place of Presentation
      愛媛大学(愛媛県)
    • Related Report
      2013 Research-status Report
  • [Presentation] ラムダ計算の型問題を支配する本質的情報について

    • Author(s)
      藤田憲悦
    • Organizer
      日本ソフトウェア科学会第30回大会
    • Place of Presentation
      東京大学(東京都)
    • Related Report
      2013 Research-status Report
  • [Presentation] Intermediate lambda-terms between Church and Curry

    • Author(s)
      Ken-etsu Fujita & Aleksy Schubert
    • Organizer
      日本数学会2014年度年会
    • Place of Presentation
      学習院大学(東京都)
    • Related Report
      2013 Research-status Report
  • [Presentation] 時相論理CTL*やその部分体系の公理化について

    • Author(s)
      鹿島亮,岩波克
    • Organizer
      日本数学会2013年度秋季総合分科会
    • Place of Presentation
      愛媛大学(愛媛県)
    • Related Report
      2013 Research-status Report
  • [Presentation] Sheaf-Theoretical Representation of Concrete Domains

    • Author(s)
      倉田俊彦
    • Organizer
      RIMS研究集会(証明論と複雑性)
    • Place of Presentation
      京都大学数理解析研究所
    • Related Report
      2012 Research-status Report
  • [Presentation] 数学者のために数理論理学雑談

    • Author(s)
      古森雄一
    • Organizer
      日本数学会
    • Place of Presentation
      九州大学
    • Related Report
      2012 Research-status Report
    • Invited
  • [Presentation] On fine structures between Church-style and Curry-style lambda2-terms

    • Author(s)
      K. Fujita
    • Organizer
      RIMS研究集会(証明論と複雑性)
    • Place of Presentation
      京都大学数理解析研究所
    • Related Report
      2012 Research-status Report

URL: 

Published: 2013-05-31   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi