Monads, indexes and transformations

Abstract

The specification and derivation of substitution for the de Bruijn representation of λ-terms is used to iUustrate programming with a function-sequence monad. The resulting program is improved by interactive program transformation methods into an efficient implementation that uses primitive machine arithmetic. These transformations illustrate new techniques that assist the discovery of the arithmetic structure of the solution.