Thirty Five years of Automath
Heriot-Watt University, Edinburgh
Wednesday 10-Saturday 13 April 2002
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
Peter Aczel (Manchester, UK):
Formalising Mathematics - for mathematicians and by mathematicians
Henk Barendregt (Nijmegen, NL):
Styles of formalization
Bert van Benthem-Jutting (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 INRIA-Rocquencourt, FR):
FOC, a certified computer algebra library
Gerard Huet (INRIA,
FR): Representation Issues for Symbolic Computation
(RISC-Linz, Austria): Theorema: a System for the Working
(Carnegie Mellon, USA) OMDoc: An Open Markup Format for
Mathematical Documents (A Building Block for Web-Based 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
Towards practical formalization of mathematcis
Benjamin Werner (INRIA, FR): Formalizing the 4-color theorem's proof (or: "500 hundred million lemmatas")
(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.
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
Here you find the Informal Proceedings of the workshop.
Here is information
on how to get to Edinburgh, Heriot-Watt, your accommodation, and the
the program of the workshop.
Here is the list of participants of the workshop.
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
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
lambda calculus, type theory, logic, rewriting
theorem proving, automated reasoning, proof checking, verification of proofs and programs
computer mathematics, automating mathematics, checking mathematics
Send your submissions by email to Professor Fairouz Kamareddine,
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
25 March: deadline for registration for participating at the workshop.
10-13 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:
10 July: submission deadline of special edited book celebrating
de Bruijn's 85th anniversary.
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 Ayala-Rincon (Brasilia University, Brasil)
Randall Holmes (Boise State University, USA)
Fairouz Kamareddine (chair)
(Heriot-Watt University, UK)
Rob Nederpelt (Eindhoven University of Technology, NL)
Giovanni Sambin (University of Padova, IT)
Joe Wells (Heriot-Watt 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 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):
- 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.
- Non-students pay UK £ 29 for a single en suite room without
Luxurious accommodation which includes en-suite, telephone and tv, is
available in a limited number at UK £ 35 pounds per night without
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
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 should be sent to
Last modified: Friday 10 May 2002.