- Lecturer: Judith Underwood
- Email:
`jlu@dcs.ed.ac.uk` - Office: JCMB 1603
- Phone: 50 5185
- Course Assistant: Thomas Schreiber (
`tms@dcs.ed.ac.uk`)

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:

- Motivation
- Reasoning about programs
- Deriving programs using proofs
- Propositional logic
- Predicate logic
- Representing mathematical objects

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.

Wed Oct 11 11:55:23 BST 1995