There will be a meeting of STP in St Andrews on December 14th 2001, in the School of Computer Science, North Haugh, St Andrews, from 2.00 to 6.00 pm.

The meeting is in Theatre B of the building (labelled "Physics and Astronomy") housing the staff of the School of Computer Science. For obvious reasons, there is no mention on the outside of thisbuilding that it houses any computer scientists. It is building 19 on the map in How to get to the School of Computer Science; or maybe you need How to get to St Andrews first.

If planning to come beforehand to lunch , the arrangements are that we meet at 12.30, at the building just mentioned, for the five minute walk to New Hall, where there is a cafeteria serving cheap but dull food, and lots of space. It is building 70 on the map. Late arrivals should just go straight to New Hall---parking is available there as well as here.

RD

- 2 pm
Donald Mackenzie, University of Edinburgh

**Computers and the Sociology of Mathematical Proof**

This talk will review the histories of mathematical proofs about computer systems (that is, of formal verification) and of proofs using computer systems (automated theorem proving, the proof of the four-colour theorem), etc. It will explain why these histories are of interest to the sociology of science, will discuss the first litigation centring on the nature of mathematical proof, and will explore the "cultures of proving" within which different forms of proof are pursued.

- 3.00 pm Randy Pollack,
University of Durham

**Modules for Dependent Types Programming and Proving**Some STP meetings ago I showed a notion of modules for dependent types that is definable in Lego and Coq with induction-recursion added. This turned out to be infeasible in practice. We are currently working on a more pragmatic notion of modules with manifestly typed signatures, abstract interfaces and subtyping. There is a very simple implementation, and examples that typecheck in seconds instead of weeks. The simplicity comes from use of semantic notions in the formalization. There is still a question of pragmatics: do we have the right expressiveness to support programming and reasoning in dependent types?

- 3.30 pm Dan
Winterstein, University of Edinburgh

**Diagrammatic Reasoning in Analysis**

The aim of this project is to investigate the potential for applying a diagrammatic approach to automated reasoning. It focuses on the domain of mathematical analysis - a geometric subject, usually taught in a purely algebraic way. This is motivated by the aim of producing theorem provers whose proofs can be understood by people. The techniques developed should also have a practical application in mathematics teaching, where hopefully they will complement conventional methods. Such work also furthers understanding of the mathematical nature of diagrams.

- 4.00 pm Tea

- 430 pm Ursula
Martin, University of St Andrews

**Computational logic for dependable mathematical systems**We survey recent work by ourselves and others on the role of computational logic in applications of mathematics, in particular for augmenting computational mathematics software such as the symbolic system

*Maple*and the numerical system*Mathworks*, with a view to applications such as mathematical modelling and control theory.

Organised by R. Dyckhoff and Ursula Martin