![[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: Year 3
Previous: CO3007 Communication and Concurrency
CO3008 Semantics of Programming Languages
| Credits: 20 |
Convenor: Dr. F. J. de Vries |
Semester: 2 |
| Prerequisites: |
essential: CO1011, CO1003, CO1004, CO2008 |
desirable: CO2005 |
| 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: CO3012 Computer Science Project 1
Up: Year 3
Previous: CO3007 Communication and Concurrency
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.
![[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}