Thirty Five years of Automath

Heriot-Watt University, Edinburgh

Wednesday 10-Saturday 13 April 2002

http://www.cedar-forest.org/forest/events/automath2002/

Automath started in 1967 by N.G. de Bruijn. Automath (automating mathematics) was the first system to use computer technology to check the correctness of whole books of mathematics. During his work on Automath, de Bruijn discovered many concepts that still remain of great relevance to the theory and practice of computation. For example, de Bruijn indices still play an important role in the implementation of programming languages and theorem provers, de Bruijn's new type systems were influential in the discovery of new powerful type systems, and de Bruijn re-invented the Curry-Howard isomorphism (which should be referred to as the Curry-Howard-de Bruijn isomorphism). The Landau book on the foundations of analysis remains the only fully encoded and checked mathematical book in any theorem prover. The Landau book was encoded by Bert van Benthem-Jutting in Automath in the early seventies.

Automath was written in Algol 60 and implemented on the primitive PCs of the sixties. Thirty five years on, both technology and theory have evolved very much and this led to impressive new directions in theorem proving and in using the computers for manipulating and checking mathematics. This workshop is to celebrate the 35th year of Automath and some of the impressive directions in using computers for mathematics. This area is so huge now, that it cannot be covered in one workshop. Hence, this workshop makes no claim that it covers all the important directions in the field.


Lecturers and Topics

Here is the list of abstracts of the invited talks at the workshop.


Accepted talks

In addition to the above list of lectures, we solicited talks that describe work in progress or work which is completed but does not yet appear in a conference or journal. See below for the submission procedure. The list of accepted talks consists of the following talks based on these long papers and these short papers.


Informal Proceedings

Here you find the Informal Proceedings of the workshop.


Travel Information

Here is information on how to get to Edinburgh, Heriot-Watt, your accommodation, and the workshop.


Program

Here is the program of the workshop.


Participants

Here is the list of participants of the workshop.


Photos

Here are some photos courtesy of Freek Wiedijk. Here are some photos courtesy of Alexander Lyaletski.


Submitting talks and papers

In addition to the above list of invited lectures, we are soliciting talks based on papers on all aspects of theory and practice related to automating/formalising mathematics. Each accepted paper will be allocated half an hour presentation and will appear in the informal proceedings of the workshop. Extended versions of the accepted papers at the workshop, will be fully refereed for consideration in the special issue of an international journal. Papers on the following non-inclusive list of topics are welcome: Please submit a maximum of 10 pages A4 papers describing work in progres or work that is completed but has not been submitted to a conference or journal. All papers submitted to the workshop will be reviewed and will appear in an informal proceedings before the workshop. After the workshop, selected papers will be refereed to journal standard and will appear in a special issue of an international journal. Outstanding work related to the theme of the workshop will be collected and refereed to appear in a special edited book that will celebrate de Bruijn's 85th anniversary in 2003. All papers must be in latex and all submissions must be in postscript or pdf. Accepted papers will be required in latex at the publishing stage.


Important dates

Send your submissions by email to Professor Fairouz Kamareddine, email:


Programme committee for selection of accepted papers at workshop

The programme committee for the selection of the papers for the workshop consists of the following:


Grants

Grants covering part or all of the registration fee are available for a limited number of applicants. We strongly welcome applications from women researchers 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 grant applications is 28 February 2002. You will receive notification of acceptance/rejection by 5 March 2002.


Cost of Registration

Registration fee before 10 March 2002 is UK £ 225 (£ 150 for PhD students). After 10 March 2002, the registration fee increases by 75 pounds. The registration fee covers refreshments, lunches, the banquet, and the informal proceedings.

Registration closes at 5 pm on Monday 25 March 2002.


Cost of Accommodation

Accommodation in university halls of residence for students and in university halls of residence/conference accommodation for non-students is priced as follows (No breakfast is included in this price, but there are many places near the accommodation and the conference site where you can purchase breakfast for a very reasonable price):


How to register and book accommodation

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 "Automath 2002".

Post applications for registration to Professor Fairouz Kamareddine, Attention Automath 2002, Heriot-Watt University, Computing and Electrical Engineering, Riccarton, Edinburgh EH14 4AS, Scotland. Fax: +44 131 451 8179.

In order to guarantee accommodation, it is advisable that your application is sent as soon as possible. The easter period is very busy in beautiful Edinburgh.

Questions

Questions should be sent to


Fairouz Kamareddine URL: http://www.cedar-forest.org/forest/events/automath2002/
Last modified: Friday 10 May 2002.