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