SML [Miln 90] is used as functional programming language. SML supports modular and high-level functional programming and integrates non-functional programming styles (such as references, assignments and concurrency) in a clean and transparent way. SML structures correspond to algebras and can therefore be understood as models of equational specifications. Moreover its module concepts can be easily expressed in the type theoretic framework. SML is used for constructing prototype implementations of specifications.