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: 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. Also recommended is the following, probably still the best example of a formal language definition in existence. It's not exactly light reading though....

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.


Home : Teaching : Courses 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh