Abstract:
Many software maintenance problems are caused by using text
editors to change programs. A more systematic and reliable way of performing
program updates is to express changes with an update language.
In particular, updates should preserve the syntax- and type-correctness of
the transformed object programs.
We describe an update calculus that can be used to update lambda-calculus
programs. We develop a type system for the update language that infers
the possible type changes that can be caused by an update program. We
demonstrate that type-safe update programs that fulfill certain structural
constraints preserve the type-correctness of lambda terms. The update calculus
can serve as a basis for higher-level update languages, such as for
Haskell or Java. We briefly indicate a possible design of these update languages.
