--------------------------------------------

Teaching

-------------------------------------------


* COMP1000: A first year course on problem solving with finite state machines.
Taught at Leeds for several years. The notes are based upon CCS with just . and +; with Plotkin's SMC machine thrown in too. Besides the usual safe controller, vending machine, coin changer, ticket machine, worked examples include a small computer, an OS kernel, and operational semantics (via Plotkin's SMC machine).
Notes in postscript.

* COMP2000: A 2nd year course on the principles of concurrent and distributed systems.
This course builds upon COMP1000. We specify and property check concurrent systems described in CCS. The emphasis is on problem solving rather than hard line theory. Examples include applications from simulation, network protocols, asynchronous hardware, ... Notes, CWB code, and other goodies.

* COMP3000: A 3rd year course on compiler design.
This is a practical course on a few key aspects of compiler design that covers: the implementation of a compiler for a small imperative language; automatic bottom-up parsing (top down to come in later years); dynamic memory allocation for both block-structured and coroutine-based (that is real object oriented) languages; elements of garbage collection.

* COMP3200/COMP6700:
A 3rd year course introducing Programming Language Semantics
.
The emphasis is on developing practical skills: reading and understanding semantic definitions; writing them; and seeing how to use formal definitions to generate translator (compiler and/or interpreter) code; and using induction to carry out useful proofs: for example, evaluating an expression increases the stack height by 1; evaluating a command leaves the stack height unaltered; showing that compilation and interpretation give the same result.

The course has 4 parts: Setting: developing translators for a sequence of block structured languages. (This involves presenting formal of type and Structural Operational Semantics (SOS) definitions and showing how the definitions lead guide the implementation code.)
Background theory: induction; the lambda calculus.
Type Inference and Structural Operational Semantics: completing the presentation for languages with (recursive) functions and block structure and again using the formal definitions to guide code development.
Run Time Systems: this historical detour shows you how to implement block structured languages with objects (in the Simula sense).

The course is assessed by coursework only. Half the marks are given for programming translators (the target language varies from year to year); the other half is for paper and pencil exercises and proofs.

Full notes and copies of the slides are available on the course web site.

[ Home Page ]