Semantics for Implementations of Programming Languages

• Project/Area Number: 15K00013
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Kyoto University
• Principal Investigator: Hasegawa Masahito 京都大学, 数理解析研究所, 教授 (50293973)
• Project Period (FY): 2015-04-01 – 2018-03-31
• Project Status: Completed (Fiscal Year 2017)
• Budget Amount: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000); Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2016: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2015: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
• Keywords: プログラミング言語 / 意味論 / 圏論 / 位相的量子計算 / 遅延評価 / 線型論理 / 線形論理

Outline of Final Research Achievements

We studied semantics of programming languages focussing on the implementation models. In particular, we developed categorical approach to such semantics and obtained the following results. (1) We introduced linear exponential comonads on non-symmetric monoidal categories. (2) We studied fundamental propeorties of traced monoidal categories and gave a partial solution to the embeddability into traced categories. (3) We gave a new theorem for the embedding from traced categories into compact closed categories and applied it to derive a new translation from the linear lambda calculus for classical linear logic to the lambda calculus with cyclic sharing.

Research Products

• [Journal Article] Linear Exponential Comonads without Symmetry (2016)
  • Author(s): Masahito Hasegawa
  • Journal Title: Electronic Proceedings in Theoretical Computer Science Volume: 238 Pages: 54-63
  • DOI: 10.4204/eptcs.238.6
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Presentation] From Linear Logic to Cyclic Sharing (2018)
  • Author(s): 長谷川真人
  • Organizer: 理論計算機科学と圏論ワークショップ（CSCAT2018）
• [Presentation] On traced *-autonomous categories (2017)
  • Author(s): 長谷川真人
  • Organizer: 計算機科学と圏論研究集会
  • Place of Presentation: 群馬大学 (群馬県前橋市)
  • Year and Date: 2017-03-21
• [Presentation] Free Traces on Symmetric Monoidal Categories (2017)
  • Author(s): 長谷川真人
  • Organizer: 代数, 論理, 幾何と情報科学研究集会（ALGI2017）
• [Presentation] On Semi-duals in Monoidal Categories (2017)
  • Author(s): Masahito Hasegawa
  • Organizer: CRECOGI Annual Meeting
• [Presentation] Traced star-autonomoud categories are compact closed (2016)
  • Author(s): Masahito Hasegawa
  • Organizer: Seminaire Preuves, Programmes et Systeme
  • Place of Presentation: Paris (France)
  • Year and Date: 2016-10-18
• [Presentation] Linear Exponential Comonads without Symmetry (2016)
  • Author(s): Masahito Hasegawa
  • Organizer: Fourth International Workshop on Linearity (LINEARITY 2016)
  • Place of Presentation: Porto (Portugal)
  • Year and Date: 2016-06-25
  • Int'l Joint Research
• [Presentation] Linear exponential comonads without symmetry (2016)
  • Author(s): Masahito Hasegawa
  • Organizer: 理論計算機科学と圏論ワークショップ
  • Place of Presentation: 理化学研究所（兵庫県神戸市）
  • Year and Date: 2016-03-16
• [Presentation] A conjecture on traced monoidal categories (2015)
  • Author(s): Masahito Hasegawa
  • Organizer: Concurrent, Resourceful and Effectful Computation, by Geometry of Interaction
  • Place of Presentation: 京都大学（京都府京都市）
  • Year and Date: 2015-07-11
  • Int'l Joint Research
• [Remarks] Masahito Hasegawa's Research
  • URL: http://www.kurims.kyoto-u.ac.jp/~hassei/papers/index.html
• [Funded Workshop] 30th Annual ACM/IEEE Symposium on Logic in Computer Science (2015)
  • Place of Presentation: グランドプリンスホテル京都（京都府京都市）
  • Year and Date: 2015-07-06