Workshop on Thirty Five years of Automath

Table of Contents

http://www.cedar-forest.org/forest/events/automath2002/informal-proceedings/contents.html

  • Editorial by Fairouz Kamareddine.
  • Program
  • Abstracts and list 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
  • Accepted long talks:
  • Arnon Avron (Tel Aviv, Israel): Transitive Closure and Inductive Reasoning
  • Mirna Bognar and Roel de Vrijer (Amsterdam, NL): The lambda cube with contexts
  • Michael Franssen (Eindhoven, NL) Hoare Logic with Explicit Contexts
  • Jamie Gabbay (Cambridge, UK): FM-HOL, a Higher-Order theory of names
  • Mohamed Mezghiche (Boumerdes, Algeria) and Choukri Ben-Yelles (Valence, FR): Elambda: A higher order logic extension of untyped lambda calculus
  • Christophe Raffalli and Rene David (Savoie, FR): Computer Assisted Teaching in Mathematics
  • Accepted short talks:
  • Koichi Takahashi (AIST, Japan) and Masami Hagiya (Tokyo, Japan): Formal proof of Abstract Model Checking of concurrent Grabage collection
  • Konstantin Verchinine (Paris, FR), Anatoli Degtyarev (Liverpool, UK), Alexander Lyaletski (Kiev, Ukraine) and Andrey Paskevich (Kiev, Ukraine): SAD, a System for Automated Deduction
  • Tanja Vos (Valencia, Spain) and Doaitse Swierstra (Utrecht,NL): Inductive data types with negative occurences in HOL
  • Contributed talks:
  • Chad Brown (Carnegie Mellon, USA): Solving for Sets in Higher-Order Theorem Proving
  • Ferruccio Guidi (Bologna, IT):The challenge of the Web for Mathematics
  • Fairouz Kamareddine (Heriot-Watt, UK): Lambda calculus a la Automath