A Type-Free Context Calculus

AzzaA.Taha, Sato, Masahiko, 亀山, 幸義

A Type-Free Context Calculus

機関リポジトリ情報処理学会 HANDLE Web Site 参考文献10件オープンアクセス

書誌事項

タイトル別名

プログラム理論 A Type-Free Context Calculus
プログラムリロン A Type Free Context Calculus

この論文をさがす

抄録

This paper develops a type free context calculus lxc. The calculus lxc includes contexts as first-class values andhole-filling as an explicit operation. In lxc holes arerepresented by ordinary variables and hole-filling is represented bythe usual application together with a new abstraction mechanism whichrepresents the variables intended to be bound after filling in thehole. We show that this calculus has desirable properties such asconfluence conservativity over lambda beta calculus and has thepreservation of strong normalization (PSN) property.

This paper develops a type free context calculus lxc. The calculus lxc includes contexts as first-class values andhole-filling as an explicit operation. In lxc, holes arerepresented by ordinary variables and hole-filling is represented bythe usual application together with a new abstraction mechanism whichrepresents the variables intended to be bound after filling in thehole. We show that this calculus has desirable properties such asconfluence, conservativity over lambda beta calculus and has thepreservation of strong normalization (PSN) property.