Thirty Five years of Automath
HeriotWatt University, Edinburgh
Wednesday 10Saturday 13 April 2002
http://www.cedarforest.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 reinvented the CurryHoward
isomorphism (which should be referred to as the CurryHowardde 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 BenthemJutting 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

Peter Aczel (Manchester, UK):
Formalising Mathematics  for mathematicians and by mathematicians

Henk Barendregt (Nijmegen, NL):
Styles of formalization

Bert van BenthemJutting (Eindhoven, NL):
Proof Checking the Full Book of Landau on the Foundations of Analysis

N.G. de Bruijn (Eindhoven, NL):
The Design of Automath

Bob Constable (Cornell, USA):
Recent Results in Type Theory and their
Applications in MetaPRL and Nuprl

Catarina Coquand (Chalmers, SE)
Structured Type Theory and the Proof Checker Agda

Ingo Dahn (University of Koblenz, Germany):
Personalising Mathematical Textbooks

Gilles Dowek (INRIA, FR): Binders, models, projections and de Bruijn indices

Therese Hardin (Paris 6 and INRIARocquencourt, FR):
FOC, a certified computer algebra library

Gerard Huet (INRIA,
FR): Representation Issues for Symbolic Computation

Tudor Jebelean
(RISCLinz, Austria): Theorema: a System for the Working
Mathematician

Michael Kohlhase
(Carnegie Mellon, USA) OMDoc: An Open Markup Format for
Mathematical Documents (A Building Block for WebBased Math)

Claude Kirchner (LORIA+INRIA, Nancy, FR):
The rewriting calculus

Helene Kirchner (LORIA, Nancy, FR):
Proof assistants and rewriting techniques: an experiment with Coq and Elan

Daniel Leivant (Indiana University, USA):
Incorporating computational complexity into mathematical libraries

Jonathan Seldin (Lethbridge, Canada):
Logic and Type Theory in Theorem Provers

Andrzej Trybulec
(Bialystok, Poland):
Towards practical formalization of mathematcis

Benjamin Werner (INRIA, FR): Formalizing the 4color theorem's proof (or: "500 hundred million lemmatas")

Freek Wiedijk
(Nijmegen, NL): A contemporary implementation of Automath
and The Fundamental Theorem of Algebra
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, HeriotWatt, 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 noninclusive
list of topics are welcome:

lambda calculus, type theory, logic, rewriting

theorem proving, automated reasoning, proof checking, verification of proofs and programs

computer mathematics, automating mathematics, checking mathematics
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

24 February: submission deadline of workshop papers.

5 March: notification of acceptance for the workshop papers.

15 March: revision of accepted paper for inclusion in informal
workshop proceedings.

25 March: deadline for registration for participating at the workshop.

1013 April: workshop on 35 years of Automath.

25 May: submission deadline of papers for the Special Issue on
Mechanising and Automating Mathematics in the Journal of Automated Reasoning.
Here is the call:
http://www.cedarforest.org/forest/events/automath2002/AR.html

10 July: submission deadline of special edited book celebrating
de Bruijn's 85th anniversary.
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:

Mauricio AyalaRincon (Brasilia University, Brasil)

Randall Holmes (Boise State University, USA)

Fairouz Kamareddine (chair)
(HeriotWatt University, UK)

Rob Nederpelt (Eindhoven University of Technology, NL)

Giovanni Sambin (University of Padova, IT)

Joe Wells (HeriotWatt University, UK)
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 lessfavoured 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
nonstudents 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):
 PhD students pay UK £ 21 per night for a single en suite
room and £ 16 per night for a single room with shared facilities
(evidence of full time student status is required). All without breakfast.
 Nonstudents pay UK £ 29 for a single en suite room without
breakfast.

Luxurious accommodation which includes ensuite, telephone and tv, is
available in a limited number at UK £ 35 pounds per night without
breakfast.
How to register and book accommodation
To register, send name, affiliation, address, email, 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 HeriotWatt University and
labelled "Automath 2002".
Post applications for registration to Professor
Fairouz Kamareddine, Attention Automath 2002,
HeriotWatt 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.cedarforest.org/forest/events/automath2002/
Last modified: Friday 10 May 2002.