Abstract

We give a typed calculus which has environments as first class objects. This calculus extends simply typed lambda calculus, and can be seen as a generalisation of both explicit substitutions and records. Basic properties such as subject reduction, church rosser theorem, conservativity over simply typed lambda calculus hold.

This is joint work with Rod Burstall and T. Sakurai.