Skip to main content
SpringerLink
Log in

Inserting injection operations to denotational specifications

  • Regular Papers
  • Published:
New Generation Computing Aims and scope Submit manuscript

Abstract

In describing denotational semantics of programming languages, injection operations into sum domains are conventionally omitted for the sake of brevity. This in turn leads to difficulties for semantic processing systems which accept denotational specifications as input and mechanically calculate them for debugging the semantics. This paper describes an algorithm for inserting injection operations to denotational specifications as part of the typechecking process.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Bodwin, J., Bradley, L., Kanda, K., Litle, D. and Pleban, U., “Experience with an Experimental Compiler Generator Based on Denotational Semantics,”Proc. 1982 ACM Symp. on Compiler Construction, SIGPLAN Notices, Vol. 17, No. 6, pp. 216–229, 1982.

    Article  Google Scholar 

  2. Cardelli, L., “Basic Polymorphic Typechecking,”Polymorphism,Vol. 2,No. 1, 1984.

  3. Chujo, H. and Takeichi, M., “Porting ML on a New Machine,”Proc. 28th Symp. of Inf. Proc. Japan, pp. 427–428, 1984, [in Japanese]. Also Cardelli, L.,Pascal VAX-Unix Version of Edinburgh ML, converted from VMS by Nobuo Saito.

  4. Futatsugi, K., Goguen, J. A., Jouannaud, J.-P. and Meseguer, J., “Principles of OBJ2,”Proc. 12th ACM Symp. on Principles of Prog. Lang., pp. 52–66, 1984.

  5. Gordon, M. J. C.,The Denotational Description of Programming Languages, Springer-Verlag, 1979.

  6. Gordon, M. J., Milner, R. and Wadsworth, C. P.,Edinburgh LCF, LNCS 78, Springer-Verlag, 1979.

  7. Milner R., “A Theory of Type Polymorphism,”J. Comput. Syst. Sci., Vol. 17, pp. 348–375, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  8. Mitchell, J. C., “Coercion and Type Inference (Summary),”Proc. 11th ACM Symp. on Principles of Prog. Lang., pp. 175–185, 1983.

  9. Mosses, P.,SIS—Semantic Implementation System: Reference Manual and User Guide, DIAMI MD-30, Dept. of Computer Science, University of Aarhus, Denmark, 1979.

    Google Scholar 

  10. Ohira, T. and Takeichi, M., “A Language Development System,”Proc. 28th Symp. of Inf. Proc. Japan, pp. 329–330, 1984, [in Japanese].

  11. Robinson, J. A., “A Machine-Oriented Logic Based on the Resolution Principle,”J. ACM, Vol. 12, pp. 23–49, 1965.

    Article  MATH  Google Scholar 

  12. Stoy, J. E.,Denotational Semantics, MIT Press, 1977.

  13. Wand, M., “A Semantic Prototyping System,”Proc. 1984 ACM Symp. on Compiler Construction, SIGPLAN Notices, Vol. 19, No. 6, pp. 213–221, 1984.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Electro-Communications, 1-5-1 Chofugaoka, Chofu-shi, 182, Tokyo, Japan

    Masato Takeichi

Authors
  1. Masato Takeichi
    View author publications

    You can also search for this author in PubMed Google Scholar

About this article

Cite this article

Takeichi, M. Inserting injection operations to denotational specifications. New Gener Comput 4, 365–381 (1986). https://doi.org/10.1007/BF03037390

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF03037390

Keywords

Search

Navigation