• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

非述語的多相型付けを用いたプログラム融合変換

Research Project

Project/Area Number 17700012
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionKyoto University

Principal Investigator

西村 進  Kyoto University, 大学院・理学研究科, 准教授 (10283681)

Project Period (FY) 2005 – 2007
Project Status Completed (Fiscal Year 2007)
Budget Amount *help
¥2,500,000 (Direct Cost: ¥2,500,000)
Fiscal Year 2007: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2006: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2005: ¥1,100,000 (Direct Cost: ¥1,100,000)
Keywordsプログラム変換 / 関数融合 / プログラム論理 / 詳細化 / 型 / 論理
Research Abstract

ヒープに割り当てられたデータ構造の書き換えを含むプログラムの変換方法についての研究を行った。このようなプログラムはポインタの操作を直接的に扱わなければならないが、ポインタ操作を含むプログラムの変換はそうでないものの変換よりも格段に難しく、その変換手法については系統的なものはあまり知られていなかった。本年度の研究では、形式的技法の分野で研究されてきているプログラムの詳細化の手法を、ポインタやヒープに関する性質を記述するための論理体系のひとつであるSeparation Logicで拡張した。これによって、プログラム中のポインタ操作がすべて、Separation Logicにおける中核的な2種類の論理演算と対応するふたつの一般化されたポインタ操作の組み合わせで表せることが明らかとなった。これら二つの操作に関する変換規則を整備して適用することにより、ポインタ操作を含むプログラムの系統的な変換手法への糸口を見出した。またこの内容を定理証明系の上で実装し、これを用いて正しさの保証されたポインタ操作を含むプログラムの変換を行うことができることを示した。これらの結果は、いくつかの国内の研究集会で発表され、また2008年7月にフランスで開催される国際会議Mathematics of Program Construction(MPC'08)でも発表予定である。
また、勝股審也氏との共同研究による、モノイド準同型を用いた代数的手法に基づいた累積変数を持つ関数プログラムの融合変換手法についての共著論文が著名雑誌Journal of Functional Programmingに近日掲載されることが決定した。この論文は2006年に国際会議ICFP'06において発表したものを拡張しまとめたものである。

Report

(3 results)
  • 2007 Annual Research Report
  • 2006 Annual Research Report
  • 2005 Annual Research Report
  • Research Products

    (7 results)

All 2009 2008 2007 2006

All Journal Article (4 results) (of which Peer Reviewed: 1 results) Presentation (3 results)

  • [Journal Article] Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement2009

    • Author(s)
      Shin-ya Katsumata, Susumu Nishimura
    • Journal Title

      Journal of Functional Programming (2009年以降掲載予定)

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Reasoning about Data-Parallel Pointer Programs in a Modal Extension of Separation Logic2006

    • Author(s)
      Susumu Nishimura
    • Journal Title

      Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006 LNCS 4019

      Pages: 293-307

    • Related Report
      2006 Annual Research Report
  • [Journal Article] Algebraic Fusion of Functions with an Accumulating Parameter and its Improvement2006

    • Author(s)
      Shin-ya Katsumata, Susumu Nishimura
    • Journal Title

      ICFP'06: Proceedings of the 11th ACMSIGPLAN International Conference on Functional Programming

      Pages: 227-238

    • Related Report
      2006 Annual Research Report
  • [Journal Article] Verifying Data-Parallel Programs with Separation Logic2006

    • Author(s)
      Susumu Nishimura
    • Journal Title

      SPACE 2006 : Third workshop on semantics, program analysis and computing evironements for memory management (unofficial proceedings)

      Pages: 101-104

    • Related Report
      2005 Annual Research Report
  • [Presentation] Safe Modification of Pointer Programs in Refinement Calculus2008

    • Author(s)
      Susumu Nishimura
    • Organizer
      Ninth International Conference on Mathematics of Program Construction (MPC'08)
    • Place of Presentation
      CIRM, Marseille (Luminy), France
    • Related Report
      2007 Annual Research Report
  • [Presentation] Correct Transformation of Pointer Programs in an Extension of Refinement Calculus with Separation Logic2007

    • Author(s)
      西村 進
    • Organizer
      Theorem Proving and Provers (TPP) Meeting
    • Place of Presentation
      筑波大学
    • Year and Date
      2007-11-22
    • Related Report
      2007 Annual Research Report
  • [Presentation] ポインタを扱うプログラムのためのrefinement calculus2007

    • Author(s)
      西村 進
    • Organizer
      日本ソフトウェア科学会第24回大会
    • Place of Presentation
      奈良先端科学技術大学院大学
    • Year and Date
      2007-09-12
    • Related Report
      2007 Annual Research Report

URL: 

Published: 2005-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi