プログラミング言語自身を拡張する技術であるメタプログラミングは様々な形で実際のプログラミングに応用されているが、特に言語埋め込みのドメイン固有言語(Domain Specific Language, DSL)を実現する上で有用な技術である。その一方でメタプログラミングの理論的な性質については未だわかっていないことが多く、それゆえその安全性を保証する手法も発展途上である。我々はメタプログラミングの中でも特にプログラミング言語自身のコードを生成するようなものを型理論と呼ばれる理論的なモデルに落としこむことで安全なメタプログラミングを実現することを試みている。
本研究では文脈様相型理論として知られる型理論を多相の文脈という概念で拡張した新しい型理論λ∀[] を提案し、それが型理論としての基本的な性質を満たすことを証明した。また、既存の研究では線形時間時相論理をベースとした型理論λ○が知られているが、本研究ではこのλ○をλ∀[]へ型安全性を保ったまま埋め込めることを示すことで、我々の提案した体系が既存のものより真に広い範囲のメタプログラムをモデル化できることを示した。
本研究は安全なメタプログラミングを実現する上での基礎を与えるもので、ソフトウェアを使う産業一般に応用可能なものである。メタプログラミングは既に実際にITの広い分野で使われているが、その安全性を確立することでメタプログラミングを用いたプログラムの開発及び保守が容易となり、ソフトウェア開発者の生産性の向上に大いに貢献することが期待できる。
| 氏名 | 専攻 | 研究室 | 役職/学年 |
|---|---|---|---|
| 村瀬 唯斗 | 通信情報システム専攻 | 五十嵐・末永研究室 | 博士1回生 |
| 西脇 友一 | その他: その他 | その他: その他 | |
| 五十嵐 淳 | 通信情報システム専攻 | 五十嵐・末永研究室 | 教授 |