@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00232258,
 author = {池渕, 未来},
 book = {第61回プログラミング・シンポジウム予稿集},
 month = {Jan},
 note = {プログラムの最適化には，たとえばshort cut fusionのように項書換として実現できるものが多くある．書換による最適化が実用されている例として，HaskellのコンパイラであるGHCは，Haskellプログラムに対してプログラマの指定した書換規則を適用し最適化する機能を持つ．
一方，証明支援系Coqは自動証明機能の一環として，等式証明のための自動的な書換の機能を持っている．今回の発表では，その機能を利用してCoqで記述されたプログラムを最適化する方法について示す．この方法ではプログラムは最適化されるだけではなく，最適化前のプログラムと最適化後のプログラムが同じ振舞いをすることが自動的に証明され，最適化の安全性が保証される．具体例として，リストを操作する関数に対する簡単な書換規則による最適化や，さらに高速フーリエ変換の一般的な場合に対する実装から特別な場合での効率的な実装の導出を見る．},
 pages = {19--22},
 publisher = {情報処理学会},
 title = {項書換による証明付き最適化},
 volume = {2020},
 year = {2020}
}