A reduction semantics for imperative higher-order languages

Abstract

Imperative higher-order languages are a highly expressive programming medium. Compared to functional programming languages, they permit the construction of safe and modular programs. However, functional languages have a simple reduction semantics, which makes it easy to evaluate program pieces in parallel. In order to overcome this dilemma, we construct a conservative extension of the λ-calculus that can deal with control and assignment facilities. This calculus simultaneously provides an algebraic reasoning system and an elegant reduction semantics of higher-order imperative languages. We show that the evaluation of applications can still take advantage of parallelism and that the major cost of these evaluations stems from the necessary communication for substitutions. Since this is also true for functional languages, we conjecture that if a successful parallel evaluation scheme for functional languages is possible, then the same strategy will also solve the problem of parallel evaluations for imperative programming languages.