Modular first-order specifications of operational semantics

  • Harald Ganzinger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 217)


This paper is about modular specification of operational semantics and the execution of such specifications. It gives a first-order specification of the semantics of a simple applicative programming language. This specification is modular in the sense that binding rules are specified independently of the concrete syntax of the language and that expression evaluation needs not consider any concept of names. We then propose a simple lemma generation technique that achieves the effect of partial evaluation to implement such specifications in Prolog.


Expression Evaluation Free Variable Operational Semantic Partial Evaluation Horn Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BHK85]
    Bergstra, J.A., Heering, J., Klint, P.: Algebraic definition of a simple programming language. CWI, Dept. of Comp. Sci., Report CS-R8504, Amsterdam, 1985.Google Scholar
  2. [Bru72]
    De Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Math. 34, (1972), pp. 381–392.Google Scholar
  3. [Clé85]
    Clément, D., Despeyroux, J., Despeyroux, Th., Hascoet, L., Kahn, G.: Natural semantics on the computer. RR 416, INRIA, Sophia Antipolis, June 1985.Google Scholar
  4. [Ers77]
    Ershov, A,: On the partial evaluation principle. Inf. Proc. Letters 6,2 (1977), 38–41.Google Scholar
  5. [Fut85]
    Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, P.: Principles of OBJ2. Proc. POPL 1985.Google Scholar
  6. [Gan83]
    Ganzinger, H.: Increasing modularity and language-independency in automatically generated compilers. SCP 3 (1983), 223–287.Google Scholar
  7. [GH85]
    Ganzinger, H., Hanus, M.: Modular logic programming of compilers. Proc. IEEE Symp. on Logic Programming, Boston, 1985.Google Scholar
  8. [GP81]
    Goguen, J.A., Parsaye-Ghomi, K.: Algebraic denotational semantics using parameterized abstract modules. LNCS 107, 1981.Google Scholar
  9. [GT79]
    Goguen, J.A., Tardo, J.J.: An introduction to OBJ: A language for writing and testing formal algebraic specifications. Proc. IEEE Conf on Spec. of Reliable Software, Cambridge, Mass. 1979.Google Scholar
  10. [Hen80]
    Henderson, P.: Functional Programming: Application and Implementation. Prentice Hall, 1980.Google Scholar
  11. [JSS85]
    Jones, N.D., Sestoft, P., Søndergaard, H.: An experiment in partial evaluation: the generation of a compiler generator. Copenhagen, 1985, to be published.Google Scholar
  12. [Lip82]
    Lipeck, U.: An algebraic calculus for structured design of data abstractions (in German). PhD-Thesis, U. Dortmund, 1982.Google Scholar
  13. [Mos83]
    Mosses, P.: Abstract semantic algebras. In Bjørner, D. (ed.): Formal Description of Programming Concepts II, North-Holland, 1983, 45–70.Google Scholar
  14. [Plo83]
    Plotkin, G.D.: An operational semantics for CSP. In Bjørner, D. (ed.): Formal Description of Programming Concepts II, North-Holland, 1983, 199–126.Google Scholar
  15. [Rey72]
    Reynolds, J.C.: Definitional interpreters for higher-order programming languages. 25th ACM Annual Conf., Boston 1972, pp. 717–740.Google Scholar
  16. [Wan79]
    Wand, M.: First-order identities as a defining language. TR No. 29, Comp. Sci. Dep't, Indiana U., Bloomington, Indiana, May 1979.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1986

Authors and Affiliations

  • Harald Ganzinger
    • 1
  1. 1.FB Informatik Universität DortmundDortmund 50W. Germany

Personalised recommendations