文献

J-GLOBAL ID：201202222798906593   整理番号：12A1689822

ストリーム上の共再帰を用いた純粋型システム 有限から無限への正規化

Pure Type Systems with Corecursion on Streams From Finite to Infinitary Normalisation

著者 (2件)： SEVERI Paula (Univ. Leicester, GBR) ,  DE VRIES Fer-Jan (Univ. Leicester, GBR)
資料名： ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages)  (ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages))
巻： 47  号： 9  ページ： 141-152  発行年： 2012年09月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 本論文において,筆者らは再帰方程式によって定義されたストリームを含むプログラムが正しく振る舞う事を保証するために型を使用する事に興味を持っている。純粋型システム(PTSs)は一様な方法において幾つかの現存する型付きλ計算を定義するフレームワークである。筆者らはあるPTSの疑似項の集合を拡張する事によって共再帰を用いた純粋型システム(CoPTSs)を定義した。CoPTSsは唯一のフレームワークを用いた共再帰を用いて拡張した幅広い範囲の型付きλ計算の研究を可能とする。筆者らはCoPTSsに対する無限(弱)正規化及び無限強正規化の特性を研究した。型付きλ計算の無限弱正規化の証明は全ての型付け可能プログラムが正しく振る舞う事を保証する方法である。

シソーラス用語： 型 ,  *λ計算 ,  *抽象データ型 ,  再帰性 ,  型理論 ,  次元 ,  *正規化 ,  様相論理
準シソーラス用語： *ストリーム【プログラミング】 ,  *型システム ,  無限次元

分類 (1件)： 言語プロセッサ  (JD03040F)

タイトルに関連する用語 (4件)： ストリーム ,  型システム ,  無限 ,  正規化