The differential λμ-calculus

被引：8
|
作者：
Vaux, Lionel [1 ]
机构：
[1] Univ Aix Marseille 2, Inst Math Luminy, F-13288 Marseille 9, France
来源：
THEORETICAL COMPUTER SCIENCE | 2007年 / 379卷 / 1-2期
关键词：
differential lambda-calculus; lambda-mu calculus; linear logic; classical logic;
D O I：
10.1016/j.tcs.2007.02.028
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We define a differential; lambda mu-calculus which is an extension of both Parigot's lambda mu-calculus and Ehrhard-Regnier's differential X-calculus. We prove some basic properties of the system: reduction enjoys Church-Rosser and simply typed terms are strongly normalizing. (c) 2007 Elsevier B.V. All rights reserved.
引用
收藏
页码：166 / 209
页数：44
相关论文
共 50 条
12345