文献

J-GLOBAL ID：201202209377781302   整理番号：12A0763729

評価による正規化のコンパイル型実装

A compiled implementation of normalisation by evaluation

著者 (3件)： AEHLIG Klaus (Ludwigs-Maximilians-Univ. Muenchen) ,  HAFTMANN Florian (Technische Univ. Muenchen) ,  NIPKOW Tobias (Technische Univ. Muenchen)
資料名： Journal of Functional Programming  (Journal of Functional Programming)
巻： 22  号： 1  ページ： 9-30  発行年： 2012年01月 
JST資料番号： W1589A  ISSN： 0956-7968  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： イギリス (GBR)  言語： 英語 (EN)

抄録/ポイント： 書換えルールに関する用語の記号的正規化は定理証明器の中心的タスクとなっており,定理証明器の中には極めて効率的な正規化器を提供しているものが存在している。これに対し本論文では,ML類似言語に対し,評価による正規化(NBE)のコンパイル型実装を提案し,新しいアプローチを提示した。関数型言語であうML言語におけるNBEの問題を取り上げ,MLにおけるλ計算,関数変換,などについて述べた。この方式をIsabelle/HOLの中でのモデリングおよび検証を行い,その中で,リダクション,コンパイレーション,健全性,などに関する議論を行った。Isabelle/HOLの中での実現を試み,拡張方式として,非左側線形ルール,ケース組合せ子,について論じた。また,このNBEの実装により,NBEがIsabelleにおける証明ルールに変換される方法について論じた。

シソーラス用語： *ML言語 ,  *コンパイラ ,  *書換え規則 ,  実装設計 ,  正規化 ,  定理証明 ,  健全性 ,  高階論理 ,  規則 ,  モデリング ,  モデル検査
準シソーラス用語： ルール

分類 (3件)： 汎用プログラミング言語  (JD03051H) ,  言語プロセッサ  (JD03040F) ,  計算理論  (JB02000A)

タイトルに関連する用語 (4件)： 評価 ,  正規化 ,  コンパイル ,  実装