Models of Computation

Models of Computation

This course runs in room 311 on Thursdays from 3-5 and Fridays from 11-12.

Course Material

  • Introduction to course
  • Operational Semantics of While
  • Induction (induction on the structure of derivations not examiend)
  • Denotational Semantics (not examined)
  • Register machines
  • Universal Register Machine:
  • The Halting Problem
  • Turing Machines (not examined)
  • Lambda Calculus
  • Exercises

    Exercises associated with the course will be posted here.

    There will be two assessed course exercises: one will be distributed on Friday 4th November and submitted on Tuesday 15th November by 4pm; the other will be distributed on Friday 25th November and submitted on Tuesday 6th December at 4.

    Recommended Books

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

    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, revised edition here. The book is subtitled `An Elementary Introduction using Structural Operational Semantics', and provides a leisurely introduction to some of the topics in this course.

    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.

    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

    Logicmix , 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 Acssociation 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.


    Philippa Gardner, pg @ doc.ic.ac.uk