Semantics of Programming Languages, spring 2001

The course Semantics of Programming Languages is given by Marcello Bonsangue. It serves students of the third and fourth year of the school in computer science at the University of Leiden. It is a compulsory course for students who have chosen the specialization in Theoretical Computer Science (in dutch: afstudeerrichting Fundamentele Informatica).

This course is worth 4 study points. It is taught in English.

In the academic year 2000/2001, the course is scheduled in the second semester.

The lessons will be given on Monday afternoon (January 15,22,29; February 5,12,19,26; March 5,12,19,26; and April 2,9,23), from 13:45 till 15.30, in room WI 403.


Objective:

A programming language can be interpreted on the basis of our intuitive concept of computation. However, an informal and vague interpretation of a programming language may cause inconsistency and ambiguity. In this course we introduce the formal semantics of programming languages, and the mathematical principles underlying it. The formal semantics of a programming language assigns to every program of the language a precise mathematical meaning. There are different reasons why this is desirable: to give programmers unambiguous and perhaps informative answers about the language in order to write correct programs, to give implementers a precise definition of the language, and to develop an abstract but intuitive model of the language in order to reason about programs and to aid program development from specifications.

The main objective of the course is the study the principles of formal notation for describing computations, and tools for analyzing and proving properties of computations. By the end of the course, the students should understand the semantics of a simple abstract programming languages, be able to prove simple equivalences between programs using the formal semantics; and have an elementary grasp of the mathematical principles underlying semantics.


Prerequisites:

Students should have followed the courses Programmeren en correctheid and Concepten van programmeertalen.


Course Outline:

The course presents various classical kinds of semantics. For historical reason the emphasis will be on formal notations for abstractly specifying how programs compute (operational semantics), on mathematical structures for describing what programs compute (denotational semantics), and, to a lesser extend, also to programming logic for reasoning about programs (axiomatic semantics).

The main differences between the semantics for imperative (state-based, non-uniform), for schematic (abstract, uniform), and for functional programs is described.


Grades:

Grading will be based on homeworks, a final examination, and (to a lesser, more informal sense) on class participation.


Required Textbook:

cover
The main text for this course is the book "The Formal Semantics of Programming Languages: An Introduction", by Glynn Winskel, The MIT Press, 1993 (ISBN 0-262-23169-7).

As supplementary text we may use the book "Control Flow Semantics", by Jaco de Bakker and Erik de Vink, The MIT Press, 1996 (ISBN 0-262-04154-5). Students may also be asked to read material from other sources that will be made available in class when needed.

Comments, remarks and suggestions can be sent to Bonsangue Marcello Last modified: Thu Aug 23 09:29:44 CEST 2001