课题基金 / 基金详情

プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成

プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成
程序分析统一理论的构建与验证以及基于该理论的分析仪自动综合
批准号：
14702063
负责人：
小林 直樹
金额：
$9.65万
依托单位：
Tohoku University (2004)Tokyo Institute of Technology (2002-2003)
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (A)
财政年份：
2002
资助国家：
日本
项目状态：
已结题
起止时间：
2002 至 2004
来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-14702063/
关键词：
型システムプログラム解析定理証明支援器Coqプログラム抽出構成的プログラミング

项目摘要

项目成果

小林 直樹的其他基金

相似基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
本研究では、プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し、さらにそれに基づき、構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.1.プログラム解析のための統一型理論の拡張・改良種々のプログラム解析を統一的に扱うための型システムとして、これまで研究してきた計算機資源使用法解析および並行プログラムの解析を拡張するとともに、並行プログラム解析器TyPiCalを実装し、そのソースプログラムをホームページ上で公開した.2.型理論に基づくプログラム解析器の抽出実験正しいプログラム解析器を自動抽出するための実験として、昨年に引き続き、一部をパラメータ化した汎用的型システムライブラリの定理証明支援器Coq上での定式化を行い、その上に単純型付きラムダ計算の定式化を行って汎用ライブラリの有効性を確かめた.昨年度に比べ、準同型写像を使ったライブラリ部分の拡充を行うなどしてライブラリの完成度を高めた.3.並行プログラムの検証のためのCoq用ライブラリの構築並行プログラムを定理証明器上で検証するためのCoq用ライブラリの作成を行った.今後は上記1番目の項目の並行プログラムの型に基づく解析の定式化を本ライブラリに組み込んでいく予定である.
期刊论文(15)
专著(0)
科研奖励(0)
会议论文
Naoki Kobayashi: "A Type System for Lock-Free Processes"Information and Computation. 177. 122-159 (2002)
Naoki Kobayashi：“无锁进程的类型系统”信息和计算。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type
基于有序线性类型的树处理程序转化为流处理程序
DOI： --
发表时间： 2008
期刊： Journal of Functional Programming (出版決定)
影响因子： --
作者： [Koichi Kodama, Kohei Suenaga and Naoki Kobayashi]
通讯作者： Kohei Suenaga and Naoki Kobayashi
A generic type system for the Pi-calculus
DOI： 10.1016/s0304-3975(03)00325-6
发表时间： 2004-01-23
期刊： THEORETICAL COMPUTER SCIENCE
影响因子： 1.1
作者： [Igarashi, A, Kobayashi, N]
通讯作者： Kobayashi, N
R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security - Theories and Systems, Springer LNCS. 2609. 217-233 (2003)
R.Affeldt、N.Kobayashi：“Coq 中邮件服务器的验证”软件安全 - 理论和系统，Springer LNCS。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
共 15 条
    無住道暁と南宋代成立典籍に関する総合的研究
    • 批准号：
      23K00298
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $1.41万
    • 财政年份：
      2023
    • 负责人：
      小林 直樹
    • 依托单位：
      Osaka Metropolitan University
    潜在的カビ毒産生菌種を利用したカビ毒生合成抑制メカニズムの解明
    • 批准号：
      23K05081
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $2.91万
    • 财政年份：
      2023
    • 负责人：
      小林 直樹
    • 依托单位：
      Azabu University
    偏光分光型マルチスペクトルカメラを用いた目視診断用画像システムの研究開発
    • 批准号：
      23K11878
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $3.08万
    • 财政年份：
      2023
    • 负责人：
      小林 直樹
    • 依托单位：
      Saitama Medical University
    Program Verification Based on Higher-Order Fixpoint Logic
    • 批准号：
      20H00577
    • 项目类别：
      Grant-in-Aid for Scientific Research (A)
    • 资助金额：
      $28.45万
    • 财政年份：
      2020
    • 负责人：
      小林 直樹
    • 依托单位：
      The University of Tokyo
    海外基金