制御フローの合流のための計算系
スポンサーリンク
概要
- 論文の詳細を見る
本論文では,制御フローの合流を扱うための計算系を提案し,その計算系から導出される中間表現を構築する.制御フローの合流は,条件式などをコンパイルするうえで必須の機構である.たとえば,3 番地コードを用いた手続き型言語のコンパイラでは,条件式は,各分岐先のコードの実行の後,同一のラベルにジャンプするコードに翻訳される.しかしながら,関数型言語の中間表現として使用される継続渡し形式 (CPS) や A-正規形などでは,制御フローの合流の機構が含まれていないため,条件式などを機械的に翻訳すると,分岐の後に続く継続が各分岐に複製されてしまう.この問題は,それら中間表現に対応する計算系に,分岐後の制御フローの合流に相当する規則を追加することで解決できるはずである.本論文では,この洞察に基づき,著者の 1人によって示されたシーケント計算と A-正規形の対応を洗練し,論理和に対する左規則が唯一の前提(上式)を持つようなシーケント計算を構築する.この結果から,証明論的意味付けに立脚し,かつ制御フローの合流を取り扱うことができるコンパイラの中間表現と,その言語へのコンパイルアルゴリズムを導く.本論文の結果は関数型言語の実用的なコンパイラのより系統的な実現を可能にするものである. Standard ML の拡張言語である SML# のコンパイラの中間表現の 1 つは,この計算系に基づいて設計され,その中間言語へのコンパイルフェーズは本論文で示すコンパイルアルゴリズムを基礎に実装されている.
- 2008-10-27
著者
関連論文
- パネル討論会 : 理輪は実践を導けるか,実践は理論を生かせるか? : 第1回プログラミング : 言語・基礎・実践 研究会報告
- 高階遠隔手続き呼出しに基づいたC言語について (分散オペレーティングシステム)
- A-031 コンパイラ構築の証明論的枠組み(モデル・アルゴリズム・プログラミング,一般論文)
- Peter J. Denning : The Working Set Model for Program Behavior(20世紀の名著名論)
- 動的永続性へのアプローチ (高度データベース論文特集)
- 型付高階モーバイル言語の設計
- MLプログラミング入門(IV)
- MLプログラミング入門(III)
- MLプログラミング入門(II)
- MLプログラミング (I)
- ML : 多相型システムをもつ関数型言語 (プログラミング言語最新情報1)
- 第19回POPL
- 3. オブジェクト指向データベースの技術的諸問題 3.1 オブジェクト指向データベースの形式化 (オブジェクト指向データベースシステム)
- 3.SML#:最先端の機能と高い実用性を実現する次世代多相型プログラミング言語(第1部:高い生産性を持つ高信頼ソフトウェア作成技術の開発,学と産の連携による基盤ソフトウェアの先進的開発)
- 制御フローの合流のための計算系
- A-030 MLとC間の多相型外部関数インターフェース(モデル・アルゴリズム・プログラミング,一般論文)
- 3M-1 プログラミング言語SML#(リーディングプロジェクト e-society:高信頼プログラミング言語と構造化文書変換技術,一般セッション,リーディングプロジェクト e-society)