The differential lambda-calculus

被引：160
|
作者：
Ehrhard, T [1 ]
Regnier, L [1 ]
机构：
[1] CNRS, Inst Math Luminy, UPR 9016, F-13288 Marseille, France
来源：
THEORETICAL COMPUTER SCIENCE | 2003年 / 309卷 / 1-3期
关键词：
lambda-calculus; linear logic; denotational semantics; linear head reduction;
D O I：
10.1016/S0304-3975(03)00392-X
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus. (C) 2003 Elsevier B.V. All rights reserved.
引用
收藏
页码：1 / 41
页数：41
相关论文
共 50 条
  • [1] Intuitionistic differential nets and lambda-calculus
    Tranquilli, Paolo
    [J]. THEORETICAL COMPUTER SCIENCE, 2011, 412 (20) : 1979 - 1997
  • [2] 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
  • [3] 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
  • [4] Categorical Models of the Differential lambda-Calculus Revisited
    Cockett, J. R. B.
    Gallagher, J. D.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 325 : 63 - 83
  • [5] ALGEBRA AND THE LAMBDA-CALCULUS
    JAFFER, A
    [J]. DR DOBBS JOURNAL, 1993, 18 (09): : 36 - &
  • [6] Lambda-calculus with constructors
    Arbiser, Ariel
    Miquel, Alexandre
    Rios, Alejandro
    [J]. TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 181 - 196
  • [7] 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
  • [8] LAMBDA-CALCULUS MODELS AND EXTENSIONALITY
    HINDLEY, R
    LONGO, G
    [J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1980, 26 (04): : 289 - 310
  • [9] ON THE DEFINITION OF LAMBDA-CALCULUS MODELS
    BERRY, G
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1981, 107 : 218 - 230
  • [10] COMPILING THE POLYMORPHIC LAMBDA-CALCULUS
    MICHAYLOV, S
    PFENNING, F
    [J]. SIGPLAN NOTICES, 1991, 26 (09): : 285 - 296
12345