階層化コントロールオペレータに対する型システムの構築
スポンサーリンク
概要
- 論文の詳細を見る
本論文は,関数型プログラム言語におけるコントロールオペレータを対象とし,これに対する型システムの構築とその性質について述べる.本論文で対象とするshift/resetは,限定継続を操作するコントロールオペレータであり,その意味がCPS変換に基づいて厳密に定義されているため,形式的に扱いやすいという特徴がある.shift/resetは様々な制御構造を表現できるが,複数の異なる目的でshift/resetを用いると,それぞれのshift/resetが干渉しあい,プログラマの意図どおりにプログラムが実行されない場合がある.そこで,それぞれのshift/resetを区別するため,shift/resetに自然数のレベルを付与して階層化することが提案されている.階層化shift/resetに対して,これまで,型システムやその性質について十分には検討されておらず,MLなどの型を特つプログラム言語に階層化shift/resetを直接導入することはできなかった.我々は,先行研究において,レベル2のshift/resetの型システムを構築したが,この方式では,1つの項の型付けにおいて,レベルの指数関数の個数の型を必要とするため,レベル3以上の型システムに拡張することは困難であった.本論文では,任意レベルの階層化shift/resetに対する型システムを提案し,型システムの健全性などの望ましい性質が成立することを示す.これにより,型があるプログラム言語に階層化shift/resetを導入できるようになると考えられる.
- 一般社団法人情報処理学会の論文
- 2007-06-15
著者
関連論文
- 二階文脈計算(プログラミング及びプログラミング言語)
- 定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
- 自己反映的証明体系RPTの理論と実現
- 抽象化と精密化による実時間モデル検査の改善
- 多値モデル検査を利用したモデル化の誤りの発見
- 限定継続に基づくスケーラブルなウェブアプリケーション構築手法
- 1Q-5 マルチステージプログラミングのための計算体系の実装(プログラミング言語・実装・支援,学生セッション,ソフトウェア科学・工学)
- 動的環境と限定継続を持つプログラム言語の意味論と実装
- オブジェクト指向言語に対するメタプログラミング言語の設計と実装
- 階層化コントロールオペレータに対する型システムの構築
- 構成的数学体系RPTに基づく超数学の定理の形式化
- 結果型を変更可能な限定継続の模倣