Research on program transformation systems based on automated theorem proving

基于自动化定理证明的程序转换系统研究

基本信息

  • 批准号:
    19500003
  • 负责人:
  • 金额:
    $ 2.41万
  • 依托单位:
  • 依托单位国家:
    日本
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
  • 财政年份:
    2007
  • 资助国家:
    日本
  • 起止时间:
    2007 至 2009
  • 项目状态:
    已结题

项目摘要

The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. This research aims to develop basic theories and prototypes for automated program transformation systems based on term rewriting theory. Concrete results include an automated construction method of program transformation templates, a new termination proof of higher-order programs, an automated lemma generation method for rewriting induction, an automated confluence prover of term rewriting systems.
术语重写系统的理论被广泛用于自动定理证明和计算模型的领域。这项研究旨在根据术语重写理论开发基本的理论和原型,以针对自动化程序转换系统。具体的结果包括一种自动化的程序转换模板的施工方法,一种新的终止终止证明,一种自动化的引理诱导方法,一种自动化的汇总诱导方法,是术语重写系统的自动化汇合摊贩。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Termination proof of S-expression rewriting systems with recursive path relations
具有递归路径关系的S-表达式重写系统的终止证明
  • DOI:
  • 发表时间:
    2008
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Alvarado CG;Maruyama S;Cheng J;Ida-Yonemochi H;Kobayashi T;Yamazaki M;Takagi R;Saku T;Yoshihito Toyama
  • 通讯作者:
    Yoshihito Toyama
Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
简单类型依赖对的参数过滤和可用规则
  • DOI:
  • 发表时间:
    2007
  • 期刊:
  • 影响因子:
    0
  • 作者:
    T. Aoto;T. Yamada
  • 通讯作者:
    T. Yamada
反証機能付き書き換え帰納法のための補題自動生成法
具有证伪功能的重写归纳法的自动引理生成方法
Proving Confluence of Term Rewriting Systems Automatically
  • DOI:
    10.1007/978-3-642-02348-4_7
  • 发表时间:
    2009-01-01
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Aoto, Takahito;Yoshida, Junichi;Toyama, Yoshihito
  • 通讯作者:
    Toyama, Yoshihito
Automatic Construction of Program Transformation Templates
程序转换模板的自动构建
{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

TOYAMA Yoshihito其他文献

TOYAMA Yoshihito的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('TOYAMA Yoshihito', 18)}}的其他基金

Research on automated confluence proving for term rewriting systems
术语重写系统自动汇合证明研究
  • 批准号:
    22500002
  • 财政年份:
    2010
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
Program verification method based on reduction approximations
基于约简近似的程序验证方法
  • 批准号:
    14580357
  • 财政年份:
    2002
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
Program verification based on higher order rewriting systems
基于高阶重写系统的程序验证
  • 批准号:
    07680347
  • 财政年份:
    1995
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)

相似海外基金

数学教育における変換の概念を取り入れた空間図形学習プログラムに関する研究
数学教育中融入转化理念的空间几何学习方案研究
  • 批准号:
    23K02454
  • 财政年份:
    2023
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
Finite Testing with Correctness Guarantee for Polymorphic Programs
多态程序正确性保证的有限测试
  • 批准号:
    23K11044
  • 财政年份:
    2023
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
作成中のプログラムを即時相互変換可能なプログラミング学習環境の開発とその教育応用
开发一个编程学习环境,允许立即转换正在创建的程序及其教育应用
  • 批准号:
    22K13765
  • 财政年份:
    2022
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Early-Career Scientists
テキストを実行可能なプログラムに変換するための基本技術の探究
探索将文本转换为可执行程序的基本技术
  • 批准号:
    22K19811
  • 财政年份:
    2022
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Challenging Research (Exploratory)
プログラム変換技術を活用する高性能科学技術計算向け高生産プログラミング環境
利用程序转换技术的高性能科学技术计算的高生产力编程环境
  • 批准号:
    20K11763
  • 财政年份:
    2020
  • 资助金额:
    $ 2.41万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了