Spinal Atomic Lambda-Calculus

被引：2

作者：

Sherratt, David ^{[1
]}

Heijltjes, Willem ^{[2
]}

Gundersen, Tom ^{[3
]}

Parigot, Michel ^{[4
]}

机构：

[1] Friedrich Schiller Univ Jena, Jena, Germany

[2] Univ Bath, Bath, Avon, England

[3] Red Hat Inc, Oslo, Norway

[4] Univ Paris, Inst Rech Informat Fondamentale, CNRS, Paris, France

来源：

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2020 | 2020年 / 12077卷

基金：

英国工程与自然科学研究理事会;

关键词：

Lambda-Calculus; Full laziness; Deep inference; Curry-Howard;

D O I：

10.1007/978-3-030-45231-5_30

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present the spinal atomic.-calculus, a typed.-calculus with explicit sharing and atomic duplication that achieves spinal full laziness: duplicating only the direct paths between a binder and bound variables is enough for beta reduction to proceed. We show this calculus is the result of a Curry-Howard style interpretation of a deep-inference proof system, and prove that it has natural properties with respect to the.-calculus: confluence and preservation of strong normalisation.

引用

页码：582 / 601

页数：20

共 50 条

[1] Atomic lambda-calculus: a typed lambda-calculus with explicit sharing
Gundersen, Tom
Heijltjes, Willem
Parigot, Michel
[J]. 2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2013, : 311 - 320
[2] An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus
Mazza, Damiano
[J]. 2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 471 - 480
[3] ALGEBRA AND THE LAMBDA-CALCULUS
JAFFER, A
[J]. DR DOBBS JOURNAL, 1993, 18 (09): : 36 - &
[4] The differential lambda-calculus
Ehrhard, T
Regnier, L
[J]. THEORETICAL COMPUTER SCIENCE, 2003, 309 (1-3) : 1 - 41
[5] Lambda-calculus with constructors
Arbiser, Ariel
Miquel, Alexandre
Rios, Alejandro
[J]. TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 181 - 196
[6] Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
Santo, Jose Espirito
Matthes, Ralph
Pinto, Luis
[J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2019, 29 (08) : 1092 - 1124
[7] LAMBDA-CALCULUS MODELS AND EXTENSIONALITY
HINDLEY, R
LONGO, G
[J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1980, 26 (04): : 289 - 310
[8] ON THE DEFINITION OF LAMBDA-CALCULUS MODELS
BERRY, G
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1981, 107 : 218 - 230
[9] COMPILING THE POLYMORPHIC LAMBDA-CALCULUS
MICHAYLOV, S
PFENNING, F
[J]. SIGPLAN NOTICES, 1991, 26 (09): : 285 - 296
[10] Lambda-calculus with director strings
Fernández, M
Mackie, I
Sinot, FR
[J]. APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING, 2005, 15 (06) : 393 - 437

← 1 2 3 4 5 →