Formal Programming Language Semantics
Homepage for the Informatics CS4/MSc/TPG course, Autumn 2007.
Course lecturer:
John
Longley.
I can be emailed at
jrl@inf.ed.ac.uk.
I live in JCMB Room 2603 (tel 505140).
Link to the official
Module
Descriptor Page for the course.
Lectures are in Appleton Tower Room 5.03 on Tuesdays and Fridays at 9am,
starting on Friday 21 September.
There will be no lecture on Friday 5 October.
I will arrange to fit in another lecture towards the end of the course.
Aims of course
A formal semantics for a programming language is a mathematically precise
description of the intended
meaning of each construct in the language.
In contrast to a formal
syntax for a language, which tells us which
sequences of symbols are correctly formed programs,
a formal
semantics tells us what programs will actually do
when we run them.
The ideas of semantics are of importance for language designers,
compiler writers, and programmers;
they also provide a basis for mathematical proofs of the
correctness
of programs. The aim of this course is to give an introduction to various
approaches to formal semantics (operational, denotational and axiomatic),
illustrating them by means of some very simple imperative, functional,
and object-oriented languages.
Prerequisites
Formally, no prior knowledge of programming language semantics will be
assumed, though having done the UG3
Language Semantics
and Implementation course would certainly be an advantage.
Compared with the LSI course,
the present course will have less on implementation
techniques and more on the logic and theory side.
There will be some overlap between the two courses
(mainly the basic material on semantics of imperative languages),
though I will probably skate fairly quickly
over this material in the early lectures.
The course will also require a little bit of background in imperative,
functional and object-oriented languages. If you have done any Java
or C++, for instance, that will take care of the first and last of these.
In addition, some experience of a typed functional language such as
Standard ML or Haskell is desirable (for instance, the CS3
Functional Programming and Specification course).
If you don't have this background, you might need to be willing to
do a bit of extra study.
Some of the assignments might involve writing little fragments of
Standard ML-style code.
Finally, the course is fairly mathematical in nature.
No particular mathematical knowledge is expected, but some natural
mathematical aptitude will be helpful and you will need to feel
generally comfortable working with mathematical concepts and notation.
Syllabus
(not necessarily in the order in which topics will be covered)
- General concepts:
-
Syntax versus semantics. Formal versus informal semantics.
Operational, denotational and axiomatic approaches.
Adequacy, full abstraction and completeness.
- Operational semantics:
-
Big-step semantics for a simple imperative language:
defining an evaluation relation via formal rules.
Extensions with run-time errors, side-effects, and input/output.
The exception and state conventions.
Notions of observational equivalence.
Dynamic versus static scoping; static semantics.
A simple block-structured language. Type safety.
Static semantics of a simple object-oriented language.
- Denotational semantics:
-
Denotational interpretation of an imperative language.
Differences between operational and denotational semantics.
Adequacy and compositionality.
Complete partial orders, recursion and fixed points.
Monotonicity and continuity as properties of computable operations.
A simple functional language; its denotational and operational semantics.
Call-by-name versus call-by-value. Static versus dynamic binding.
- Advanced topics:
- Introduction to game semantics.
Denotational semantics of object-oriented languages.
Assessment
The assessed coursework will consist of three exercise sheets which will
be issued during the course. These will consist of pencil-and-paper
exercises. The hand-in deadlines will be as follows:
-
Sheet 1: Friday 12 October, 9am (at the lecture if you like).
-
Sheet 2: Tuesday 13 November, 9am
-
Sheet 3: Tuesday 14 December, 4pm
For CS4 and MSc students, each exercise sheet will carry 10% of the
total credit for the course; the exam will carry 70%.
For postgraduate students, assessment will be based on whatever parts of
the exercise sheets you attempt, plus participation in the lectures.
Suggested reading
The following would be suitable as a main text for the course.
However, in previous years, students have in practice found that the
course lecture notes have been sufficient.
- G. Winskel, The Formal Semantics of Programming Languages:
an introduction, MIT Press, 1993.
Also recommended is the following, probably still the best
example of a formal language definition in existence.
It's not exactly light reading though....
- R. Milner, M. Tofte, R. Harper and D. MacQueen,
The Definition of Standard ML (Revised), MIT Press, 1997.
Lecture notes and handouts
(Meta-note: One lecture note is usually about one lecture's worth of material,
but I won't stick strictly to a practice of one lecture note per lecture.)
WARNING: For lecture notes and exercise sheets that I haven't handed
out in lectures yet, the versions here are the versions I used last year.
They probably won't change much this year, but this isn't guaranteed.
Once I have given out a lecture note or exercise sheet, the version
here is guaranteed to be this year's version.
- Note 1: What is formal semantics?
- Note 2: Goals of formal semantics
- Note 3: Operational semantics of an
imperative language
- Note 4: Semantics of IMP: the fine details
- Note 5: A language with run-time errors
- Note 6: A language with side-effects
- Note 7: Static semantics: scoping and
typing rules
- Note 8: Evaluation and binding mechanisms
- Note 9: Extended example: a fragment of Java
- Note 10: Introduction to denotational semantics
- Note 11: Adequacy and its consequences
- Note 12: Complete partial orders (CPOs)
- Note 13: A simple functional language
- Note 14: Operational semantics of PCF
- Note 15: Full abstraction and universality
- Note 16: More datatypes, and reasoning about
programs
- Note 17: Introduction to game semantics (to appear)