Workshop on Thirty Five years of Automath
Invited talks
Abstracts of the invited talks.
Invited speakers and titles of invited talks:
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
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)
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 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