The intensional lambda calculus

被引：12

作者：

Artemov, Sergei ^{[1
]}

Bonelli, Eduardo ^{[2
,3
]}

机构：

[1] CUNY, Grad Ctr, PhD Program Comp Sci, 365 5th Ave, New York, NY 10016 USA

[2] UNLP, Fac Informat, LIFIA, CONICET, Ensenada, Buenos Aires, Argentina

[3] Consejo Nacl Invest Cient & Tecn, RA-1033 Buenos Aires, DF, Argentina

来源：

LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS | 2007年 / 4514卷

关键词：

D O I：

10.1007/978-3-540-72734-7_2

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion square A is replaced by [s]A whose intended reading is "s is a proof of A". A term calculus for this formulation yields a typed lambda calculus lambda(I) that internalises intensional information on how a term is computed. In the same way that the Logic of Proofs internalises its own derivations, lambda(I) internalises its own computations. Confluence and strong normalisation of lambda(I) is proved. This system serves as the basis for the study of type theories that internalise intensional aspects of computation.

引用

页码：12 / +

页数：4

共 20 条

[1]

ALT J, 2001, P DAGST SEM PROOF TH, V2183

[2]

ARTEMOV S, 1996, 9606 MSI

[3]

ARTEMOV S, 2001, ALGEBRAS DIAGRAMS DE, P89

[4]

ARTEMOV S, 2006, INTENSIONAL LAMBDA C

[5]

Artemov Sergei N., 1995, 9529 MSI

[6]

BRZHNEV V, 2001, P 6 ESSLLI STUD SESS, P35

[7] Some properties of conversion [J].

Church, Alonzo ;

Rosser, J. B. .

TRANSACTIONS OF THE AMERICAN MATHEMATICAL SOCIETY, 1936, 39 (1-3) :472-482

[8] A modal analysis of staged computation [J].

Davies, R ;

Pfenning, F .

JOURNAL OF THE ACM, 2001, 48 (03) :555-604

[9]

DAVIES R, 1996, P 23 ANN S PRINC PRO, P258

[10]

DAVIES R, 2001, COMPUTER SCI, V11, P511

← 1 2 →