This is a 2nd year MEng compulsory course at the Department of Computing, Imperial College London. The course focuses on teaching students the fundamental skills involved in dealing with abstract systems and constructing proofs, through both teaching and exercises.

Description of the Course

This course provides a whirlwind tour of some of the key concepts in theoretical computer science. In particular, we will study formal descriptions (models) of computational behaviour. The course intends to make sure that all students establish a stronger foundation in the more theoretical side of Computer Science, thus better preparing them for the courses that will follow in the fourth year.

Course Outline

The course comprises two hours a week for seven weeks.

General Information for 2016 autumn term

Time: Wednesdays: 9am - 11am (Tutorial from 10am)

Thursdays: 12 - 1pm

Coursework Schedule:

Coursework 1: published 4th Nov / deadline 20th Nov 2pm

Coursework 2: published 2nd Dec / deadline 14th Dec 2pm

Tutorials: Tutorial exercises will be posted online before the tutorial each week, printed copies will also be available. Tutorial solutions will be published here before the next week’s tutorial.

Recommended Reading: H.R. Nielson and F. Nielson (1999). Semantics with Applications: A Formal Introduction, originally published in 1992 by John Wiley and Sons. Revised edition

G. Winskel (1993). The Formal Semantics of Programming Languages, MIT Press. This is an excellent introduction to both the operational and denotational semantics of programming languages.

M. Hennessy (1990). The Semantics of Programming Languages, Wiley. The book is subtitled ‘An Elementary Introduction using Structural Operational Semantics’, and provides a leisurely introduction to some of the topics in this course. Revised edition

J.E. Hopcroft, R. Motwani and J.D. Ullman (2001). Introduction to Automata Theory, Languages and Computation, 2nd edition, Addison-Wesley.

J.R. Hindley and J.P. Seldin (2008). Lambda Calculus and Combinators, an Introduction, 2nd edition, Cambridge University Press.

F. Cardone and J.R. Hindley (2006). History of Lambda-calculus and Combinatory Logic.

N,J. Cutland (1980). Computability. An Introduction to Recursive Function Theory, Cambridge University Press.

M.D. Davis, R. Sigal and E.J. Wyuker. (1994). Computability, Complexity and Languages, 2nd edition, Academic Press.

T.A. Sudkamp (1995). Languages and Machines, 2nd edition, Addison-Wesley.

Other Recommendations: Logicomix: the graphic novel Logicomix was inspired by the epic story of the quest for the Foundations of Mathematics…

Turing (A Novel about Computation), Christos Papadimitriou, Berkeley.

Scooping the Loop Snooper(© Mathematical Association of America), a poetic proof of the undecidability of the halting problem in the style of Dr Seuss by Geoffrey K. Pullum.

A real Turing machine.