On typability for rank-2 intersection types with polymorphic recursion

Tachio Terauchi*, Alex Aiken

*この研究の対応する著者

研究成果: Conference contribution

3 被引用数 (Scopus)

抄録

We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a context free language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problem for Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the Milner-Mycroft type system. We also show undecidability of a related program analysis problem.

本文言語English
ホスト出版物のタイトルProceedings - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
ページ111-120
ページ数10
DOI
出版ステータスPublished - 2006
外部発表はい
イベント21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006 - Seattle, WA, United States
継続期間: 2006 8月 122006 8月 15

出版物シリーズ

名前Proceedings - Symposium on Logic in Computer Science
ISSN(印刷版)1043-6871

Other

Other21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
国/地域United States
CitySeattle, WA
Period06/8/1206/8/15

ASJC Scopus subject areas

  • ソフトウェア
  • 数学 (全般)

フィンガープリント

「On typability for rank-2 intersection types with polymorphic recursion」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル