@article{oai:ipsj.ixsq.nii.ac.jp:00014318,
 author = {川田, 秀司 and 坂井, 公 and 藤田, 正幸 and 白井, 康之 and 大坪透 and Hideji, Kawata and Ko, Sakai and Masayuki, Fujita and Yasuyuki, Shirai and Toru, Ohtubo},
 issue = {1},
 journal = {情報処理学会論文誌},
 month = {Jan},
 note = {Curry-Howard Isomorphismに墓づくプログラム生成法では、諭理式に対しプログラムの仕様としての解釈を定義し、諭理式の証明から誤りのないプログラムの生成方式をあたえる。PAPYRUS（PArallel Programs sYnthesis by Reasoning Upon System）は、このような方法をべ一スとしたプログラム生成実験システムであり、大まかには以下の2つの機能を提供する。1つは、諭理や表記法、プログラム生成規則の管理と、これらの定義のもとでの証明チェックやプログラム生成の機能で、型諭理の1つであるCC（Calculus of Constructions）における型推諭機能とTRS（Term Rewriting System）の技術により実現される、これらの定議を変更することにより、プログラム生成のためのさまざまな諭理や表現方法、実現可能性解釈を利用することがで妻る。もう1つは、証明作成の簡単化を目的とする証明エディタ機能であり、（1）適用可能な推論規測の表示と、選択された規則による自動証明展開機能、（2）部分証明が構成されるたびに行われる自動証明チェック機能（この機能により完成した証明はその時点で正しさが保証される）、（3）未証明部をプルーバに証明させる機能などがある。本稿ではPAPYRUSの原理と構成、機能について述ぺる。},
 pages = {127--142},
 title = {プログラム生成システムPAPYRUS},
 volume = {35},
 year = {1994}
}