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"
Return to Scottish Theorem Proving page.