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 条
  • [41] The lambda calculus is algebraic
    Selinger, P
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2002, 12 : 549 - 566
  • [42] An Introduction to the Lambda Calculus
    Csoernyei, Zoltan
    Devai, Gergely
    CENTRAL EUROPEAN FUNCTIONAL PROGRAMMING SCHOOL, 2008, 5161 : 87 - 111
  • [43] A lambda calculus with forms
    Lumpe, M
    SOFTWARE COMPOSITION, 2005, 3628 : 83 - 98
  • [44] A Simpler Lambda Calculus
    Jay, Barry
    PROCEEDINGS OF THE 2019 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM '19), 2019, : 1 - 9
  • [45] MODELS OF THE LAMBDA CALCULUS
    KOYMANS, CPJ
    INFORMATION AND CONTROL, 1982, 52 (03): : 306 - 332
  • [46] Graphic Lambda Calculus
    Buliga, Marius
    COMPLEX SYSTEMS, 2013, 22 (04): : 311 - 360
  • [47] The safe lambda calculus
    Blum, William
    Ong, C. -H. Luke
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2007, 4583 : 39 - +
  • [48] The intensional lambda calculus
    Artemov, Sergei
    Bonelli, Eduardo
    LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 2007, 4514 : 12 - +
  • [49] Godelization in the lambda calculus
    Goldberg, M
    INFORMATION PROCESSING LETTERS, 2000, 75 (1-2) : 13 - 16
  • [50] Infinitary lambda calculus
    Kennaway, JR
    Klop, JW
    Sleep, MR
    deVries, FJ
    THEORETICAL COMPUTER SCIENCE, 1997, 175 (01) : 93 - 125
12345