A calculus of lambda calculus contexts

被引：6

作者：

Bognar, M ^{[1
]}

De Vrijer, R ^{[1
]}

机构：

[1] Vrije Univ Amsterdam, Amsterdam, Netherlands

来源：

JOURNAL OF AUTOMATED REASONING | 2001年 / 27卷 / 01期

关键词：

lambda calculus; context calculus; pretyping;

D O I：

10.1023/A:1010654904735

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

The calculus lambdac serves as a general framework for representing contexts. Essential features are control over variable capturing and the freedom to manipulate contexts before or after hole filling, by a mechanism of delayed substitution. The context calculus lambdac is given in the form of an extension of the lambda calculus. Many notions of context can be represented within the framework; a particular variation can be obtained by the choice of a pretyping, which we illustrate by three examples.

引用

页码：29 / 59

页数：31

共 23 条

[1]

Abadi M., 1991, Journal of Functional Programming, V1, P375, DOI 10.1017/S0956796800000186

[2]

[Anonymous], 1988, PLDI 88 P ACM SIGPLA

[3]

BALSTERS H, 1987, MATH LOGIC THEORETIC, P15

[4]

BALSTERS H, 1994, SELECTED PAPERS AUTH, P339

[5]

BARENDREGT HP, 1985, STUD LOGIC FDN MATH, V103

[6]

BOGNAR M, 1999, SEGMENTS CONTEXT

[7]

DEBRUIJN N, 1978, 78WSK03 TU EINDH

[8]

Despeyroux J, 1997, LECT NOTES COMPUT SC, V1210, P147

[9]

HASHIMOTO M, 1998, SURIKAISEKIKENKYUSHO, V1023, P76

[10]

Kahrs S., 1993, Conditional Term Rewriting Systems. Third International Workshop, CTRS-92 Proceedings, P21

← 1 2 3 →