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

On algebraic structure of functional programming languages: towards mathematical foundation of logical relations

Research Project

Project/Area Number 26730004
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeMulti-year Fund
Research Field Theory of informatics
Research InstitutionKyoto University

Principal Investigator

Hoshino Naohiko  京都大学, 数理解析研究所, 助教 (20611883)

Project Period (FY) 2014-04-01 – 2019-03-31
Project Status Completed (Fiscal Year 2018)
Budget Amount *help
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2017: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2016: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2015: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2014: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Keywords論理関係 / 圏論的意味論 / 関数型プログラミング言語
Outline of Final Research Achievements

Logical relation is a powerful mathematical technique to prove mathematical properties of functional programming languages such as: observational equivalence of programs, strong normalization of lambda terms and parametricity principle of second-order lambda calculi. The main contribution of this research project is a construction of categorical models for higher-order (high-level) functional programming languages starting from categorical models of first-order (low-level) programming languages. We applied this construction technique to give adequate categorical models for higher-order functional programming languages with algebraic effects and a higher-order functional programming language with continuous probabilistic distribution and "scoring" mechanism. Our construction can be regarded as a program translation technique of higher-order (high-level) programming languages into first-order (low-level) programming languages.

Academic Significance and Societal Importance of the Research Achievements

本研究の成果からは種々の特徴(代数的副作用や連続的確率分布を扱えるなど)を持った高階の関数型プログラミング言語を同様の特徴を持つ一階のプログラミング言語に変換する手法が得られる.ここでの変換の数学的正しさは変換の導出に用いた論理関係により保証されている.この変換手法を経由することで一階のプログラミング言語の検証手法を高階の関数型プログラミング言語の検証手法に拡張することができると期待される.特に連続的確率分布を扱うプログラミング言語の検証は機械学習の研究の進展によりその重要性が増している.

Report

(6 results)
  • 2018 Annual Research Report   Final Research Report ( PDF )
  • 2017 Research-status Report
  • 2016 Research-status Report
  • 2015 Research-status Report
  • 2014 Research-status Report
  • Research Products

    (6 results)

All 2019 2018 2016 2014 Other

All Journal Article (2 results) (of which Peer Reviewed: 2 results) Presentation (3 results) (of which Int'l Joint Research: 2 results) Remarks (1 results)

  • [Journal Article] Geometry of Bayesian Programming2019

    • Author(s)
      Ugo Dal Lago and Naohiko Hoshino
    • Journal Title

      To appear in Proceedings of Logic in Computer Science 2019

      Volume: -

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Partial Traces on Additive Categories2018

    • Author(s)
      Hoshino Naohiko
    • Journal Title

      Electronic Notes in Theoretical Computer Science

      Volume: 341 Pages: 219-237

    • DOI

      10.1016/j.entcs.2018.11.011

    • NAID

      120006695789

    • Related Report
      2018 Annual Research Report
    • Peer Reviewed
  • [Presentation] Partial Traces on Additive Categories2018

    • Author(s)
      Naohiko Hoshino
    • Organizer
      Mathematical Foundations of Programming Semantics
    • Related Report
      2018 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Memoryful Geometry of Interaction II: Recursion and Adequacy2016

    • Author(s)
      Koko Muroya, Naohiko Hoshino, Ichiro Hasuo
    • Organizer
      Principle of programming language
    • Place of Presentation
      St. Petersburg, Florida, United States
    • Year and Date
      2016-01-22
    • Related Report
      2015 Research-status Report
    • Int'l Joint Research
  • [Presentation] Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects2014

    • Author(s)
      Naohiko Hoshino, Koko Muroya, Ichiro Hasuo
    • Organizer
      Logic in computer science
    • Place of Presentation
      Vienna, Austria
    • Year and Date
      2014-07-14 – 2014-07-18
    • Related Report
      2014 Research-status Report
  • [Remarks]

    • URL

      http://www.kurims.kyoto-u.ac.jp/~naophiko/

    • Related Report
      2016 Research-status Report

URL: 

Published: 2014-04-04   Modified: 2020-03-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi