Specification languages in algebraic compilers

Research output: Contribution to journalConference articlepeer-review

3 Scopus citations


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

Original languageEnglish (US)
Pages (from-to)351-385
Number of pages35
JournalTheoretical Computer Science
Issue number3
StatePublished - Jan 6 2003
Externally publishedYes
EventAlgebraic Methodology and Software Technology (AMAST 2000) - Iowa City, IO, United States
Duration: May 20 2000May 27 2000

Bibliographical note

Funding Information:
We would like to thank the anonymous reviewers for their helpful suggestions in improving this paper and Microsoft Research for funding this research.


  • Algebraic compiler
  • Specification languages


Dive into the research topics of 'Specification languages in algebraic compilers'. Together they form a unique fingerprint.

Cite this