[Prev][Next][Index][Thread]
Calculemus and Types 98: Call for Participation and Program
-
To: categories@mta.ca, fsdm@it.uq.edu.au, softverf@leopard.cs.byu.edu, formal-methods@cs.uidaho.edu, relmics-list@diogenes.informatik.unibw-muenchen.de, lics-request@research.bell-labs.com, dataloger@cs.chalmers.se, afp@cs.chalmers.se, types@cs.indiana.edu, logic@cs.cornell.edu, logic@theory.lcs.mit.edu, eacsl@dimi.uniud.it, eapls@mailbase.ac.uk, eatcs-it@cs.unibo.it, mop@cs.ruu.nl, isabelle-users@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu, theorem-provers@mc.lcs.mit.edu, clics@doc.ic.ac.uk, qed@mcs.anl.gov, ccl@dfki.uni-sb.de, tapsoft@dcs.ed.ac.uk, prog-lang@diku.dk, theorynt@listserv.nodak.edu, flprog@informatik.uni-muenchen.de, reliable_computing@interval.usl.edu, uitp@dcs.gla.ac.uk, facs@lboro.ac.uk, bra-types@cs.chalmers.se, coq-club@pauillac.inria.fr, ipalist@win.tue.nl, siksleden@cs.ruu.nl, asci@twi.tudelft.nl, ozsl-list@fwi.uva.nl, protagonist@cs.kun.nl, theory-a@vm1.nodak.edu, calculemus-ig@dist.unige.it, logic-ml@logic.jaist.ac.jp, theorem-provers@ai.mit.edu, ftp@logic.at, om-announce@lars.math.fsu.edu, amast@cs.utwente.nl, rewriting@ens-lyon.fr
-
Subject: Calculemus and Types 98: Call for Participation and Program
-
From: Calculemus and Types 98 <calc@win.tue.nl>
-
Date: Tue, 2 Jun 1998 11:17:12 +0200 (MET DST)
-
cc: calc@win.tue.nl
-
Delivery-Date: Tue, 02 Jun 1998 04:42:48 -0500
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