EEF Foundations school in Deduction and Theorem Proving
Heriot-Watt University, Edinburgh
6-16 April 2000
Organized by computer science research centers
as part of the EEF series of
summer schools, supported by the European Commission and by
Useful Logics, Types, Rewriting,
UK Institute of Informatics,
Basic Research in Computer Science,
Institute for Programming Research and Algorithmics,
Cambridge University Computer Laboratory
Turku Centre for Computer Science,
Here is information on how to get to Edinburgh, Heriot-Watt, your accommodation,
and the school.
Here is the program of the school.
Here are the
Here is the List of
Participants at the school. Here are some
photos from the school, here are more photos and yet more photos and more and more photos and more
Grants covering, part or all of
the registration fee and accommodation are available for
eligible researchers aged 35 years or less, see below.
Lecturers/Tutors and Topics
David Aspinall (Edinburgh University, UK):
Stefano Berardi (Turin, IT): A syntax for implicit text in formal proofs
N.G. de Bruijn (Eindhoven, NL):
The Automath System for Verification of Mathematics
Robert Constable (Cornell, USA):
Types in Logic, Mathematics and Programming
(Turin, IT) and Joe Wells (Heriot-Watt University, Edinburgh)
Themes in Type Theory and Lambda Calculus with Intersection Types Daniel Hirschkoff
(ENS Lyon, FR)
The coq proof assistant
(Heriot-Watt University, Edinburgh)
Explicit Extensions in Typed Lambda calculi
Claude Kirchner (LORIA, Nancy, FR):
Computation and deductions by rewriting with ELAN
Elements of Algorithmic Proof
- Larry Paulson
(University of Cambridge, UK) and
Isabelle and Designing a Theorem Prover
(University of Edinburgh, UK) and
Jan van Eijck
Temporal and Dynamic Logics
Systems Practicals and Demonstrations
There will be systems practicals and demonstrations on
Grants cover part or all of the registration fee and accommodation.
Grants are restricted to researchers of age 35 or younger
with nationality in the European Union or associated states.
We strongly welcome applications from
women researchers, researchers who work in industry, and
researchers whose place of work is in a less-favoured region.
If you are not sure about eligibility, send an email to
Here is the form
for application for funding.
Deadline for receipt of the form is Wednesday 28 March 2000.
You will receive notification of acceptance/rejection by Wednesday 31 March 2000.
Registration The registration fee is UK £ 590 for full-time PhD students and 690 for non-PhD students.
The registration fee covers lunches, one social banquet, and coffee/tea
during breaks. Extra banquets cost UK £ 30 for full-time PhD students
and UK £ 40 for non-PhD students.
Accommodation in university halls of residence for students
and in university halls of residence/conference accommodation for
non-students is priced as follows:
To register, send name, affiliation, address, e-mail, dates of
arrival/departure and a cheque in UK £ drawn on a UK bank to cover the
registration fee and the number of nights of accommodation required.
The cheque should be made payable to Heriot-Watt University and
labelled "School in Deduction and Theorem Proving".
- PhD students pay UK £ 15 per night for a single room (evidence
of full time student status is required). No breakfast is included in this
price, but breakfast can be reserved at UK £ 5 extra per day.
- Non-students pay UK £ 30 per night for a single en suite room
with breakfast or UK £ 25 for a single en suite room without breakfast.
Luxurious accommodation which includes en-suite, telephone, tv, and restaurant
breakfast is available in a limited number at UK £ 35 pounds per night.
Post applications for registration and grants to Professor
Fairouz Kamareddine, Attention School in Deduction and Theorem Proving,
Heriot-Watt University, Computing and Electrical Engineering,
Riccarton, Edinburgh EH14 4AS, Scotland. Fax: +44 131 451 3327.
Recall that the deadline for grants is 28 March.
In order to guarantee accommodation, it is advisable that
your application is sent as soon as possible.
Questions should be sent to
and Alan Mycroft
Last modified: Friday 24 March 2000.