![[The University of Leicester]](http://www.le.ac.uk/corporateid/departmentresource/000066/unilogo.gif) | Department of Mathematics & Computer Science |
 |
Next: MC312 Computer Science Project 1
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 |
Problem Classes: |
6 |
| Tutorials: |
none |
Private Study: |
96 |
| Labs: |
none |
Seminars: |
none |
| Project: |
none |
Other: |
none |
| Surgeries: |
12 |
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 background reading to become
familiar with the basic principles of functional and possibly 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
and functional 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.
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. Evaluation semantics for the object oriented
language. 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. Neilson 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.
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 1
Up: Year 3
Previous: MC307 Communication and Concurrency
Author: S. J. Ambler, tel: +44 (0)116 252 3884
Last updated: 10/4/2000
MCS Web Maintainer
This document has been approved by the Head of Department.
© University of Leicester.
![[University Home]](http://www.le.ac.uk/corporateid/navigation/unihome.gif){kind=small}
![[MCS Home]](http://www.le.ac.uk/corporateid/navigation/depthome.gif){kind=small}
![[University Index A-Z]](http://www.le.ac.uk/corporateid/navigation/index.gif){kind=small}
![[University Search]](http://www.le.ac.uk/corporateid/navigation/search.gif){kind=small}
![[University Help]](http://www.le.ac.uk/corporateid/navigation/help.gif){kind=small}