It appears that the transformational set-up is closely related to the structure of mechanical reasoning performed in meta-logical systems like LCF, HOL or LAMBDA. We shall explore this relationship and work on the mechanisation of the transformational approach to the design of programs.
We are using the LAMBDA system of Abstract Hardware Ltd. to implement a transformational approach. Initially these activities will be performed within a national ``BMFT'' research project, called ``KORSO'' (for ``Correct Software''). In KORSO we are implementing a semantics model in LAMBDA which allows the verification of transformation rules and their mechanical application for the design of -like programs from specifications [6]. Later we plan to take over this work to ProCoS II for (subsets of) the specification language and transformation rules used there.