Multi-Stage Programming with Dependent Types: Theory and Implementation

点击翻译按钮获取中文摘要

研究初年度となる２０２２年度は、本研究の基盤となる段階的計算体系において、計算リソース（メモリ量など）や生成されたコードのサイズ・性能などの量を扱うプログラム生成技法とその実例について調査を行った。特に、依存型を用いない従来型の型システムにおいてこれらの量的な情報をもとに質の高いプログラムを生成したりプログラム解析・検証を行った成功例について詳細に検討を行った。そのような研究の１つとして、亀山らが開発してきたプログラム生成・解析・検証を統一して行うフレームワークについて、暗号分野の適用事例をさらに洗練させて性能向上を果たした。特に、従来は、数論的変換関数だけの実装にとどまっていたのに対し、本研究では、多項式乗算など、より大きな関数を適用対象として、高性能コードの生成とその正しさの検証を同時に達成することに成功した。上記と並行して、コード重複を回避する段階的計算において重要となる計算エフェクトについて理論・実装の両面からの研究を行い、代数的エフェクトと限定継続コントロールオペレータの関係を解明したり、限定継続コントロールオペレータに関する統一的型システムを与えることに成功した。さらに、高性能コード生成において鍵となる技術の１つである「オフショアリング」の実装および応用例の作成を進めた。オフショアリングは、コード生成器を記述する高レベル言語と、生成されるコードを記述する低レベル言語の橋渡しをする技術であり、現代的な高性能コードの生成においては必須とされる技術である。段階的計算を実現するプログラミング言語MetaOCamlにオフショアリング機能を標準装備することに生成するとともに、C言語へのオフショアリングに関する従来手法において変数の取り扱いに問題がある事を発見して、改善手法を提案した。