A unified-algebra-based specification language for symbolic computing

  • J. Calmet
  • I. A. Tjandra
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)


A precise and perspicuous specification of mathematical domains of computation and their inherently related type inference mechanisms is a prerequisite for the design and systematic development of a system for symbolic computing. This paper describes Formal, a language for giving modular and well-structured specifications of such domains and particularly of “mathematical objects”. A novel framework for algebraic specification involving so-called “unified algebras” has been adopted, where sorts are treated as values. The adoption of this framework aims also at being capable of specifying polymorphism, unifying the notions of “parametric” and “inclusion” polymorphisms. Furthermore, the operational nature of the specification formalisms allows a straightforward transformation into an executable form.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BHK89]
    J.A. Bergstra, J. Heering, and P. Klint. Algebraic Specification. Addison-Wesley Publising Company, 1989.Google Scholar
  2. [BHPS86]
    R.J. Bradford, A.C. Hearn, J.A. Padget, and E. Schrufer. Enlarging the Reduce domain of computation. In SYMSAC 1986, pages 100–106. ACM, New York, 1986.Google Scholar
  3. [CT93]
    J. Calmet and I.A. Tjandra. Specifying type polymorphisms in symbolic computing with formal. In preparation, 1993.Google Scholar
  4. [CTB91]
    J. Calmet, I.A. Tjandra, and G. Bittencourt. Mantra: A shell for hybrid knowledge representation. In IEEE-Conference on Tools for AI, pages 164–171. IEEE, IEEE Computer Society Press, 1991.Google Scholar
  5. [CTH93]
    J Calmet, I.A. Tjandra, and K. Homann. Unified domains and abstract computational structures (to be published). In J. Calmet and J. Campbell, editors, Int. Conference on Ai and Symbolic Computations. Springer-Verlag, LNCS, 1993.Google Scholar
  6. [CW85]
    L. Cardelli and P. Wagner. On understanding types, data abstraction and polymorphism. Computing Survey, 17(4):471–522, 1985.CrossRefGoogle Scholar
  7. [EM85]
    H. Ehrig and B. Mahr. Fundamental of Algebraic Specification 1 — Equations and Initial Semantics. EATCS Monograph on Theoretical Computer Science, vol 6. Springer-Verlag, 1985.Google Scholar
  8. [EM90]
    H. Ehrig and B. Mahr. Fundamental of Algebraic Specification 2. Monograph on Theoretical Computer Science, vol 21. Springer-Verlag, 1990.Google Scholar
  9. [GB84]
    J.A. Goguen and R.M. Burstall. Introducing institution. In Logics of Programming Workshop, pages 221–256. Springer-Verlag, 1984.Google Scholar
  10. [GB85]
    J.A. Goguen and R.M. Burstall. Institutions: Abstract model theory for computer science. Technical report, Stanford University, CSLI-85-30, 1985.Google Scholar
  11. [JKKM88]
    J.P. Jounnaud, C. Kirchner, H. Kirchner, and A. Megrelis. Obj: Programming with equalities, subsorts, overloading and parameterization. In J. Grabowski, P. Lescanne, and P. Wechler, editors, Algebraic and Logic Programming, pages 41–52. Spriner-Verlag, LNCS 343, 1988.Google Scholar
  12. [LL87]
    T. Lehman and J. Loeckx. The specification language obscure. In D. Sanella and A. Tarlecki, editors, Recent Trends in Data Types Specification, pages 131–153. Springer-Verlag, LNCS 332, 1987.Google Scholar
  13. [Mac71]
    S MacLane. Categories for the Working Mathematician. Graduate Text in Mathematics. Springer-Verlag, 1971.Google Scholar
  14. [Mos89]
    P.D. Mosses. Unified algebras and institutions. In Logics in Computer Science, pages 304–312. IEEE Press, 1989.Google Scholar
  15. [Mos92]
    P.D. Mosses. Action Semantics. Cambridge Tracks in Theoretical Computer Science. Cambridge University Press, 1992.Google Scholar
  16. [San84]
    D Sanella. A set-theoretic semantics of Clear. Acta Informatica, 21(5): 443–472, 1984.CrossRefGoogle Scholar
  17. [SLC91]
    P Schnoebelen, D Lugiez, and H Comon. A rewrite-based type discipline for a subset of computer algebra. Journal of Symbolic Computation, 11: 349–368, 1991.Google Scholar
  18. [ST85]
    D. Sanella and A. Tarlecki. Program specification and development in Standard-ml. In 12th ACM Symposium on Principle of Programming Languages, New Orleans, USA, pages 67–77. ACM Press, 1985.Google Scholar
  19. [Sut91]
    R.S. (Ed.) Sutor. Axiom User's Guide. The Numerical Algorithm Group Limited, 1991.Google Scholar
  20. [Wir86]
    M. Wirsing. Structured algebraic specification: A kernel language. Theoretical Computer Science, 42:124–249, 1986.CrossRefGoogle Scholar
  21. [Wir90]
    M. Wirsing. Algebraic specification. In J. VanLeeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 677–788. Elsevier Science Publishers B.V., 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • J. Calmet
    • 1
  • I. A. Tjandra
    • 1
  1. 1.Institut für Algorithmen und Kognitive SystemeUniversität KarlsruheKarlsruheGermany

Personalised recommendations