The course meets Tuesdays at 10:00 in room 3317 and Thursdays at 3:00 in room 3317, through 12 December.
The first tutorials will be at 10:00am and 4:00pm on Friday, 13 October in or near room 2501. The scheduled lecture times during the week of 16 October will be informal tutorials starting in room 3317.
The course covers foundations for and applications of computer aided formal reasoning. A rough outline is:
There is no required text for this course. You may find the books below useful as references or for further reading.
For background reading on proof, D. J. Velleman's How to Prove it: a Structured Approach (1994) is recommended.
For background mathematics, see J. K. Truss, Discrete Mathematics for Computer Scientists. This book appears to be on reserve in the JCMB library. Chapters 1,2, 5, and 6 are particularly relevant.
Larry Paulson's ML for the Working Programmer is an introduction to functional programming using ML.
The best source for information and documentation on LEGO is the LEGO home page, at http://www.dcs.ed.ac.uk/packages/lego/index.html (also accessible directly from the LFCS home page.)
Type Theory and Functional Programming, by Simon Thompson, is a useful reference as well as an introductory text. It is worth buying if you are interested in the mathematical ideas discussed in the course.
Computation and Reasoning: a type theory for computer science, by Z. Luo, is a deeper study of the theory underlying LEGO.
Proof and Types, by Girard, Lafont, and Taylor, gives detailed theoretical foundations for some of these topics.
Other related books include:
The Automation of Proof: An Historical and Sociological Exploration, by Donald MacKenzie.
The Computer Modelling of Mathematical Reasoning, by Alan Bundy.