定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
スポンサーリンク
概要
- 論文の詳細を見る
仕様からプログラムを開発する際, 抽象的な仕様を具体的なプログラムへ変換することが行われている.抽象的な仕様には, 用いるプログラミング言語では与えられていないデータ構造が含まれている可能性があり, 具体的なプログラムとは, それらのデータ構造が実現されたプログラムである.このような変換のことを"詳細化"と呼ぶ.Honsellは, Pre Logical Relationを用いる, 詳細化の正しさの証明技法を提案した.本研究では, 定理証明システムCoqを用いて彼らの技法を形式化した.このことより, 計算機上でプログラムの詳細化の正しさを厳密に証明することができる.
- 社団法人情報処理学会の論文
- 2001-11-15
著者
-
佐藤 雅彦
京都大学大学院情報学研究科
-
永山 友和
京都大学大学院情報学研究科
-
亀山 幸義
京都大学大学院情報学研究科
-
亀山 幸義
筑波大
-
亀山 幸義
筑波大学システム情報工学研究科
-
佐藤 雅彦
Department Of Information Science Faculty Of Science University Of Tokyo
-
Sato Masahiko
Graduate School Department Of Mathematics Kyoto University
-
Sato Masahiko
Department Of Information Science Kyoto University
-
佐藤 雅彦
京都大学大学院エネルギー科学研究科
関連論文
- 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)
- フレーゲの計算機科学への影響 (特集 フレーゲの現代性)
- 数学記号の認知速度 : 実験心理学的計測方法と実例
- Polyvariant Specializationon Type-directed Partial Evaluation
- Constructive Data Refinementの証明技法の改善
- 二階文脈計算(プログラミング及びプログラミング言語)
- 定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
- 型情報を一部明示した環境計算体系
- A Second Order Typed Context Calculus
- 型付きλ計算の拡張によるMobile計算の定式化
- オメガ正規言語の測度が有理数であること
- プログラム理論 A Type-Free Context Calculus
- 適切さの論理を用いた帰納論理プログラミング
- 発見科学の構想と展開(発見科学)
- 参照透明な代入を持つ純関数型言語
- 自己反映的証明体系RPTの理論と実現
- ソフトウェア科学会第3回大会
- 抽象化と精密化による実時間モデル検査の改善
- 多値モデル検査を利用したモデル化の誤りの発見
- 17aRA-6 非線形抵抗性壁モードのモデリング
- 構成的理論に基づいたプログラミング言語Zとその実装
- 限定継続に基づくスケーラブルなウェブアプリケーション構築手法
- $\lambda_C$計算と$\lambda_P$計算との対応(計算理論とその応用)
- 22pXG-13 負磁気シアートカマクにおける非線形ダブルテアリングモード
- 1Q-5 マルチステージプログラミングのための計算体系の実装(プログラミング言語・実装・支援,学生セッション,ソフトウェア科学・工学)
- 情報学科シンポジウム
- A Formal Theory of Symbolic Expressions(LOGIC AND THE FOUNDATIONS OF MATHEMATICS)
- Algebraic Structure of Symbolic Expressions (Mathematical Studies of Information Processing)
- ニセ金発見パズルについて (計算機によるパズル・ゲームの研究)
- On Formal Fractions Associated with the Symmetric Groups (組合せ構造とグラフ理論)
- 2個の生成元を持つFree IN-Algebra及びFree ICN-Algebraの決定 (数理論理とモデル理論)
- Lゲームの計算機による分類 (計算機によるゲームとパズルをめぐる諸問題研究会報告集)
- Nonlinear Double Tearing Mode in Negative Shear Cylindrical Tokamaks
- 動的環境と限定継続を持つプログラム言語の意味論と実装
- Classical Brouwer-Heyting-Kolmogorov interpretation
- オブジェクト指向言語に対するメタプログラミング言語の設計と実装
- 階層化コントロールオペレータに対する型システムの構築
- 構成的数学体系RPTに基づく超数学の定理の形式化
- A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability(Type Theory and its Applications to Computer Systems)
- On the Periods of Certain Pseudorandom Sequences
- ACUTE MYOCARDIAL INFARCTION IN FUKUSHIMA AREA OF JAPAN
- 結果型を変更可能な限定継続の模倣
- Nonlinear Double Tearing Mode in Negative Shear Cylindrical Tokamaks
- 8aSS-1 簡約化MHDモデルによる新古典テアリングモードの解析((理論・数値解析),磁場閉じ込め,領域2)