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 条

[31] COMPILING THE POLYMORPHIC LAMBDA-CALCULUS
MICHAYLOV, S
PFENNING, F
SIGPLAN NOTICES, 1991, 26 (09): : 285 - 296
[32] LAMBDA-CALCULUS MODELS AND EXTENSIONALITY
HINDLEY, R
LONGO, G
ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1980, 26 (04): : 289 - 310
[33] Spinal Atomic Lambda-Calculus
Sherratt, David
Heijltjes, Willem
Gundersen, Tom
Parigot, Michel
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2020, 2020, 12077 : 582 - 601
[34] ON THE REPRESENTATION OF DATA IN LAMBDA-CALCULUS
PARIGOT, M
LECTURE NOTES IN COMPUTER SCIENCE, 1990, 440 : 309 - 321
[35] LAMBDA-CALCULUS MODELS AND EXTENSIONALITY
HINDLEY, R
LONGO, G
JOURNAL OF SYMBOLIC LOGIC, 1980, 45 (02) : 392 - 392
[36] COMPUTATIONAL LAMBDA-CALCULUS AND MONADS
MOGGI, E
FOURTH ANNUAL SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, 1989, : 14 - 23
[37] Solvability in Resource Lambda-Calculus
Pagani, Michele
della Rocca, Simona Ronchi
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2010, 6014 : 358 - 373
[38] HIGHLIGHTS OF THE HISTORY OF THE LAMBDA-CALCULUS
ROSSER, JB
ANNALS OF THE HISTORY OF COMPUTING, 1984, 6 (04): : 337 - 349
[39] Standardization in resource lambda-calculus
Dominici, Maurizio
Della Rocca, Simona Ronchi
Tranquilli, Paolo
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (101): : 1 - 11
[40] INVERTIBLE TERMS IN THE LAMBDA-CALCULUS
BERGSTRA, J
KLOP, JW
THEORETICAL COMPUTER SCIENCE, 1980, 11 (01) : 19 - 37

← 1 2 3 4 5 →