Models of Computation

Module aims

This module focuses on formal descriptions (models) of computational behaviour. You will learn about:

• the operational semantics (formal description)  of a simple 'WHILE' programming language
• the operational semantics of other styles of real-world languages, such as Java and Haskell
• equivalent  definitions of algorithm, initiated in the 1930s and providing the foundations for programming languages and computation

Learning outcomes

Upon successful completion of this module, you will be able to:

• provide formal descriptions of the precise behaviour of several styles of programming language
• prove properties of such languages
• provide several formal definitions of algorithm
• link the definition of algorithm with the fundamental notion of a computable function   

Module syllabus

This module covers the following topics:

• operational semantics for a simple while language (WHILE) and many extensions
• simple properties of programming language such as confluence and totality
• inductive proofs or counter examples of such properties for WHILE and extensions
• an introduction to simple featherweight semantics for other styles of programming languages
• register machines and the universal register machine
• computable functions expressed as register machines
• the Halting problem for register machines
• Turing machines
• the lambda calculus with language properties such as confluence and totality
• the Church-Turing thesis   

Teaching methods

This module introduces mathematical techniques which provide formal descriptions of computational behaviour. The material is taught through traditional lectures, backed up by unassessed, formative tutorial exercises, all designed to reinforce understanding of the comprehensive course notes that accompany the module. The tutorial exercises will be accompanied by specimen answers, and the tutorials will be supported by Graduate Teaching Assistants (GTAs). The tutorial questions will include past exam questions, in preparation for the final exam.       

An online service will be used as a discussion forum for the module.

Assessments

The module will feature two courseworks which carry 20% of the marks, and one exam which carries the remaining 80% of the marks. The first coursework can be undertaken either on your own or in pairs. The second course work is an individual exercise.        

                               
There will be detailed feedback on the coursework exercises, including comprehensive written answers, written feedback on your individual submission, and an in-class question and answer session with an explanation of the common pitfalls and suggestions for improvement.   

Reading list

Supplementary

• Semantics with Applications: An Appetizer

  Nielson, Hanne Riis. author.

  London : Springer London

• Introduction to automata theory, languages, and computation

  Hopcroft, John E.,

  Third edition.; Pearson new international edition., Pearson

• The formal semantics of programming languages : an introduction / [electronic resource]

  Winskel, G.

  MIT Press

• Introduction to automata theory, languages, and computation

  Hopcroft, John E.,

  3rd ed./Pearson International Edition., Pearson/Addison-Wesley

• The semantics of programming languages : an elementary introduction using structural operational semantics

  Hennessy, Matthew.

  Wiley

• Lambda-calculus and combinators, an introduction

  Hindley, J. Roger.

  Cambridge University Press

• The Lambda Calculus

  H.P. Barendregt

• The lambda calculus : its syntax and semantics

  Barendregt, H. P.

  Rev. ed., North-Holland

• Introduction to the theory of computation

  Sipser, Michael, author.

  Third edition., Cengage Learning

• Computational complexity

  Papadimitriou, Christos H.

  Addison-Wesley

Module leaders

Dr Herbert Wiklicky
Professor Sophia Drossopoulou