研究課題
2023年度は、依存型付き言語に対する型安全かつ効率的な CPS 変換を開発した。CPS 変換はすべての式を残りの計算（継続）を受け取る形に書き換えるプログラム変換であり、関数型言語のコンパイルに広く用いられている。申請者らの先行研究により、依存型を保存する CPS 変換が与えられているが、この変換は出力の型付けに独自の型規則を必要とするほか、変換の過程で余計な計算ステップを導入する。本研究では、これらの問題が起きない CPS 変換を開発した。具体的には、変換によって導入される変数が型に現れる場合にラムダ抽象ではなく let 文を用いることで、独自の型規則の必要性を回避した。さらに、項に対する補助的な変換を定義することで、計算ステップの増加を回避した。研究期間全体では、まず制御演算子 shift/reset を持つ依存型付き言語を Racket の Turnstile ライブラリを用いて実装した。次に、shift/reset と条件文を持つ依存型付き言語を形式化し、型安全性を保証しながら柔軟な型付けを許すにはどのように型システムを設計すれば良いかを検討した。また、shift/reset より複雑な振る舞いを持つ control/prompt に対して、最も一般的な型システムを定義した。さらに、制御演算子と類似した機能を持つ代数的エフェクトとハンドラにも着目し、安全な型システム、型保存コンパイラ、制御演算子との相互変換を開発した。これらの研究成果は、いずれも本研究課題の目標である信頼性と表現力の両立につながるものである。
すべて 2024 2023
すべて 雑誌論文 (2件) (うち査読あり 2件) 学会発表 (2件) (うち国際学会 2件、 招待講演 1件)
Proceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation
巻: N/A ページ: 134-145
10.1145/3635800.3636968
Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming
巻: N/A ページ: 1-13
10.1145/3610612.3610616
