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 ------------------------------------------------------------------------