Monads, Indexes and Transformations

. The specification and derivation of substitution for the de Bruijn representation of -terms is used to illustrate programming with a functionsequence 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. Introduction Substitution is one of many problems in computer science that, once understood in one context, is understood in all contexts. Why, then, must a different substitution function be written for every abstract syntax implemented? This paper shows how to specify substitution once and use the monadic structure of the specification to instantiate it on different abstract syntax structures. It also shows how to interactively derive an efficient implementation of substitution from this very abstract specification. Formal methods that support reasoning about ..