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] On the lambda Y calculus
Statman, R
17TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2002, : 159 - 166
[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] MODELS OF THE LAMBDA CALCULUS
KOYMANS, CPJ
INFORMATION AND CONTROL, 1982, 52 (03): : 306 - 332
[45] A Simpler Lambda Calculus
Jay, Barry
PROCEEDINGS OF THE 2019 ACM SIGPLAN WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM '19), 2019, : 1 - 9
[46] Graphic Lambda Calculus
Buliga, Marius
COMPLEX SYSTEMS, 2013, 22 (04): : 311 - 360
[47] The intensional lambda calculus
Artemov, Sergei
Bonelli, Eduardo
LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 2007, 4514 : 12 - +
[48] The safe lambda calculus
Blum, William
Ong, C. -H. Luke
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2007, 4583 : 39 - +
[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

← 1 2 3 4 5 →