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 http://www.win.tue.nl/~calc 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: http://www.win.tue.nl/~calc http://www.win.tue.nl/cs/ipa/uitp/ 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 Verhoeven 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 programs 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 Integration 12:30 Lunch 14:00 Erik Poll and Simon Thompson Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor 14:30 Bruno Buchberger and Wolfgang System Demonstrations Windsteiger (Details to be included later) The Theorema Language: Implementing Object- and Meta Level Usage of Symbols 15:00 Arjeh M. Cohen, Olga Caprotti, Hugo Elbers, and Herman Geuvers Connecting OpenMath to Formal Math 15:30 Break 16:00 System Demonstrations Invited Lecture, Henk Barendregt (Details to be included later) 17:00 Panel Discussion 20:00 Banquet Wednesday July 15 9:30 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 al. 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 12:30 Lunch 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 Yarrow 15:30 Break 16:00 Invited Lecture, Dana Scott A Logic for Types and Computability 17:00 Closing, Arjeh Cohen