The confluent terminating context-free substitutive rewriting system for the lambda-calculus with surjective pairing & terminal type

研究成果: Conference contribution

抄録

For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo, inspired by Knuth-Bendix completion, introduced a confluent rewriting system of the naive rewriting system. Their system is a confluent (CR) rewriting system stable under contexts. They left the strong normalization (SN) of their rewriting system open. By Girard's reducibility method with restricting reducibility theorem, we prove SN of their rewriting, and SN of the extensions by polymorphism and (terminal types caused by parametric polymorphism). We extend their system by sum types and eta-like reductions, and prove the SN. We compare their system to type-directed expansions.

本文言語English
ホスト出版物のタイトル2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
編集者Dale Miller
出版社Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN(電子版)9783959770477
DOI
出版ステータスPublished - 2017 9 1
イベント2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 - Oxford, United Kingdom
継続期間: 2017 9 32017 9 9

出版物シリーズ

名前Leibniz International Proceedings in Informatics, LIPIcs
84
ISSN(印刷版)1868-8969

Other

Other2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
国/地域United Kingdom
CityOxford
Period17/9/317/9/9

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「The confluent terminating context-free substitutive rewriting system for the lambda-calculus with surjective pairing & terminal type」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル