Scottish Applied Theorem Proving Day
University of St. Andrews
Friday March 14th, 1997
This meeting is intended to bring together people from Scottish
universities who are interested in theorem proving, with a focus
on applications. To this end, a number of people have been invited
to speak on their current work on applications of theorem proving.
The speakers are intended to represent a wide range of interests
in theorem proving, and it is hoped that this meeting will lead to
a fruitful exchange of ideas.
The timetable of speakers was:
- 12:00-12:30
- Steve Linton
(University of St.Andrews)
"Theorem Proving and Computer Algebra"
- 12:30-13:15
- Paul Jackson
(University of Edinburgh)
"Verifying a Garbage Collector in PVS"
- 13:15-14:30
- Lunch
- 14:30-15:30
- John Harrison
(University of Cambridge)
"Verifying Algorithms for the Transcendental Functions"
- 15:30-16:00
- Tea/Coffee Break
- 16:00-16:45
- Tom Melham
(University of Glasgow)
"Working with Name-binding Syntax in Mechanised Theories"
- 16:45-17:30
- Andrew Ireland
(Heriot-Watt University)
"On the Automation of Eureka Steps"