课题基金 / 基金详情

A Study on Proof System That Combines Verification and Optimization Technologies

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/
关键词：
プログラミング言語コード最適化コード検証証明論

项目摘要

项目成果

OHORI Atsushi的其他基金

相似基金

相关文献

中文摘要
翻译
直観主義的論理学の自然演繹証明システムとラムダ計算との同型関係を拡張・一般化し, 機械語コードの証明論を完成し, コードの最適化やコードの検証をより体系的に行う基礎を構築した。この証明論では, 機械語コードは, 左規則のみからなるある種のシーケント計算として表現され, その操作的意味, すなわち, コードを実行する機械の状態遷移規則は, シーケント計算のカット除去定理の証明から系統的に抽出することができる。さらに, この証明システムは, 低レベルコードのアクセス権限の検証や制御フロー遷移の最適化などの基礎となることが示された。
英文摘要
直観主義的論理学の自然演繹証明システムとラムダ計算との同型関係を拡張・一般化し, 機械語コードの証明論を完成し, コードの最適化やコードの検証をより体系的に行う基礎を構築した。この証明論では, 機械語コードは, 左規則のみからなるある種のシーケント計算として表現され, その操作的意味, すなわち, コードを実行する機械の状態遷移規則は, シーケント計算のカット除去定理の証明から系統的に抽出することができる。さらに, この証明システムは, 低レベルコードのアクセス権限の検証や制御フロー遷移の最適化などの基礎となることが示された。
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
型代入を遅延する髄化型推論アルゴリズム
延迟类型分配的髓鞘类型推断算法
DOI： --
发表时间： 2008
期刊： コンピュータソフトウェア 25
影响因子： --
作者： [上野雄大, 大堀淳]
通讯作者： 大堀淳
A Proof Theory for Machine Code
机器代码的证明理论
DOI： --
发表时间： 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
制御フローの合流のための計算系
控制流合并计算系统
DOI： --
发表时间： 2008
期刊： 情報処理学会論文誌プログラミング(PRO) 1
影响因子： --
作者： [上野雄大, 大堀淳]
通讯作者： 大堀淳
型代入を遅延する最適化型推論アルゴリズム
延迟类型分配的优化类型推断算法
DOI： --
发表时间： 2008
期刊： コンピュータソフトウェア 25
影响因子： --
作者： [上野雄大, 大堀淳]
通讯作者： 大堀淳
Basic research on implementation technology for making SML# a practical polymorphic language
  • 批准号：
    25280019
  • 项目类别：
    Grant-in-Aid for Scientific Research (B)
  • 资助金额：
    $5.24万
  • 财政年份：
    2013
  • 负责人：
    OHORI Atsushi
  • 依托单位：
    Tohoku University
A Study on Proof-Theoretical Foundations for Compiler Construction
  • 批准号：
    22500023
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $2.41万
  • 财政年份：
    2010
  • 负责人：
    OHORI Atsushi
  • 依托单位：
    Tohoku University
A Framework for Integrating Programming Languages, Repository and Development Environment
PROOF-THEORETICAL INVESTIGATION ON MACHINE CODE AND CODE GENERATION
海外基金