首页    期刊浏览 2024年11月05日 星期二
登录注册

文章基本信息

  • 标题:Isomorphism of "Functional" Intersection Types
  • 本地全文:下载
  • 作者:Mario Coppo ; Mariangiola Dezani-Ciancaglini ; Ines Margaria
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2014
  • 卷号:26
  • 页码:129-149
  • DOI:10.4230/LIPIcs.TYPES.2013.129
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Type isomorphism for intersection types is quite odd, since it is not a congruence and it does not extend type equality in the standard interpretation of types. The lack of congruence is due to the proof theoretic nature of the intersection introduction rule, which requires the same term to be the subject of both premises. A partial congruence can be recovered by introducing a suitable notion of type similarity. Type equality in standard models becomes included in type isomorphism whenever atomic types have "functional" interpretations, i.e. they are equivalent to arrow types. This paper characterises type isomorphism for a type system in which the equivalence between atomic types and arrow types is induced by the initial projections of the Scott's model via the correspondence between inverse limit models and filter lambda-models.
  • 关键词:Type Isomorphism; Lambda calculus; Intersection Types
国家哲学社会科学文献中心版权所有