Meta Languages in Algebraic Compilers?

Abstract. Algebraic compilers provide a powerful and convenient mech-anism for specifying language translators. With each source language operation one associates a computation for constructing its target lan-guage image; these associated computations, called derived operations, are expressed in terms of operations from the target language. Some-times the target language operations are not powerful enough to specify the required computations and one may then need to extend the tar-get language algebras with more computationally expressive operations. A better solution is to package them in a meta language which can be automatically composed with the target language operations to ensure that all operations needed or desired for performing a translation are provided. In this paper, we show how imperative and functional meta languages can be composed with a target language in an example which implements a temporal logic model checker as an algebraic compiler and show how meta languages can be seen as components to be combined with a source and target language to generate an algebraic compiler.