INTERSECTION TYPES FOR lambda(Gtz)-CALCULUS

被引：0
|
作者：
Ghilezan, Silvia [1 ]
Ivetic, Jelena [1 ]
机构：
[1] Univ Novom Sadu, Fak Tehnickih Nauka, Trg Dositeja Obradovica 6, Novi Sad 21000, Serbia
来源：
PUBLICATIONS DE L INSTITUT MATHEMATIQUE-BEOGRAD | 2007年 / 82卷 / 96期
关键词：
D O I：
10.2298/PIM0796085G
中图分类号：
O29 [应用数学];
学科分类号：
070104 ;
摘要：
We introduce an intersection type assignment system for Espirito-Santo's lambda(Gtz)-calculus, a term calculus embodying the Curry-Howard correspondence for the intuitionistic sequent calculus. We investigate basic properties of this intersection type system. Our main result is Subject reduction property.
引用
收藏
页码：85 / 91
页数：7
相关论文
共 50 条
  • [21] INHABITATION OF TYPES IN THE SIMPLY TYPED LAMBDA-CALCULUS
    DEKKERS, W
    INFORMATION AND COMPUTATION, 1995, 119 (01) : 14 - 17
  • [22] Intersection types for lambda-terms and combinators and their logics
    Bunder, M
    LOGIC JOURNAL OF THE IGPL, 2002, 10 (04) : 357 - 378
  • [23] Intersection Types and Runtime Errors in the Pi-Calculus
    Dal Lago, Ugo
    de Visme, Marc
    Mazza, Damiano
    Yoshimizu, Akira
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [24] Linearization of the lambda-calculus and its relation with intersection type systems
    Florido, M
    Damas, L
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2004, 14 : 519 - 546
  • [25] Characterizing Strongly Normalizing λGtz-terms via Non-Idem potent Intersection Types
    Shen, Xinxin
    Zheng, Kougen
    PROCEEDINGS OF THE THIRD INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND APPLICATION ENGINEERING (CSAE2019), 2019,
  • [26] NORMAL FORMS IN THE TYPED LAMBDA-CALCULUS WITH TUPLE TYPES
    ZLATUSKA, J
    KYBERNETIKA, 1985, 21 (05) : 366 - 381
  • [27] Some algebraic structures in Lambda-calculus with inductive types
    Soloviev, S
    Chemouil, D
    TYPES FOR PROOFS AND PROGRAMS, 2004, 3085 : 338 - 354
  • [28] Light types for polynomial time computation in Lambda-calculus
    Baillot, P
    Terui, K
    19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 266 - 275
  • [29] Polymorphic lambda calculus with context-free session types
    Almeida, Bernardo
    Mordido, Andreia
    Thiemann, Peter
    Vasconcelos, Vasco T.
    INFORMATION AND COMPUTATION, 2022, 289
  • [30] A Calculus of Lambda Calculus Contexts
    Mirna Bognar
    Roel de Vrijer
    Journal of Automated Reasoning, 2001, 27 : 29 - 59
12345