Intersection-types a la church

• 全文链接
• 请求原文
• 全文直达

作   者：

Liquori L;  Della Rocca SR; 

作者机构：

I-10124 Turin;  Italy;  Univ Turin;  Dipartimento Informat; 

关键词：

ASSIGNMENT;  lambda-Calculus a la Curry and a la Church;  logics and intersection-types; 

期刊名称：

Information & Computation

i s s n：

0890-5401

年卷期：

2007 年 205 卷 9 期

页   码：

1371-1386

页   码：

摘   要：

In this paper, we present Lambda(t)(Lambda), a fully typed lambda-calculus based on the intersection-type system discipline, which is a counterpart a la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Lambda(t)(Lambda) and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover, both type checking and type reconstruction are decidable. (c) 2007 Elsevier Inc. All rights reserved.