View Related Documents

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 a set 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.

Fulltext Preview

Image of the first page of the fulltext document