A Study on Proof System That Combines Verification and Optimization Technologies

验证与优化技术相结合的证明系统研究

• 批准号: 19500021
• 负责人: OHORI Atsushi
• 金额: $ 2.66万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2008
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19500021/
• 关键词: プログラミング言語; コード最適化; コード検証; 証明論

直観主義的論理学の自然演繹証明システムとラムダ計算との同型関係を拡張・一般化し, 機械語コードの証明論を完成し, コードの最適化やコードの検証をより体系的に行う基礎を構築した。この証明論では, 機械語コードは, 左規則のみからなるある種のシーケント計算として表現され, その操作的意味, すなわち, コードを実行する機械の状態遷移規則は, シーケント計算のカット除去定理の証明から系統的に抽出することができる。さらに, この証明システムは, 低レベルコードのアクセス権限の検証や制御フロー遷移の最適化などの基礎となることが示された。

The natural deduction of the logic of directness proves that the theory of the system of the system The proof theory is that the mechanical state transition rule is that the left rule is that the left rule is that the right rule is that the left rule is that the right rule that the right rule is that the right rule that is that is that the right rule that is In addition, the proof system is based on the low cost model and the optimization of the migration model.

项目成果

型代入を遅延する髄化型推論アルゴリズム

延迟类型分配的髓鞘类型推断算法

• 发表时间: 2008
• 期刊: コンピュータソフトウェア 25
• 作者: 上野雄大;大堀淳
• 通讯作者: 大堀淳

A Proof Theory for Machine Code

机器代码的证明理论

• 发表时间: 2007
• 期刊: ACM Transactions on Programming Languages and Systems 29(6)
• 作者: N. Katoh;M. Ohsaki;T. Kinoshita;S. Tanigawa;D. Avis and I. Streinu;Atsushi Ohori
• 通讯作者: Atsushi Ohori

制御フローの合流のための計算系

控制流合并计算系统

• 发表时间: 2008
• 期刊: 情報処理学会論文誌プログラミング(PRO) 1
• 作者: 上野雄大;大堀淳
• 通讯作者: 大堀淳

型代入を遅延する最適化型推論アルゴリズム

延迟类型分配的优化类型推断算法

• 发表时间: 2008
• 期刊: コンピュータソフトウェア 25
• 作者: 上野雄大;大堀淳
• 通讯作者: 大堀淳