Reasoning about computational effects by TT-lifting

• Project/Area Number: 24700012
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Fundamental theory of informatics
• Research Institution: Kyoto University
• Principal Investigator: KATSUMATA Shiin-ya 京都大学, 数理解析研究所, 助教 (30378963)
• Research Collaborator: SATO Tetsuya
• Project Period (FY): 2012-04-01 – 2015-03-31
• Project Status: Completed (Fiscal Year 2014)
• Budget Amount: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2014: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2013: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2012: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
• Keywords: モナド / 論理関係 / 表示的意味論 / エフェクトシステム / ファイブレーション / 余代数 / 計算効果 / TT-lifting / 国際研究者交流

Outline of Final Research Achievements

In the denotational semantics of programming languages, monads are a widely used mathematical structure to give a unified model of various kinds of side-effects. Previously, Katsumata introduced the semantic TT-lifting as a mathematical tool to study the properties of monadic semantics of programming languages. In this research, we apply the semantic TT-lifting 1) to show a generic effect soundness in the denotational semantics of general effect systems, and 2) to give a construction and a characterisation of preorders on monads. We also extend the semantic TT-lifting so that it works with wider categorical situations.

Research Products

• [Journal Article] Parametric effect monads and semantics of effect systems (2014)
  • Author(s): Shin-ya Katsumata
  • Journal Title: ACM SIGPLAN Notices - POPL '14 Volume: 49-1 Issue: 1 Pages: 633-645
  • DOI: 10.1145/2578855.2535846
  • Peer Reviewed
• [Journal Article] Relating computational effects by TT-lifting (2013)
  • Author(s): Shin-ya Katsumata
  • Journal Title: Information and Computation Volume: 222 Pages: 228-246
  • DOI: 10.1016/j.ic.2012.10.014
  • Peer Reviewed
• [Journal Article] Preorders on Monads and Coalgebraic Simulations (2013)
  • Author(s): Shin-ya Katsumata and Tetsuya Sato
  • Journal Title: Lecture Notes in Computer Science Volume: 7794 Pages: 145-160
  • DOI: 10.1007/978-3-642-37075-5_10
  • ISBN: 9783642370748, 9783642370755
  • Peer Reviewed
• [Presentation] ファイブレーションと余稠密モナドによるモナドの持ち上げ (2015)
  • Author(s): 勝股審也
  • Organizer: 理論計算機科学と圏論ワークショップ CSCAT 2015
  • Place of Presentation: 鹿児島大学
  • Year and Date: 2015-03-15
• [Presentation] Parametric effect monads and semantics of effect systems (2014)
  • Author(s): Shin-ya Katsumata
  • Organizer: Principles of Programming Languages, POPL 2014
  • Place of Presentation: US grant, San Diego, USA
• [Presentation] Relating Computational Effects by TT-Lifting (2013)
  • Author(s): Shin-ya Katsumata
  • Organizer: Nordic Workshop on Programming Theory, NWPT '13
  • Place of Presentation: Mustpeade maja, Tallinn, Estonia
  • Invited
• [Presentation] Preorders on Monads and Coalgebraic Simulations (2013)
  • Author(s): Tetsuya Sato (Shin-ya Katsumata)
  • Organizer: The 16th International Conference on Foundations of Software Science and Computation Structures
  • Place of Presentation: Sapienza Universita di Rome, Italy
• [Presentation] A Generic Soundness Result for Effect Systems (2012)
  • Author(s): Shin-ya Katsumata
  • Organizer: The 10th Asian Symposium on Programming Languages and Systems
  • Place of Presentation: 京都市国際交流会館, 京都
• [Remarks] 研究業績一覧
  • URL: http://www.kurims.kyoto-u.ac.jp/~sinya/research.html
• [Remarks] 研究業績一覧
  • URL: http://www.kurims.kyoto-u.ac.jp/~sinya/research.html