权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

定理証明システムによる型システムとプログラム変換の検証

使用定理证明系统验证类型系统和程序转换

基本信息

批准号：
13780193
负责人：
南出靖彦
金额：
$ 1.28万
依托单位：
University of Tsukuba
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2001
资助国家：
日本
起止时间：
2001 至 2002
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13780193/
关键词：
定理証明システム型システムプログラム変換操作的意味論

项目摘要

関数型プログラミング言語のコンパイラで用いられるCPS変換の定理証明システムIsabelle/HOLによる検証について二つの拡張を行った.まず,CPS変換がプログラムの実行に必要な記憶領域の大きさを保存することを検証した.証明すべき性質はより複雑なものになり,証明の長さも2倍程度になった.しかし,変換で導入される変数の形式化などは,記憶領域を考慮しない場合の形式化をそのまま応用することができ,自動証明を多くの補題の証明に用いることができた.次に,変換の検証を自由変数に含む式に拡張した.前年度の検証では,扱うプログラムが閉じた式であることを仮定し,証明を単純化した.しかし,前年度の証明を再検討したところ,この制限は証明の単純化にあまり貢献していないことがわかった.そこで,本年度には,この制限を取り除いて検証を行い,この制限が本質的でないことを確認した.関数型プログラミング言語の末尾呼び出しを,Java仮想機械などの末尾呼び出しを直接サポートしていない環境で効率的に実装するためのプログラム変換を提案した.末尾呼び出しをサポートしない環境でも,特殊な関数呼び出しの仕組みを用いることで,末尾呼び出しが実現できるが,そのような方法はオーバーヘッドが大きい.提案した方法では,型推論を用いてプログラムの末尾呼び出しに関する性質を推論する.その型情報に基づき,末尾呼び出しの正当な実装が必要な関数に対してだけ,選択的に,非効率的な末尾呼び出しの実装を用いることで,オーバーヘッドを抑えている.

A theorem for CPS transformation proves that Isabelle/HOL is the most important factor in the evolution of speech. In this case,CPS conversion is necessary for the implementation of the list of memory areas to be preserved. Prove that the property of The formalization of the number of entries is considered in the memory field. The formalization of the number of entries is used in the automatic proof of the number of entries. Second, the number of free changes in the number of changes. In the past year, the evidence has been verified, and the evidence has been verified. The proof of the previous year was re-examined, and the limit of the proof was purified. This year, the restrictions on the implementation of the test, the restrictions on the nature of the confirmation. The end of the speech is called out, and the end of the speech is called out directly by Java. The last call is for the environment, the special number is for the group, the last call is for the group, the method is for the group. The proposed method is used to deduce the properties of the proposed method. All types of information are based on the number of connections, the number of connections.