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:	Eight worksheets: 30%	Three hour exam in May/June: 70%

Lectures:	36	Classes:	12
Tutorials:	none	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 MC111; 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. Any student without such knowledge will need to undertake a small amount of background reading to become familiar with the basic principles of functional and object oriented programming; however, the material in MC308 is taught from first principles.

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''. If you would like to learn more about the ideas behind modern programming languages, how they work, why they work, and gain a clear picture of how high and low level languages interact, then this is the course for you!

All programming languages should have a clear syntax and semantics, from the low level of microprogramming in a CPU, right up to high level programming languages. In this course you will learn methods for giving a semantics to various programming languages. The languages range from high level programming languages (such as Java, C, and Haskell) to intermediate languages (which resemble assembler). The 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. For example, Java was claimed to be type safe , which means that if a program compiles, certain run time errors cannot occur. In 1997, Java was shown to not be type safe, using ideas similar to those met in this module.

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 benefit to your future understanding of software systems. Any students who wish to discuss this option, are welcome to contact Dr. Roy Crole, G10.

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 useful in many IT and industrial jobs;
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. 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 [non-examinable]. Eager (call-by-value) evaluation semantics of a functional language with recursive function declarations. 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. Higher order type systems, and their type checking algorithms.

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

S. J. Ambler
11/20/1999