λ-V-CS: an extended λ-calculus for scheme
Matthias Felleisen · 1988
The λ-v-CS-calculus is a conservative extension of the λ-value-calculus for reasoning about programs in Scheme-like languages. The basis of the extended calculus is a symbolic rewriting semantics for imperative programs. We show with numerous examples how to state and prove equational properties of Scheme-programs in the calculus. The examples suggest that the algebraic manipulation of imperative-functional programs is as feasible and as fruitful as that of functional ones.