文献

J-GLOBAL ID：200902287656234945   整理番号：09A0986799

プログラム運算のためのCoqライブラリ

著者 (5件)： 橋本英樹 (東大 大学院情報理工学系研究科) ,  HU Zhenjiang (国立情報学研) ,  TESSON Julien (Univ. Orleans) ,  LOULERGUE Frederic (Univ. Orleans) ,  武市正人 (東大 大学院情報理工学系研究科)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 26th  ページ： ROMBUNNO.4C-3  発行年： 2009年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： プログラム運算は,プログラムを,その意味を変えない運算規則(定理)を用いて,より効率のよいプログラムに書き換えていくプログラミング手法である。プログラム運算のよい特徴として,運算前のプログラムが自明に正しいプログラムであれば,運算後のプログラムも意味を保存しているため検証が不要であり,正しく効率のよいプログラムの開発に利用しうることがあげられる。本研究で,我々は定理証明支援系Coqのライブラリとしてプログラム運算を支援するシステムを構築した。これを用いて,ユーザーは証明された定理のみを用いて安全にプログラム運算を行うことができる。また,我々は応用として,Birdによるプログラム運算のレクチャーノートを表現した。リスト上の関数のための運算規則を証明し,プログラム運算を我々のライブラリを用いてCoqで表現した。本発表では,上記のプログラム運算支援システム,および応用例の実装を紹介する。(著者抄録)

シソーラス用語： *プログラム変換 ,  *計算機プログラミング ,  プログラムの正しさ ,  意味論 ,  *定理証明 ,  ライブラリ【計算機】 ,  安全性 ,  規則 ,  実装設計
準シソーラス用語： Coq ,  *プログラム運算 ,  運算規則

分類 (3件)： 言語プロセッサ  (JD03040F) ,  計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

タイトルに関連する用語 (1件)： ライブラリ