Non-idempotent intersection types for the Lambda-Calculus

被引：32

作者：

Bucciarelli, Antonio ^{[1
,2
]}

Kesner, Delia ^{[1
,2
]}

Ventura, Daniel ^{[3
]}

机构：

[1] CNRS, Inst Rech Informat Fondamentale, Paris, France

[2] Univ Paris Diderot, Paris, France

[3] Univ Fed Goias, Inst Informat, Goiania, Go, Brazil

来源：

LOGIC JOURNAL OF THE IGPL | 2017年 / 25卷 / 04期

关键词：

Type Systems; intersection types; quantitative semantics; normalization properties; inhabitation problems; principal typing; STRONG NORMALIZATION; ASSIGNMENT;

D O I：

10.1093/jigpal/jzx018

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

This article explores the use of non-idempotent intersection types in the framework of the lambda-calculus. Different topics are presented in a uniform framework: head normalization, weak normalization, weak head normalization, strong normalization, inhabitation, exact bounds and principal typings. The reducibility technique, traditionally used when working with idempotent types, is replaced in this framework by trivial combinatorial arguments.

引用

页码：431 / 464

页数：34

共 50 条

[1] INHABITATION FOR NON-IDEMPOTENT INTERSECTION TYPES
Bucciarelli, Antonio
Kesner, Delia
Della Rocca, Simona Ronchi
LOGICAL METHODS IN COMPUTER SCIENCE, 2018, 14 (03)
[2] NON-IDEMPOTENT INTERSECTION TYPES AND STRONG NORMALISATION
Bernadet, Alexis
Graham-Lengrand, Stephane
LOGICAL METHODS IN COMPUTER SCIENCE, 2013, 9 (04)
[3] Non-idempotent intersection types in logical form
Ehrhard, Thomas
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2020, 2020, 12077 : 198 - 216
[4] A binary modal logic for the intersection types of lambda-calculus
Valentini, S
Viale, M
INFORMATION AND COMPUTATION, 2003, 185 (02) : 211 - 232
[5] Plays as Resource Terms via Non-idempotent Intersection Types
Tsukada, Takeshi
Ong, C. -H. Luke
PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), 2016, : 237 - 246
[6] Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
Bernadet, Alexis
Lengrand, Stephane
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, 2011, 6604 : 88 - 107
[7] INHABITATION OF TYPES IN THE SIMPLY TYPED LAMBDA-CALCULUS
DEKKERS, W
INFORMATION AND COMPUTATION, 1995, 119 (01) : 14 - 17
[8] An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus
Mazza, Damiano
2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 471 - 480
[9] Atomic lambda-calculus: a typed lambda-calculus with explicit sharing
Gundersen, Tom
Heijltjes, Willem
Parigot, Michel
2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2013, : 311 - 320
[10] INTERSECTION TYPES FOR lambda(Gtz)-CALCULUS
Ghilezan, Silvia
Ivetic, Jelena
PUBLICATIONS DE L INSTITUT MATHEMATIQUE-BEOGRAD, 2007, 82 (96): : 85 - 91

← 1 2 3 4 5 →