[The University of Leicester]

Department of Mathematics & Computer Science



Next: CO7096 Compression Methods for Multimedia Up: MSc Previous: MSc

CO7008 Semantics of Programming Languages

CO7008 Semantics of Programming Languages

Credits: 15 Convenor: Dr. F. J. de Vries Semester: 2
Prerequisites:
Assessment: Coursework: 30% Three hour exam in May/June: 70%
Lectures: 36 Problem Classes: 6
Tutorials: none Private Study: 96
Labs: none Seminars: none
Project: none Other: none
Surgeries: 12 Total: 150

Subject Knowledge

Aims

To give a broad account of operational and abstract machine semantics, and to explain type assignment and checking, for both imperative and functional programming.

Learning Outcomes

Students should be able to: specify a formal language syntax for various languages, sometimes from a novel and informal description; explain type inference and checking, and apply both simple, and complex (algorithm W) methods for type inference; explain evaluation and transition operational semantics, for various languages, and be able to develop simple formal semantics from descriptions of run time executions; they will be able to solve problems in operational semantics, and explain basic principles; explain abstract machines for two languages and the connections with operational semantics; do simple proofs based on inductive definitions and Rule Induction, at all stages of the module.

Methods

Class sessions together with course notes, worksheets, some printed solutions, and some additional hand-outs and web support.

Assessment

Marked coursework, traditional written examination.

Subject Skills

Aims

To teach students scientific writing and problem solving skills. To teach programming principles which can be adapted to future languages.

Learning Outcomes

Students will be able to: write short, clear, note based, summaries of technical knowledge; solve abstract and concrete problems (both routine seen, and simple unseen); understand new languages by applying the programming principles taught.

Methods

Class sessions together with worksheets.

Assessment

Marked coursework, traditional written examination.

Explanation of Pre-requisites

Students taking this module should have a sound knowledge of simple discrete mathematics, such as that found in CO1011; and of basic imperative and functional programming, such as that found in CO1003, CO1004 and CO2008. 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 basic functional programming is also required, but again, not on a large scale. Any student without such knowledge will need to undertake background reading to become familiar with the basic principles of functional and possibly object oriented programming; however, the material in CO3008 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 run-time 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). 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. The high level semantics describes how a large program executes by the step-by-step execution of smaller sub-programs, whose execution is easy to specify precisely. The low level semantics works by translation of a high level language into a low level language; the simpler low level language can also be executed simply and precisely.

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.

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. 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 abstractions and local declarations. Further type checking and inference; algorithm W. The SECD machine.

Reading list

Recommended:

M. Hennessy, The Semantics of Programming Languages: An Introduction Using Structured Operational Semantics, Wiley, 1990 (out of print).

H. R. Nielson and F. Nielson, Semantics with Applications, Wiley, 1992.

Background:

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

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

J. Mitchell, Concepts in Programming Languages, Cambridge University Press, 2003.

M. Scott, Programming Language Pragmatics, Morgan Kaufmann, 2000.

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.

Resources

Course notes, web page, study guide, worksheets, handouts, lecture rooms with two OHPs, past examination papers.

Module Evaluation

Course questionnaires, course review.

Next: CO7096 Compression Methods for Multimedia Up: MSc Previous: MSc

[University Home] [MCS Home] [University Index A-Z] [University Search] [University Help]

Author: N. Rahman, tel: +44 (0)116 252 3902
Last updated: 2003-09-23
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.