Minutes by Mark Staples (Cambridge University)
19 September 1995
People mentioned in these minutes are:
Burkhart Wolff, firstname.lastname@example.org
Chris Owens, email@example.com
Larry Paulson, firstname.lastname@example.org
Mark Staples, email@example.com
Norbert Vvlker, Norbert.Voelker@FernUni-Hagen.de
Ole Rasmussen, firstname.lastname@example.org
Sara Kalvala email@example.com
Sian Matthews firstname.lastname@example.org
Tobias Nipkow email@example.com
The meeting was chaired by Tobias Nipkow.
Tobias said that discussion should stick to fairly strategic issues, and that concerned people could discuss specific or technical points in groups and/or with the implementors.
From discussions with other participants prior to the session, Tobias had distilled 5 topics for general discussion:
Sean requested that the issue of Annotations also be discussed. Sara requested that the issue of Documentation also be discussed.
This set the agenda for the meeting.
Burkhart presented a slide on a proposal for persistent proof obligations for theories. He saw a need for `theory-global assumptions' arising naturally in refinement, verification, etc. He believed that a mechanism could provide support for the obligations involved in managing conservative extensions in various object logics.
Mark wanted parametrised theories for algebraic-like reasoning, modular theory development, and support for data refinement.
Some general discussion ensued about persistent proof obligations and parametrised theories (`theories with assumptions').
Tobias summarised by noting general agreement for parametrised theories. Support for proof obligations was less clear. It was felt important to separate the concerns of parametrised theories from proof obligations, but it was noted that proof obligations may be useful in the implementation of parametrised theories.
Tobias mentioned that he was considering implementing an ML-like mechanism for qualifying constant and type names by the name of their theories. There was in principle general support for a facility like this.
Norbert requested a subtype facility, so that some theories about supertypes could be reused for subtypes.
Mark requested dependent types or existential types for HOL. Larry felt that this would be a major change to HOL, but suggested a possible way for simulating it in a slightly modified HOL variant.
Norbert mentioned the success of PVS subtyping. Ole mentioned that Veritas subtyping gave more expressive freedom, at the expense of sometimes having proof obligations.
Larry suggested a possible mechanism for flagging "type conditions" for ZF-like theories so that side-conditions could be left as proof-obligations.
Norbert and Tobias raised the issues of different approaches to type classes.
Burkhart had previously presented a slide showing support for GUIs. He proposed to supply an ML interface to tk, to allow the construction of GUIs in ML, and thence for Isabelle.
Burkhart needed some support for separating the output from Isabelle, so that, for example, hooks for error, warning and standard output information could be changed to provide a method for suitable interaction with GUIs.
Burkhart also required some general method for the management of Isabelle objects for theories. Mark suggests storing these other types in the qed table.
Sean suggested that we look at previous work in the GUI-for-theorem-provers area. He suggested pillaging results (not necessarily code!) from Gilles Kahn's group. Sara suggested that the aims of that group may not match the aims of people developing a specific interface to Isabelle.
Mark wanted extra-logical information removed from theories/signatures. That is, syntactic information to be handled by an interface, with theories left to handle logical issues about dependencies of definitions, etc.
Tobias questioned if anyone has provided tools for LaTeX output of theories, etc. Ole and Chris wanted automatically extractable lists of theorems for theories, etc. Chris wanted comprehensive theorem lists available on the Web.
Ole asked about the distribution of small tools for Isabelle. Tobias suggested setting up a Web page for this purpose. Tobias mentioned a .thy to .html converter.
Burkhart asked if anyone has used the pretty-printer for non-standard tasks such as producing LaTeX output. (Alternative symbol tables may be required.) Larry mentioned problems with spacing and the current pretty-printer.
Larry says a decision procedure for linear arithmetic will be supplied. There was much rejoicing.
Concerns were expressed about issues in combining decision procedures with proof terms.
Burkhart noted that proof-obligations could document the assumptions about decision procedures which were specifically relied upon.
Sean suggested doing something like this using a becauseBDD _ facility. Tobias and Larry wanted a methodological way to ensure that an external tool is also actually called.
Sean wanted rewrite rules supporting annotations, and rippling.
Larry asked whether people meant:
Sean wanted the latter, for compliance with an MoD standard. Tobias questioned whether the standard is vague enough to allow many interpretations.
The issue was again raised about how the use, and the documentation of use, of external decision procedures interacts with a design for proof terms.
Sara noted the need for better documentation. A particular need is documentation for the construction of .thy files, and documentation internal to the .thy files included with Isabelle.
Burkhart commented that the existing documentation was, in conjunction with the mailing list, adequate for him to learn Isabelle. He wished to thank Larry and Tobias for their usually prompt and precise answers.
There was general agreement on the need for a FAQ and a `Tips and Tricks' document. It was suggested that these be available on the Web.
There was general agreement that people use the Isabelle mailing list more. People should pose questions to the Isabelle mailing list rather than an implementor, so that the frequency of FAQs can be guaged, and so that other people with similar problems can see possible solutions. The Isabelle mailing list should also be used to provide announcements and pointers to ongoing work with Isabelle.
Tobias pointed out a problem with logical frameworks is that people need to learn about both the meta-logic and any specific object-logics they use. The two manuals try to separate concerns to reduce redundancy and improve maintainability, resulting in slightly fragmented documentation, and users learning more than they want to learn.
Larry pointed out that changes are noted in release READMEs. Mark also wanted pointers to sections of the documentation which describe such changes.
The implementors subtly hinted about the general problem of implementors doing documentation, and suggested that relatively new users may be better suited to writing informative introductory or tutorial documentation.
Sara saw this as a research issue, and will do a proposal.
Sean wanted to be able to solve problems with variable decoration conventions in specification languages etc, by using annotation information to control the application of meta-theorems.
Last modified Monday, November 17, 2003