WEKO3
アイテム
項書換による証明付き最適化
https://ipsj.ixsq.nii.ac.jp/records/232258
https://ipsj.ixsq.nii.ac.jp/records/2322582d7e355b-fe5f-4e57-ad00-96bdb241d0ed
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2020005.pdf (203.6 kB)
|
Copyright (c) 2020 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2020-01-10 | |||||||
| タイトル | ||||||||
| タイトル | 項書換による証明付き最適化 | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 形式検証，Coq，項書換，最適化 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| マサチューセッツ工科大学 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Massachusetts Institute of Technology | ||||||||
| 著者名 |
池渕, 未来
× 池渕, 未来
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | プログラムの最適化には，たとえばshort cut fusionのように項書換として実現できるものが多くある．書換による最適化が実用されている例として，HaskellのコンパイラであるGHCは，Haskellプログラムに対してプログラマの指定した書換規則を適用し最適化する機能を持つ． 一方，証明支援系Coqは自動証明機能の一環として，等式証明のための自動的な書換の機能を持っている．今回の発表では，その機能を利用してCoqで記述されたプログラムを最適化する方法について示す．この方法ではプログラムは最適化されるだけではなく，最適化前のプログラムと最適化後のプログラムが同じ振舞いをすることが自動的に証明され，最適化の安全性が保証される．具体例として，リストを操作する関数に対する簡単な書換規則による最適化や，さらに高速フーリエ変換の一般的な場合に対する実装から特別な場合での効率的な実装の導出を見る． |
|||||||
| 書誌情報 |
第61回プログラミング・シンポジウム予稿集 巻 2020, p. 19-22, 発行日 2020-01-10 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
