[Prev][Next][Index][Thread]
Final call for participation (25 March closing date)
Thirty Five years of Automath
Heriot-Watt University, Edinburgh
Wednesday 10-Saturday 13 April 2002
http://www.cee.hw.ac.uk/~fairouz/automath2002/
FINAL CALL FOR PARTICIPATION
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
mathematics.
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:
http://www.cee.hw.ac.uk/~fairouz/automath2002/program.html
For registration and accommodation check the URL
http://www.cee.hw.ac.uk/~fairouz/automath2002/
Registration closes at 5 pm on 25 March.
If you have any questions, email fairouz@cee.hw.ac.uk