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