[Prev][Next][Index][Thread]

formal semantics of real-world programming languages lists



Please forward, distribute, post, circulate:


                       SOLICITING CONTRIBUTIONS TO 
         FORMAL SEMANTICS OF REAL-WORLD PROGRAMMING LANGUAGES LISTS


Work on formal semantics of programming languages is an area of intensive
research. Several successful approaches exist, and numerous books on the
subject have been published. See, e.g.,
- C. Gunter, Semantics of programming languages: structures and techniques, 
  MIT Press 1992
- H.R. Nielson and F. Nielson, Semantics with applications: A formal
  introduction, Wiley, 1992 
- D. Schmidt, The structure of typed programming languages, MIT Press 1994
- R. Tennent, Semantics of programming languages, Prentice Hall, 1991
- G. Winskel, The formal semantics of programming languages: an introduction,
  MIT Press 1993
and the references therein.

There are a number of formal semantics of real-world programming languages. 
In order to establish which approach has been used to describe the semantics 
of which language, we would like to maintain corresponding lists.

We are seeking formal semantics of languages such as SML, Erlang, Haskell,
Miranda, Clean, Gofer, Opal, Prolog, C, C++, Smalltalk, Pascal, Cobol, 
Fortran, Sisal, Modula-2, Oberon, Occam, Lisp, Scheme, Ada, Eiffel, Spark, 
etc. We are not looking for formal semantics of languages such as PCF,
simple "while" languages or xy-"like" languages.

Semantics given in formalisms such as 

- action semantics 
  see, e.g.,
  - P. Mosses, Action semantics, Cambridge University Press, 1992
  - D. Watt, Programming language syntax and semantics, Prentice Hall, 1991

- axiomatic semantics
  see, e.g.,
  - D. Gries, The science of programming, Springer, 1981
  - J.W. de Bakker, Mathematical theory of program correctness, 
    Prentice-Hall, 1980

- denotational semantics
  see, e.g.,
  - J. Stoy, Denotational Semantics: The Scott-Strachey approach to 
    programming language theory, MIT Press, 1977
  - D. Schmidt, Denotational Semantics: A methodology for language
    development, WM.C. Brown Publishers, 1986

- evolving algebras 
  see, e.g.,
  - Y. Gurevich, Evolving algebras 1993: Lipari Guide. Specification and
    Validation Methods, E. B\"orger, editor, Oxford University Press, 1994

- natural semantics or structural operational semantics
  see, e.g.,
  - G. Plotkin, Structural operational semantics, Lecture Notes, 
    DAIMI FN-19, Aarhus University, 1981
  - M. Hennessy, The semantics of programming languages: An elementary
    introduction using structural operational semantics, Wiley, 1990

are welcome. 


There will be two lists, one for complete semantics and another for formal
semantics of significant and large parts of languages, including information 
on which constructs are not covered. Please submit only semantics that are 
published or available by ftp or WWW, to ensure public access to the 
semantics.

Below are example entries for each list. Please use the same format when
submitting your entry and specify to which list the entry belongs.

The lists are available at the WWW addresses
    http://www.ifi.unizh.ch/groups/baumann/compl_sem.html
    http://www.ifi.unizh.ch/groups/baumann/almost_compl_sem.html


Please send your entries to 

    baumann@ifi.unizh.ch


Best regards
Peter Baumann

Dept. of Computer Science
University of Zurich
Winterthurerstrasse 190
CH - 8057 Zurich, 
Switzerland
E-mail:   baumann@ifi.unizh.ch



------------------------------------------------------------------------
------------------------------------------------------------------------

        COMPLETE SEMANTICS OF REAL-WORLD PROGRAMMING LANGUAGES

------------------------------------------------------------------------
------------------------------------------------------------------------

Language:      Standard ML

Formalism:     Natural semantics

Publications/  R. Milner, M. Tofte and R. Harper, The Definition of 
Availability:  Standard ML, MIT Press, 1990

               R. Milner and M. Tofte, Commentary on Standard ML, 
               MIT Press, 1991

               S. Kahr, Mistakes and ambiguities in the definition of
               Standard ML, Report ECS-LFCS-93-257, University of
               Edinburgh 1993


------------------------------------------------------------------------

Language:      C

Formalism:     Evolving algebras

Publications/  Y. Gurevich and J. Huggins,  The semantics of the C 
Availability:  programming language, In E. B\"orger, H. Kleine B\"uning, 
               G. J\"ager, S. Martini, and M. M. Richter, editors, 
               Computer Science Logic, LNCS 702, pages 274-309, Springer, 
               1993

               Y. Gurevich and J. Huggins,  Errata to ``The semantics of
               the C programming language", In E. B\"orger, Y. Gurevich, 
               K. Meinke, editors, 
               Computer Science Logic, LNCS 832, pages 334-336, Springer, 
               1994

------------------------------------------------------------------------




------------------------------------------------------------------------
------------------------------------------------------------------------

      ALMOST COMPLETE SEMANTICS OF REAL-WORLD PROGRAMMING LANGUAGES.

------------------------------------------------------------------------
------------------------------------------------------------------------

Language:      Pascal

Formalism:     Hoare logic

Missing        real arithmetic, goto statements
Constructs:    

Publications/  C.A.R. Hoare and N. Wirth, An axiomatic definition of the
Availability:  programming language Pascal, Acta Informatica, 2, pages
               335-355, 1973

------------------------------------------------------------------------