The course meets Tuesdays at noon in room 3218 and Thursdays at 2:00pm in room 3317, through 6 December.
We will be using the Lego proof assistant extensively during the course. To help you get started with the system, I plan to arrange a few lab/tutorial sessions during the first half of the course. These will probably be in the lab in room 2501.
A rough outline of the course is:
There is some flexibility in the later part of the term, and once the foundation has been laid I will offer the class a number of topics to choose from.
A couple of books on proof, useful if you do not have much experience with mathematical proofs in practice are:
Kelleman, D.J. (1994) How to Prove it: a Structured Approach. (£14.95) and
Exner, George R. (1996) An Accompaniment to Higher Mathematics. (£22.50) This book is designed for undergraduate mathematics students, but contains a good deal of practical logic as well, and is written in a very friendly style.
For background mathematics which you might need to catch up on, the following book covers the material needed without too much elaboration.
Truss, J.K. (1991) Discrete Mathematics for Computer Scientists, Addison Wesley (£19.95). See especially chapters 1, 2, 5 and 6.
For background in functional programming, using ML, see Paulson (1991) ML for the Working Programmer.
For background in lambda-calculus, see Gunter (1992), Semantics of Programming Languages, sections 2.1 and 2.2.
There is no set text for the course. Lecture notes will be distributed, which will cover all examinable material. The books below give more details on the topics covered. The most suitable for M.Sc. students are probably Thompson and chapters 7 and 8 of Luo. Ph.D. students may be interested in Proofs and Types.
Thompson, S. (1991) Type Theory and Functional Programming, Addison Wesley (about £24.95).
Luo, Z. 1994 Computation and Reasoning: a type theory for computer science. Clarendon Press, Oxford (£30.00).
Girard, Lafont and Taylor. Proofs and Types. Cambridge (about £18).
Nordstrom, B., Petersson, K. and Smith, J. (1990) Programming in Martin-Lof Type Theory: an introduction. Clarendon Press, Oxford.
For related reading in resolution and automatic theorem proving, see
Bundy, A. (1983) The Computer Modelling of Mathematical Reasoning. Academic Press.
Judith Underwood