Final call for participation (25 March closing date)

		Thirty Five years of Automath
		Heriot-Watt University, Edinburgh
		Wednesday 10-Saturday 13 April 2002

			Registration closes on 25 March 2002
Final call for registration which closes on 25 March 2002 at 5 pm.

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.

This workshop is to celebrate the 35th year of Automath
and some of the impressive directions in using computers for

Lecturers and Topics:
+Peter Aczel (Manchester, UK): Formalising Mathematics 
			 --for mathematicians and by mathematicians 
+Andrea Asperti (Bologna, IT): 
		The challenge of the Web for 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 
+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 
+Jacques Fleuriot (Edinburgh, UK): 
	A Theory of Infinite Hyperreal Base Logarithms in Isabelle/HOL 
+Therese Hardin (Paris 6 and INRIA-Rocquencourt, FR): 
			FOC, a certified computer algebra library 
+ Gerard Huet (INRIA, FR): Title to be announced 
+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): Title to be announced 
+Claude Kirchner (LORIA, Nancy, FR): The ELAN System 
+ 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 (Poland): Towards practical formalization of mathematcis 
+Benjamin Werner (INRIA, FR): Formalizing the 4-color theorem's 
				proof (or: "500 hundred million lemmatas") 
+Freek Wiedijk (Nijmegen, NL): A contemporary Implementation of Automath and
				The Fundamental Theorem of Algebra

In addition to the above list of lectures, there are also accepted talks.
Program can be found at:

For  registration and accommodation check the URL 

Registration closes at 5 pm on 25 March.

If you have any questions, email fairouz@cee.hw.ac.uk