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

A study on denotational semantics of λμ-calculus

Research Project

Project/Area Number 14540119
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionGunma University (2004)
Shimane University (2002-2003)

Principal Investigator

FUJITA Ken-etsu  Gunma University, Department of Computer Science, Associate Professor, 工学部, 助教授 (30228994)

Co-Investigator(Kenkyū-buntansha) KONDO Michio  Tokyo Denki University, School of Information Environment, Professor, 情報環境学部, 教授 (40211916)
Project Period (FY) 2002 – 2004
Project Status Completed (Fiscal Year 2004)
Budget Amount *help
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 2004: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2003: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2002: ¥1,200,000 (Direct Cost: ¥1,200,000)
Keywordsλμ-calculus / CPS-translation (continuation) / Polymorphic functions / Abstract data types / Curry-Howard isomorphism / Galois connection / Control operator / Duality / CPS変換 / 表示的意味論 / 継続 / スコット領域 / Cモノイド / タイプフリーラムダミュウ計算 / 継続的意味論 / タイプフリーラムダ計算 / 不動点演算子 / 完備半順序集合(CPO)
Research Abstract

A correspondence between Intuitionistic logic and typed λ-calculus is well-known as Curry-Howard isomorphism. M.Parigot (1992) has extended the correspondence and introduced λμ-calculus as a second-order classical logic. λμ-calculus is a natural extension of λ-calculus and the system itself is quite interesting as a functional computation model. In the last two years' project, we have investigated the following points :
(1)CPS-translation from type-free and simply typed λμ-calculi intoλ-calculus ;
(2)Continuation denotational semantics of λμ-calculus and C-monoid ;
(3)Similarity relation on CPO between CPS-translation and continuation denotational semantics.
In order to extend the results above, we introduced a new system, an existential type system λ∃. It is proved that there exist bijective translations between polymorphicλ-calculus and a subsystem of λ∃, which form a Galois connection and moreover Galois embedding. From a programming point of view, this result means that polymorphic functions can be represented by abstract data types.

Report

(4 results)
  • 2004 Annual Research Report   Final Research Report Summary
  • 2003 Annual Research Report
  • 2002 Annual Research Report
  • Research Products

    (17 results)

All 2005 2004 Other

All Journal Article (7 results) Publications (10 results)

  • [Journal Article] Galois embedding from polymorphic types into existential types2005

    • Author(s)
      Ken-etsu Fujita
    • Journal Title

      Lecture Notes in Computer Science 3461

      Pages: 194-208

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] Galois embedding from polymorphie types into existential types2005

    • Author(s)
      Ken-etsu Fujita
    • Journal Title

      Lecture Notes in Computer Science Vol.3461

      Pages: 194-208

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] ガロア埋め込み:多相型関数と抽象データ型の証明双対性2004

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

      日本ソフトウェア科学会第21回大会講演論文集 (CD-R)

    • NAID

      130005006578

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] Characterization theorem of lattice implication algebras2004

    • Author(s)
      Michio Kondo
    • Journal Title

      Proc.34th International Symposium on Multiple-Valued Logics

      Pages: 257-206

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] On the class of QS-algebras2004

    • Author(s)
      Michio Kondo
    • Journal Title

      International Journal of Mathematics and Mathematical Sciences 49-1

      Pages: 2629-2639

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] Galois embedding : proof duality between polymorphic functions and abstract data types2004

    • Author(s)
      Ken-etsu Fujita
    • Journal Title

      21st Conference Proceedings Japan Society for Software Science and Technology (CD-R)

    • NAID

      40022142607

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Characterization theorem of lattice implication algebra2004

    • Author(s)
      Michio Kondo
    • Journal Title

      Proc.34th International Symposium on Multi-Valued Logics

      Pages: 257-260

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Publications] 藤田 憲悦: "λμ計算のモデルについて"コンピュータソフトウェア. 20・3. 73-79 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Ken-etsu Fujita: "An injective CPS-translation for the extensional λ-calculus"Memoirs of the Faculty of Science and Engineering, Shimane University, Series B : Mathematical Science. 36. 39-48 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Ken-etsu Fujita: "A sound and complete CPS-translation for λμ-calculus"Lecture Notes in Computer Science. 2701. 120-134 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Michio Kondo: "Fuzzy congruence on BCI-algebras"Scientiae Mathematicae Japonicae. 57. 191-196 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Y.B.Jun, H.S.Kim, M.Kondo: "The class of B-algebras coincides with the class of groups"Scientiae Matheraaticae Japonicae. 58. 93-97 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Michio Kondo: "A note on interval-valued subalgebras ideals in BCK-algebras"Far East Jour.of Math.Sciences. 8. 109-119 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Ken-etsu Fujita: "An interpretation of λμ-calculus in λ-calculus"Information Processing Letters. 84. 261-264 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Ken-etsu Fujita: "Continuation semantics and CPS-translation of λμ-calculus"Scientiae Mathematicae Japonicae. 57・1. 73-82 (2003)

    • Related Report
      2002 Annual Research Report
  • [Publications] Michio Kondo: "On the structure of weak interlaced bilattice"Proc. 32^<nd> International Symposium for Multiple-Valued Logic. 23-26 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] H.J.Jung, M.Kondo, S.M.Hong: "Intuitionistic fuzzy filters in BCH-algebras"Mathematica Japonica Online. 7. 337-345 (2002)

    • Related Report
      2002 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi