Reduction semantics for a Calculus of Closures

_Reduction semantics for a Calculus of Closures_

David Van Horn

This is a PLT Redex formulation of the applicative order reduction 
strategy for the _lambda-rho-hat_ calculus, an extension of Curien's 
calculus of _closures_, lambda rho, that allows for one-step reduction
to be expressed.

The reference for this work is Section 2.2 and 2.4 of A Concrete 
Framework for Environment Machines, Magorzata Biernacka and Olivier 

(Note that this uses de Bruijn indices-- variables are represented by 
natural numbers and a substitution (an environment) is a list of values.
A variable's number gives the index into the list for value to which it 
is bound.  Environment extension is just cons.)

See to trace a few example expressions in the language.