[Prev][Next][Index][Thread]
formal semantics of realworld programming languages lists

To: types@dcs.gla.ac.uk

Subject: formal semantics of realworld programming languages lists

From: Peter Baumann <baumann@ifi.unizh.ch>

Date: Thu, 29 Dec 1994 17:26:23 +0100

Approved: types@dcs.gla.ac.uk
Please forward, distribute, post, circulate:
SOLICITING CONTRIBUTIONS TO
FORMAL SEMANTICS OF REALWORLD 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 realworld 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, Modula2, 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,
PrenticeHall, 1980
 denotational semantics
see, e.g.,
 J. Stoy, Denotational Semantics: The ScottStrachey 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 FN19, 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
Email: baumann@ifi.unizh.ch


COMPLETE SEMANTICS OF REALWORLD 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 ECSLFCS93257, 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 274309, 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 334336, Springer,
1994



ALMOST COMPLETE SEMANTICS OF REALWORLD 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
335355, 1973
