Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Semantics of Data Types

SDT 1984: Semantics of Data Types pp 215–233Cite as

Executable specification of static semantics

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 173))

Abstract

In this paper we have presented three main ideas:

  • Semantic specifications written using inference rules may be executed. The method may be compared with the approach taken in the SIS system of Peter Mosses [Mos78].

  • A Prolog system is adequate for executing such a specification.

  • Intensive use of overloading make semantic specifications easier and more elegant.

Typol seems to be a very intuitive way to introduce semantic specifications into a system like Mentor. We would like to use more of Prolog's power (back-tracking for example) to specify the static semantics of programming languages with overloading, such as Ada. Other examples will be needed to improve the Typol formalism and to see exactly what its limits are, both from a theoretical and a practical standpoint.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Barberye, T. Joubert, M. Martin, Manuel d'utilisation de Prolog/Cnet — version Pascal/Multics 2.00 C.N.E.T. NT/PAA/CLC/ICS/1058, Paris, October 1983

    Google Scholar 

  2. Th. Despeyroux, Spécifications sémantiques dans le système Mentor, Thèse de 3ème cycle, Université Paris-XI, Orsay, October 1983

    Google Scholar 

  3. V. Donzeau-Gouge, G. Huet, G. Kahn, B. Lang, Programming environments based on structured editors: the MENTOR experience, Rapport de recherche no 26, Inria, July 1980

    Google Scholar 

  4. V. Donzeau-Gouge, G. Huet, G. Kahn, B. Lang, J.-J. Lévy, A structure oriented program editor: a first step toward computer assisted programming, International Computing Symposium, North-Holland Publishing Company, 1975

    Google Scholar 

  5. V. Donzeau-Gouge, G. Kahn, B. Lang, A complete machine-checked definition of a simple programming language using denotational semantics, Rapport de recherche no 330, Inria, October 1978

    Google Scholar 

  6. L. Damas, R. Milner, Principal type-schemes for functional program, ACM, 1982

    Google Scholar 

  7. V. Donzeau-Gouge, Les raisons des choix dans la définition formelle du langage Ada, Thèse d'état, Université Paris-7 July 1982

    Google Scholar 

  8. M. Gordon, R. Milner, C. Wadsworth, Edinburg LCF, Lecture Notes in Computer Science, Springer-Verlag, 1979

    Google Scholar 

  9. M.S.C. Gordon, Descriptive technique for denotational semantics, Springer Verlag, 1979

    Google Scholar 

  10. Formal definition of the Ada programming language, Honewell Inc., CII-Honewell Bull, Inria, November 1980

    Google Scholar 

  11. S. C. Johnson, Yacc: Yet Another Compiler-Compiler Bell Laboratories, July 1978

    Google Scholar 

  12. G. Kahn, B. Lang, B. Melese, E. Morcos, Metal: a formalism to specify formalisms, Science of Computer Programming, vol. 3, no 2, p. 151–188, August 83

    Google Scholar 

  13. D. E. Knuth, Semantics of context-free languages, Mathematical Systems Theory, 2, 2, p. 127–145, 1968, correction in vol. 5, 1, p. 95–96, 1971

    Google Scholar 

  14. P. Mosses, SIS: a compiler generator system using denotational semantics, DAIMI, University of Aarhus, 1978

    Google Scholar 

  15. D. B. MacQueen, R. Sethi, A semantic model of types for applicative languages, ACM symposium on LISP and functional programming, p. 243–252, 1982.

    Google Scholar 

  16. R. Milner, A theory of type polymorphism in programming, JCSS 17,3, p. 348–375, 1978

    Google Scholar 

  17. L. Paulson, A compiler generator for semantic grammars, PhD Thesis, Stanford University, December 1981

    Google Scholar 

  18. G.D. Plotkin, A structural approach to operational semantics, DAIMI FN-19, Aarhus university, September 1981

    Google Scholar 

  19. V. Pratt, Semantical considerations on Floyd-Hoare logic, 17th Focs, 109–121, Huston, 1976

    Google Scholar 

  20. T. W. Reps, Generating language-based environments, PhD Thesis, Cornell University, August 1982

    Google Scholar 

  21. J. A. Robinson, A machine-oriented logic based on the resolution principle JACM 12,1, p. 23–41, 1965

    Google Scholar 

  22. R. Sethi, Semantics of computer programs: overview of language definition methods, Bell Laboratories, September 1977

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. I.N.R.I.A. Route des Lucioles Sophia-Antipolis, F-06565, Valbonne

    Thierry Despeyroux

Authors
  1. Thierry Despeyroux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gilles Kahn David B. MacQueen Gordon Plotkin

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Despeyroux, T. (1984). Executable specification of static semantics. In: Kahn, G., MacQueen, D.B., Plotkin, G. (eds) Semantics of Data Types. SDT 1984. Lecture Notes in Computer Science, vol 173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-13346-1_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-13346-1_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-13346-9

  • Online ISBN: 978-3-540-38891-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation