Calculemus and Types 98: Call for Participation and Program

Calculemus and Types 98 / User Interfaces for Theorem Provers 1998

Call for Participation and Final Programme

Eindhoven University of Technology, The Netherlands
Monday, Tuesday and Wednesday, 13-15th July 1998 

A few years ago, several groups from the deduction and computer
algebra communities decided to work together towards the integration
of theorem provers and computer algebra systems. This collaborative
project has been called Calculemus.  The Types project has operated in
much the same direction, but with a stronger focus on Lambda-Calculus.
Significant progress has now been achieved and it has been decided
that this workshop will be fully open and provide the atmosphere for
discussion among the two communities.  

The workshop will be held in parallel with the UITP workshop on the
analysis and design of user interfaces for theorem proving assistants.

For full details of the workshop, hotel reservation and the registration 
form consult:

Early registration and hotel reservation is strongly recommended
since the number of delegates we can accommodate is limited.

Presentations in the first column of the programme are part of the
UITP workshop, presentations in the second column are Calculemus and
Types presentations. Presentations in the middle are joint.  Delegates
will be free to move between the two workshops. 

                                     Monday July 13

     8:30                                 Registration

     9:30                           Opening, Roland Backhouse

    9:35                        Invited Lecture, Joerg Siekmann
                      "CALCULEMUS" survey talk on the project achievements

    10:30                                     Break

    11:00 Richard Bornat and Bernard Sufrin       Manfred Kerber
          Using gestures to disambiguate          Towards an Open System for Theorem
          unification                             Proving

    11:30 James H. Andrews
          On the Spreadsheet Presentation of
          Proof Obligations                       Invited Lecture, Benjamin Werner
    12:00 Katherine Eastaughffe                   "Formal Proof of Buchberger's
          Support for Interactive Theorem         Algorithm"
          Proving: Some Design Principles and
          Their Application

   12:30                                      Lunch

    14:00 Olivier Pons, Yves Bertot and Laurence
          Rideau                                  Martin Dunstan, Tom Kelsey,  Steve
          Notions of dependency in proof          Linton, and Ursula Martin,
          assistants                              Light formal methods for CA systems

    14:30 Patrick Viry
          A user-interface for Knuth-Bendix       Loic Pottier and Laurent Thery
          completion                              Certified Computer Algebra

    15:00 Roland Backhouse and Richard
          Extracting proofs from documents        Thierry Coquand and Henrik Persson
                                                  Integrated Development of Algebra in
    15:15 Hans van Ditmarsch                      Type Theory
          User interfaces in natural deduction

    15:30 Ingo Dahn
          Using ILF as a User Interface for Many
          Theorem Provers

    15:45                                     Break

    16:00                      Invited Lecture, Harold Thimbleby
                      The detection and elimination of spurious complexity

                                    Tuesday July 14

     9:30                      Invited Lecture, Robert Constable
                       A Module Mechanism for Developing Algebra in Nuprl

    10:30                                     Break

    11:00                     Koichi Takahashi and Masami Hagiya
                                 Proving as Editing HOL Tactics

    11:30                                        Masaki Ishiguro and Ataru T.
          Stuart Allen
          From dy/dx to []P : a matter of        Nakagawa
          notation                               Proof Abstraction with Parametric
                                                 Specifications and Views in CafeOBJ

    12:00                                        Seref Mirasyedioglu
          Richard Moot
          Grail. An Automated Proof Assistant    The Church-Rosser Property in
          for Categorial Grammar Logics          Computer Algebra for Symbolic



    14:00                                        Erik Poll and Simon Thompson
                                                 Adding the axioms to Axiom: Towards a
                                                 system of automated reasoning in

    14:30                                        Bruno Buchberger and Wolfgang
          System Demonstrations                  Windsteiger
          (Details to be included later)         The Theorema Language: Implementing
                                                 Object- and Meta Level Usage of

    15:00                                        Arjeh M. Cohen, Olga Caprotti, Hugo
                                                 Elbers, and Herman Geuvers
                                                 Connecting OpenMath to Formal Math

    15:30                                     Break

          System Demonstrations
                                                 Invited Lecture, Henk Barendregt
          (Details to be included later)


                                        Panel Discussion

    20:00                                    Banquet

                                   Wednesday July 15

                             Invited Lecture, Jean-Raymond Abrial
                         Overview and Rationale of an Industrial Prover

    10:30                                     Break

    11:00 Nicholas Merriam, Michael Harrison    Stephan Hess, Michael Kohlhase, and
          Making Design Decisions to Support    Volker Sorge
          Diversity in Interactive Theorem      An Implementation of Distributed
          Proving                               Mathematical Services

    11:30 Joerg Siekmann, Stephan Hess, et       Alessandro Armando and Silvio Ranise
          A Distributed Graphical User           From Integrated Reasoning Specialists
          Interface for the Interactive Proof   to ``Plug-and-Play'' Reasoning
          System OMEGA                          Components

    12:00 Myla Archer, Constance Heitmeyer,
          Steve Sims                            Clemens Ballarin
          TAME: A PVS Interface to Simplify      A Challenge for Sound Integration of
          Proofs for Automata Models            Computer Algebra



    14:00 Bernard Sufrin and Richard Bornat
          User Interfaces for Generic Proof     Erica Melis
          Assistants Part II: Displaying        Combining Proof Planning with
          Proofs                                Constraint Solving

    14:30 Mike Jackson, David Benyon, Helen     Jeremy Dawson and Rajeev Gore
          Lowe                                  A Mechanised Proof System for Relation
          Using ERMIA for the Evaluation of a   Algebra using Display Logic for
          Theorem Prover Interface              Calculemus

    15:00 Paul Callaghan and Zhaohui Luo
          Mathematical Vernacular in Type
          Theory-based Proof Assistants         Michael Beeson
                                                Automatic generation of epsilon-delta
    15:15 Jan Zwanenburg                        proofs of continuity
          Aspects of the Proof-assistant

    15:30                                     Break

                                  Invited Lecture, Dana Scott
                              A Logic for Types and Computability

    17:00                             Closing, Arjeh Cohen