MC308 Semantics of Programming Languages

Next: MC312 Computer Science Project Up: Year 3 Previous: MC307 Communication and Concurrency

MC308 Semantics of Programming Languages

Credits: 20

Convenor: Dr. R. Crole

Semester: 2

Prerequisites:	essential: MC111, MC103, MC104	desirable: MC208, MC205
Assessment:	Five worksheets: 30%	Three hour exam in May/June: 70%

Lectures:	36	Classes:	none
Tutorials:	12	Private Study:	102
Labs:	none	Seminars:	none
Project:	none	Other:	none
Total:	150

Explanation of Pre-requisites

Students taking this module should have a sound knowledge of simple discrete mathematics, such as that found in MC150; and of basic programming, such as that found in MC103 and MC104. In particular, the module will make use of sets, functions, (equivalence) relations, elementary (classical) logic, and mathematical induction. An understanding of basic programming constructs such as loops, conditionals, and assignments is required, but not necessarily large scale programming. Knowledge of functional, object oriented and concurrent programming is not required explicitly, but students will benefit from previous exposure.

Course Description

Syntax is the formal arrangement of symbols and words, often to create a language; and all programming languages have a particular syntax. Semantics is the study of meaning , and in this module we shall be concerned with the meaning of programming languages. An example will help. Consider if true then x:=3 else x:=4; and if (true) x=3; else x=4; The syntax of the two statements is clearly different, but Pascal and C(++) programmers will know that their semantics should be the same. In this example, the semantics of each statement is the ``effect on a computer at run time''.

In this course you will learn methods for giving a semantics to various programming languages. These methods vary from being quite low level (the meaning of a program is simply its effect when compiled and executed) to very high level (we give a mathematical model of the language which allows us to calculate the effect of a program, independently of a machine). We shall see that we can give both high and low level semantics to the same language syntax, and show that any one of the semantic descriptions is equivalent to any other.

You will also learn more about the notion of a type , which you will have met in previous programming courses, and how types can be used to reduce errors in program code.

By the end of this module, you will have a very sound grasp of the basic ideas on which modern programming languages are based, which will be of very great benefit to your future understanding of software systems.

Aims

To give a broad account of operational semantics, for both imperative, functional and object oriented programming; and to explain type assignment and checking for functional and imperative languages. The course will begin with the definition of a very broad language syntax which will contain features which belong to each of the three programming paradigms. Selected fragments of this syntax will be used to explain how to give different kinds of semantics, ranging from high level to low level; and how simple type checking works. The fragments we select will be chosen to illustrate the ideas of the course, while keeping technicalities to a minimum (for example, in a first course it is better to only explain type assigment for functional languages: the techniques apply to object oriented languages, but are more complex).

Objectives

To specify a language syntax L for imperative, functional and object oriented constructs;
to specify evaluation and transition semantics for fragments of L;
to define an abstract machine for an L fragment, along with a simple compiler;
to prove the correctness of the semantics;
to teach a simple type assignment algorithm for an L fragment.

Transferable Skills

A deep understanding of program execution, which will be indispensable when debugging large scale programs, in both academia and industry;
knowledge of type assignment, which is applicable to many programming languages;
a clear understanding of what a model of a programming language is like, which is applicable to languages not actually covered in this module.

Syllabus

Inductive definitions and proofs, including simultaneous inductive definitions. Rule and structural induction. Transition and evaluation semantics for an imperative language. Proofs of deterministic computation and the equivalence of the transition and evaluation semantics. An abstract machine for the execution of the imperative language. A proof of machine correctness. Eager (call-by-value) evaluation semantics of a functional language with recursive function declarations and imperative features. Lazy (call-by-name) evaluation semantics of the same language. An extension of the functional language with objects. Evaluation semantics for the object oriented language.

Reading list

Background:

C. Gunter, Semantics of Programming Languages, MIT Press, 1992.

B. Kirkerud, Programming Language Semantics, Thompson Computer Press, 1997.

D. Schmidt, The Structure of Typed Programming Languages, MIT Press, 1994.

R. D. Tennent, Semantics of Programming Languages, Prentice-Hall, 1991.

David Watt, The Syntax and Semantics of Programming Languages, Prentice Hall Computer Science.

G. Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993.

Next: MC312 Computer Science Project Up: Year 3 Previous: MC307 Communication and Concurrency

Roy L. Crole
10/22/1998