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.

General Information for 2021 autumn term

Time: Mondays: 11am - 12am, Room TBC and Fridays: 4pm - 6pm, Room TBC.

Coursework Schedule:

Assesed coursework 1: published TBC / deadline for submission TBC.

Assesed coursework 2: TBC / deadline for submission TBC.

Tutorials: Tutorial exercises will be posted online (here and on CATE) before the tutorial each week, printed copies will also be available. Tutorial solutions will be published online 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.

A LEGO Turing Machine and another LEGO Turing Machine