Scottish Theorem Proving
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
Programme:
- 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