Program of the Workshop on 35 years of Automath

Final Schedule

http://www.cedar-forest.org/forest/events/automath2002/program.html
 
 
 

     8:00 - 9:30        REGISTRATION


Chair: Fairouz Kamareddine

9.30 - 10.30	Invited talk Styles of formalization Henk Barendregt (Nijmegen, NL)
10.30 - 11.00	BREAK
11.00 - 12.00	Invited talk Logic and Type Theory in Theorem Provers Jonathan Seldin (Lethbridge, Canada)
12.00 - 12.30	Invited talk The Design of Automath N.G. de Bruijn (Eindhoven, NL)

     12.30 - 14.00        LUNCH


Afternoon Session Chair: Gordon Plotkin

14.00 - 15.00	Invited talk Representation Issues for Symbolic Computation Gerard Huet (INRIA, FR)
15.00 - 15.30	Accepted talk Computer Assisted Teaching in Mathematics Christophe Raffalli and Rene David (Savoie, FR)
15.30 - 16.00	BREAK
16.00 - 16.45	Invited talk A contemporary implementation of Automath Freek Wiedijk (Nijmegen, NL)
16.45 - 17.15	Accepted talk Hoare Logic with Explicit Contexts Michael Franssen (Eindhoven, NL)
17.15 - 17.30	Accepted short talk SAD, a System for Automated Deduction Verchinine (Paris, FR), Degtyarev (Liverpool, UK), Lyaletski (Kiev, Ukraine) and Paskevich (Kiev, Ukraine)

Morning Session Chair: Henk Barendregt

8.45 - 9.30	Invited talk Formalising Mathematics - for mathematicians and by mathematicians Peter Aczel (Manchester, UK)
9.30 - 10.15	Invited talk Recent Results in Type Theory and their Applications in MetaPRL and Nuprl Bob Constable (Cornell, USA)
10.15 - 10.45	BREAK
10.45 - 11.00	Accepted short talk Inductive data types with negative occurences in HOL Tanja Vos (Valencia, Spain) and Doaitse Swierstra (Utrecht,NL)
11.00 - 11.30	Invited talk Proof Checking the Full Book of Landau on the Foundations of Analysis Bert van Benthem-Jutting (Eindhoven, NL)
11.30 - 12.30	Invited talk FOC, a certified computer algebra library Therese Hardin (Paris, FR)

     12.30 - 14.00        LUNCH


Afternoon Session Chair: Therese Hardin

14.00 - 15.00	Invited talk OMDoc: An Open Markup Format for Mathematical Documents Michael Kohlhase (Carnegie Mellon, USA)
15.00 - 15.30	Accepted talk Transitive Closure and Inductive Reasoning Arnon Avron (Tel Aviv, Israel)
15.30 - 16.00	BREAK
16.00 - 17.00	Invited talk Theorema: a System for the Working Mathematician Tudor Jebelean (RISC-Linz, Austria)
17.00 - 17.30	Accepted talk FM-HOL, a Higher-Order theory of names Jamie Gabbay (Cambridge, UK)
17.30 - 17.45	Accepted short talk Formal proof of Abstract Model Checking of concurrent Grabage collection Koichi Takahashi (AIST, Japan) and Masami Hagiya (Tokyo, Japan)

                       19.30         SOCIAL BANQUET  
 
 

 

Friday, 12 April 2002

Morning Session Chair: Gerard Huet

8.30 - 9.30	Invited talk Incorporating computational complexity into mathematical libraries Daniel Leivant (Indiana University, USA)
9.30 - 10.30	Invited talk Formalizing the 4-color theorem's proof (or: "500 hundred million lemmatas") Benjamin Werner (INRIA, FR)
10.30 - 11.00	BREAK
11.00 - 12.00	Invited talk The rewriting calculus Claude Kirchner (LORIA+INRIA, FR)
12.00 - 12.30	Accepted talk Elambda: A higher order logic extension of untyped lambda calculus Mohamed Mezghiche (Boumerdes, Algeria) and Choukri Ben-Yelles (Valence, FR)

     12.30 - 14.00        LUNCH


Afternoon Session Chair: Michael Kohlhase

14.30 - 15.00	Contributed talk Lambda calculus a la Automath Fairouz Kamareddine (Heriot-Watt, UK)
15.00 - 16.00	Invited talk Structured Type Theory and the Proof Checker Agda Catarina Coquand (Gotenburgh, Sweden)
16.00 - 16.30	BREAK
16.30 - 17.30	Invited talk Proof assistants and rewriting techniques: an experiment with Coq and Elan Helene Kirchner (LORIA, FR)

Saturday, 13 April 2002

Morning Session Chair: Gilles Dowek

10.00 - 11.00	Invited talk Personalising Mathematical Textbooks Ingo Dahn (Koblenz, Germany)
11.00 - 11:30	BREAK
11.30 - 12.30	Invited talk Towards practical formalization of mathematcis Andrzej Trybulec (Bialystok, Poland)

     12.30 - 14.00        LUNCH


Afternoon Session Chair: Paul Jackson

14.00 - 15.00	Invited talk Binders, models, projections and de Bruijn indices Gilles Dowek (INRIA, FR)
15.00 - 15.30	Contributed talk Solving for Sets in Higher-Order Theorem Proving Chad Brown (Carnegie Mellon, USA)
15.30 - 16.00	BREAK
16.00 - 16.45	Invited talk The Fundamental Theorem of Algebra Freek Wiedijk (Nijmegen, NL)
16.45 - 17.15	Contributed talk The challenge of the Web for Mathematics Ferruccio Guidi (Bologna, IT)
17.15 - 17.45	Invited talk On the Design of Mathematical Concepts Manfred Kerber Birmingham, UK)

                       18.00          END  of workshop on 35 years Automath
 

---

Fairouz Kamareddine URL: http://www.cedar-forest.org/forest/events/automath2002/

Last modified: Saturday 13 April 2002.