Implementing a Reliable and Expressive Programming Language

2023 Fiscal Year Final Research Report

• Project/Area Number: 19K24339
• Research Category: Grant-in-Aid for Research Activity Start-up
• Allocation Type: Multi-year Fund
• Review Section: 1001:Information science, computer engineering, and related fields
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: Cong Youyou 東京工業大学, 情報理工学院, 助教 (30847629)
• Project Period (FY): 2019-08-30 – 2024-03-31
• Keywords: 依存型 / 代数的効果 / 制御演算子

Outline of Final Research Achievements

I developed type systems and program transformations for calculi that have constructs for manipulating continuations. Examples include a type system that can describe the detailed behavior of control operators, a simple type system that ensures safe use of named effect handlers, and program translations that convert between control operators and effect handlers. I also implemented a dependently typed language with effect handlers based on the type systems and program translations I developed and using the Turnstile package of the Racket language.

Free Research Field

プログラミング言語

Academic Significance and Societal Importance of the Research Achievements

型システムと継続機構はそれぞれプログラムの信頼性とプログラミング言語の表現力の向上に有用である。実際、研究期間中にさまざまなプログラミング言語のコミュニティで強力な型システムやプリミティブの継続機構を導入する動きが見られた。本研究ではこれらの基礎理論を構築したが、その中で得られた成果は安全なソフトウェアの簡潔な実装につながると考えられる。