Explicit Environments

Issue title: Typed Lambda Calculi and Applications (TLCA'99)

Article type: Research Article

Authors: Sato, Masahiko | Sakurai, Takafumi | Burstall, Rod

Abstract: We introduce λε, a simply typed calculus with environments as first class values. As well as the usual constructs of λ and application, we have e[a] which evaluates term a in an environment e. Our environments are sets of variable-value pairs, but environments can also be computed by function application and evaluation in some other environments. The notion of environments here is a generalization of explicit substitutions and records. We show that the calculus has desirable properties such as subject reduction, confluence, conservativity over the simply typed λβ-calculus and strong normalizability.

Keywords: explicit environments, simply typed calculus, confluence, conservativity, strong normalizability

Journal: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 79-115, 2001