プログラムに対する変換の正しさの形式検証

• 吉原 宏之

  筑波大学理工学研究科

• 亀山 幸義

  筑波大学システム情報工学研究科

抄録

本研究の目的は，定理証明システム Twelf を用いてλ計算に基づくプログラム言語で書かれた，プログラムに対する変換の性質を形式的に証明することである．プログラム変換に関する形式検証は，λ抽象を含む高階のデータを正しく扱う必要があるため，一階のデータを扱うプログラムの検証に比べて困難である．変数束縛を持つデータ構造を表現するために，高階抽象構文 (HOAS) と呼ばれる表現法があり，高階抽象構文をサポートする定理証明システムとしてTwelf がある．本研究では，プログラム変換の一種として，CPS 変換 (継続渡し方式への変換)を取り上げ，その健全性と完全性を Twelf で厳密に証明することを試みた．本発表では，この形式証明の手法について述べ，Twelf における高階抽象構文を用いたことによる問題点と解決法を述べる．

収録刊行物

• 日本ソフトウェア科学会大会講演論文集

  日本ソフトウェア科学会大会講演論文集 22 (0), 491-500, 2005

  日本ソフトウェア科学会

キーワード

• ラムダ計算
• 形式検証
• CPS変換
• 高階抽象構文
• ロジカルフレームワーク

詳細情報

• CRID: 1390282680500031616
• NII論文ID: 130004638905
• DOI: 10.11309/jssstconference.22.0.491.0
• ISSN: 13493515
• 本文言語コード: ja
• データソース種別:
  • JaLC
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可