[Prev][Next][Index][Thread]
CFP: Thirty Five years of Automath
Thirty Five years of Automath
Heriot-Watt University, Edinburgh
Wednesday 10-Saturday 13 April 2002
First announcement and CALL FOR PAPERS
http://www.cee.hw.ac.uk/~fairouz/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:
---------------------
+Peter Aczel (Manchester, UK): Formalising Mathematics
+Andrea Asperti (Bologna, IT):
An Hypertextual Electronic Library of Mathematics
+Henk Barendregt (Nijmegen, NL): Proof-assistants for Mathematics
+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
+Catarina Coquand (Chalmers, SE):
Structured Type Theory and the Proof Checker Agda
+Ingo Dahn (University of Koblenz, Germany):
Personalising Mathematical Textbooks
+Jacques Fleuriot (Edinburgh, UK):
A Theory of Infinite Hyperreal Base Logarithms in Isabelle/HOL
+Herman Geuvers (Nijmegen, NL): The Fundamental Theorem of Algebra
+Therese Hardin (Paris 6 and INRIA-Rocquencourt, FR): The Theorem Prover FOC
+Tudor Jebelean (RISC-Linz, 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 Web-Based Math)
+Jan-Willem Klop (Amsterdam, NL): The Rewriting Theory in Automath
+Claude Kirchner (LORIA, Nancy, FR): The ELAN System
+Jonathan Seldin (Lethbridge, Canada):
Logic and Type Theory in Theorem Provers
+Andrzej Trybulec (Poland): The Theorem Prover Mizar
+speaker to be confirmed (INRIA, FR): The Theorem Prover Coq
In addition to the above list of lectures, we are soliciting talks
that describe work in progress or work which is completed but does not
yet appear in a conference or journal. See below for how to submit
papers
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:
+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 sof 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. Here are the important dates:
24 February: submission deadline of workshop papers.
10 March: notification of acceptance for the workshop papers.
20 March: revision of accepted paper for inclusion in informal
workshop proceedings.
10-13 April: workshop on 35 years of Automath.
10 May: submission deadline of papers in special issue of an
international journal.
10 July: submission deadline of special edited book celebrating
de Bruijn's 85th anniversary.
The programme committee for the selection of the papers for the
workshop consists of the following:
Mauricio Ayala-Rincon
Dirk van Dalen
Randall Holmes
Fairouz Kamareddine (chair)
Rob Nederpelt
Giovanni Sambin
Joe Wells
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 fairouz@cee.hw.ac.uk. Deadline for receipt of grant
applications is 28 February 2002. You will receive notification of
acceptance/rejection by 5 March 2002.
For information on registration, check the URL
http://www.cee.hw.ac.uk/~fairouz/automath2002/