![[The University of Leicester]](http://www.le.ac.uk/corporateid/departmentresource/000066/unilogo.gif) | Department of Mathematics & Computer Science |
 |
Next: CO3012 Computer Science Project 1
Up: Level 3
Previous: CO3007 Communication and Concurrency
CO3008 Semantics of Programming Languages
| Credits: 20 |
Convenor: Dr. R. Crole |
Semester: 2 |
| Prerequisites: |
essential: CO1011, CO1003, CO1004, CO2008 |
desirable: CO2005 |
| Assessment: |
Six 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 CO1011; and of basic
programming, such as that found in CO1003 and CO1004. 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 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. Any students who wish to discuss this option, are
welcome to contact Dr. Roy Crole, G10.
Aims
To give a broad account of operational and abstract machine semantics,
for both imperative and functional programming; and to explain type
assignment and checking for functional and imperative languages.
Objectives
- Students will be able to specify a formal language syntax for various
imperative and functional languages; they will be able to solve simple
problems, such as describing a formal syntax from a novel and informal
description.
- Knowledge of type inference and checking: Students will know
basic methods for describing type checking via inductive definitions,
and be able to apply both simple and complex (algorithm W) methods for
type inference.
- Knowledge of evaluation and transition operational semantics for various
imperative and functional languages: students will be able to develop
formal semantics from novel and informal descriptions of run time
executions; they will be able to solve unseen problems involving new
language semantics unseen in the course notes. Students will
understand deterministic execution, and the preservation of types
during program executions.
- Knowledge of abstract machines for various
imperative and functional languages: students will know how these
machines relate to the operational semantics, and be able to work out
how to compile simple, but unseen, syntax.
- Students will be able to do simple proofs based on Rule
Induction, at all stages of the module. They will have a sound
knowledge of inductive definitions, and how such definitions can be
used throughout modern (operational) semantics.
Transferable Skills
- A deep understanding of program execution, which will prove
useful when thinking about and trying to understand the execution
behaviour of large scale languages;
- knowledge of type assignment, which is applicable to many
programming languages;
- a clear understanding of what a semantic model of a programming
language is like; the concepts are 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. 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: CO3012 Computer Science Project 1
Up: Level 3
Previous: CO3007 Communication and Concurrency
Author: S. J. Ambler, tel: +44 (0)116 252 3884
Last updated: 2002-07-11
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}