Arrays in Imperative Lambda Calculus

In recent work, Swarup, Reddy, and Ireland defined a formal system called Imperative Lambda Calculus to provide clean integration of functional and imperative programming styles. In this paper, we study the issues of array manipulation in this framework. It is shown that the unique features of the calculus allow one to express array algorithms using high-level abstractions that are not available in purely functional languages. 1 Introduction One view of functional programming is that it is restricted to "value-oriented" computation. Values are, by definition, static (or eternal) and no dynamic quantities are permissible. This viewpoint makes it difficult to deal with large aggregates such as arrays. It also makes it difficult to model a variety of dynamic objects which are required in programming. We take a more "positive" view towards functional programming. First of all, we value functional programming for the abstractions it offers in terms of higher-order functions and lazy data s..