Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.uidaho.edu
Cc: hol2000@leopard.cs.byu.edu
Subject: Notes from HOL94
Date: Mon, 17 Oct 94 10:09:35 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:077320:941017090944"@cl.cam.ac.uk>

Below are notes I took during the HOL2000 (future of HOL) discussion and
business session at HOL94 in Malta. My apologies for any errors or omissions.

Richard Boulton.

------------------------------------------------------------------------------

`HOL2000' discussion at HOL94, Malta
====================================

Tom Melham (TFM) described the HOL2000 initiative and introduced the
discussion by presenting some possible topics.


Documentation for hol90
-----------------------

Stephen Brackin (SB) raised the issue of lack of documentation for hol90,
stating that his organisation needs it for customers.

Phil Windley (PW) responded by suggesting use of subcontracts.

SB reminded the community that people had agreed in Vancouver (HUG93) to
translate Reference Manual entries to hol90 but that few had actually done so.
He requested that people volunteer again and actually do some this time.

TFM asked if anyone would like to edit a hol90 version of the HOL book,
bringing fame though not fortune. Cambridge University Press could then be
approached about publishing it.

PW called for a show of hands as to who is using HOL88 and hol90. Some
observers claimed that the result was about two thirds using hol90 but others
thought it was more like half and half.

Paul Curzon (PC) suggested deleting the sources of HOL88 from the ftp servers
to encourage change over to hol90.

Konrad Slind (KS) indicated that he would not do the documentation translation
work.

Elsa Gunter (EG) said that she would continue to do it slowly.

John Harrison (JRH) remarked that he was surprised that much effort was
required.

EG noted the importance of checking any translated reference entries in an
executing hol90.


Abstract theories
-----------------

Ching-Tsun Chou (CTC) requested abstract theories.

EG responded that she has done implementations and has been working with a
student this summer on a specification for higher-order abstract theories.
Changes to support these are ready to go into hol90. On list of things to do.

PW said that in the meantime people might look at David Shepherd's translation
of the HOL88 abstract theory stuff.


Assumption hacking
------------------

TFM, noticing that the discussion was flagging, raised the perennial subject
of how to refer to assumptions in backward proofs.

CTC thought that this subject is related to abstract theories since with the
latter one has less assumptions (some are axioms instead).

EG responded that lots of assumptions will still arise due to the use of
RES_TAC and STRIP_TAC.

CTC thought that this is a problem with the resolution tactics.

TFM said that having assumptions as axioms in abstract theories is essentially
a way of naming them.

Peter Homeier (PH) would prefer to have a new subgoal package (like the one in
TPS demonstrated by Peter Andrews last year in Vancouver) tied to the user
interface. Refer to assumptions by line number.

EG thought that this would not be good for redoing proofs. This applies to use
of names as well. Need naming that is less dependent on the context.

PH agreed that he doesn't like line numbers either.

Tom Schubert (TS) said that there is no difference between numbers and names.

Mark Aagaard (MA) said that he didn't know of any experiments being done into
determining a good approach to this problem.

Kim Dam Petersen (KDP) said that he and his colleagues use explicit terms to
refer to assumptions.

EG replied that this is robust but verbose.

PC said that quoting terms is bad for proof maintenance. It breaks proofs a
lot. He suggested naming assumptions at the start of a proof and avoiding
adding new ones.

TFM said that we would have to go for some simple form of names.

CTC asked about assumptions that are automatically added.

David Fura (DF) said that he usually doesn't want to look at all the
assumptions and suggested splitting them.

PW said that in doing microprocessor verifications symbolic execution puts
stuff on the stack [of assumptions?] and this is difficult to avoid. He
proposed the use of a most general discriminator, a predicate that is just
restrictive enough to select the assumption(s) required.

EG proposed changing the notion of a goal so that some assumptions can be
labelled explicitly. The labels can be chosen by the user. This would allow
the user to (optionally) only display labelled assumptions. STRIP_TAC and
RES_TAC could still add lots of assumptions. The user would label only those
required.

TFM asked if records should be used.

PW pointed out that when a goal changes the labels will have changed so the
proof cannot be replayed.

A rapid exchange followed involving TS, PC and others.

Albert Camilleri (AC) thought that two issues were being confused:
   Why name assumptions?
   How do we maintain proofs?
With regards to naming he suggested having all ML declarations be local once
a proof has been started, then later generate a nameless script.

Prof. de Bruijn (NGdeB) said that AUTOMATH is book oriented and proofs are
objects. It was assumed that a proof got a name. Also, it is based on a
nameless lambda calculus. He suggested looking at these features of AUTOMATH
to assist in the search for a solution to the problem of referring to
assumptions.
He also said that he would like to see what fragment of HOL could be embedded
in other systems, e.g., Coq, and comparisons made.

DF wondered about having a default naming system with RES_TAC.

JRH said that the same problem of referring to things occurs in mathematics
books. In these, a star or number is used.


Versions of HOL
---------------

KS said that there are already three or four extensions of HOL. How are we
going to evaluate them?

PH requested that we keep to one system as the community is small.

TFM talked about the community as chunks drifting apart.

TS asked why.

TFM thought that this could be due to people not switching to hol90.

PC proposed freezing HOL88 and mentioned the extra work involved in building
multiple versions of tools, etc.

TFM suggested that no new tools should be developed for HOL88 and stated that
he would not develop HOL88 tools. He also said that there is a problem of lack
of control -- a `dictator' is required to direct the development.

KS said that HOL seems to be the most major theorem prover with no commercial
link. Less ad hoc methods than those currently used for development and
maintenance of HOL are required. Would some sort of company be the right front
to achieve this?

TFM said that it would not cost much to do many things. We could seek out
funding like that received to develop the documentation for HOL88 -- no
strings attached, no research results required.

Shiu-Kai Chin (SKC) enquired as to how much funding was required for the HOL88
documentation effort.

TFM related the story of how the HOL88 reference entries got written and
suggested a figure of 5,000 pounds.

Malcolm Newey (MN) asked whether it would be feasible to charge licence fees
for HOL.

SB responded that this would put some organisations off HOL, emphasizing the
importance that HOL be completely free.

PC observed that research grants often have a percentage that goes into
supporting general infrastructure. Could a percentage go into a HOL support
fund?

John Van Tassel (JVT) raised what he considered to be a more basic question:
How many people would be confident to sell work in HOL? Is the system mature
enough?

PW responded that the answer may be no, but the same is true for PVS and the
Boyer-Moore theorem prover but they both have major patrons.

SB encouraged us not to undersell ourselves. HOL is well developed.

PW agreed that HOL is as well developed as the other systems but we have no
sponsor. We also have the largest community. He thought that this was no
coincidence.

TFM asked if we can deliver value for money.

EG replied that we could since HOL is free!

SKC said he thought we could sell expertise in HOL and the tool. He wondered
about seeking NSF infrastructure grants.

PW suggested writing a proposal as a community.

AC asked if ICL are making money out of selling ProofPower [their version of
HOL].

TFM said that he didn't think ICL were selling ProofPower itself.

JRH asked who would get the money if HOL were to be sold.

TFM agreed that HOL cannot be sold as there have been too many people involved
over the years.

NGdeB said that we can still have a sponsor.

Juanito Camilleri (JC) said that we have a problem of lack of direction. What
front are we going to present to potential sponsors? Need a committee to
direct. What about demonstrating the applicability of the tool?

At this point TFM drew the discussion to a close.


Vote of thanks
==============

Malcolm Newey thanked Juanito Camilleri for hosting the conference and the
participants demonstrated their appreciation.


Business session
================

TFM introduced the business session by summarising the conference: A poster
session had been introduced this year, with a modified form of refereeing.
He believed that we had crossed the line from an informal free-for-all to a
fully peer-reviewed conference. He asked for feedback on the format. He then
handed over to the organizers of the 1995 conference including the
responsibility of arranging a vote for the location of the 1996 conference.

PW and TS took the chair.

PW asked about dates for 1995. He said that the current plan is to hold the
conference in the first or second week of August.

TS requested feedback on the format.

JRH asked how many people submitted category B papers this year.

KS asked how many were rejected outright.

TFM responded that he was not prepared to provide this information but that it
could be deduced from other statistics. He did say that there were some
outright rejections.

PC requested a later deadline for category B papers.

TS said that this makes the refereeing process more difficult.

CTC suggested that the people presenting posters be given a little bit of
time to say what their work is about.

TS considered two minute slots or just two overhead projector slides.

TS asked how long the conference should be: four days with a half day off or
three very full days. He also asked whether there should be a tutorial. He
remarked that these don't seem to have brought in many outsiders in the past.
He proposed a split day, half on model checking and half on something
theoretical, as a possibility. Tutorials on other systems are a possibility
provided they are not simply a sales pitch.

AC said that the original intention of the workshop was for HOL users to meet,
say what they were doing, etc. Things have moved on because of the growth in
the community, but he was uneasy about widening the scope.

PW said that people seemed to have taken the attitude of not submitting in
category B but would let the programme committee decide. However, category B
was intended as a means of sharing things that are not real research. There
could be as many as fifty.

TS said that there didn't seem to be enthusiasm for a half-day tutorial.

JVT responded that one can find out about model checking elsewhere.

PW queried whether, more generally, we wanted a tutorial.

TFM said that there is a great range of interest in the community which is
difficult to fit in.

TS said that the discussion over the tutorial was because they had promised
to do one and didn't want to go back on this without the community's consent.

DF requested a tutorial on the inner workings of HOL.

TS suggested that this could be a category A paper next year.

MA suggested more demos, remarking that it would be nice to have enough
machines available for people to do all sorts of things including tutorials.

TFM raised the issue of the coverage of the conference.

EG asked if higher-order is the right issue. Why not include Boyer-Moore?

PW responded that it could get too wide.

TFM characterized the scope as type-theoretic.

KS asked if the scope is really interactive theorem proving.

Sara Kalvala (SK) said that she had set-theoretic work in Isabelle but didn't
know whether to submit it. Is this covered by `higher-order'?

PW said that we could come up with a complex specification for the scope but
suggested it was better just to have people submit if the works seems
appropriate. The aim is to have HOL with a sprinkling of other things to make
it interesting.

PC asked whether the programme committee should include users of other theorem
provers.

TFM responded that yes, the committee must reflect the submissions.

TS observed that there were not many non-HOL users this year.

TS confirmed the required duration: four days with a half day off.


Summary of people's initials
============================

AC      Albert Camilleri, Hewlett-Packard
CTC     Ching-Tsun Chou, UCLA
DF      David Fura, Boeing
EG      Elsa Gunter, AT&T Bell Labs.
JC      Juanito Camilleri, Malta
JRH     John Harrison, Cambridge
JVT     John Van Tassel, U.S. Government
KDP     Kim Dam Petersen, Tele Danmark
KS      Konrad Slind, Munich
MA      Mark Aagaard, Cornell
MN      Malcolm Newey, Australian National Univ.
NGdeB   N. G. de Bruijn, Eindhoven
PC      Paul Curzon, Cambridge
PH      Peter Homeier, UCLA
PW      Phil Windley, Brigham Young
SB      Stephen Brackin, ORA Corp.
SK      Sara Kalvala, Cambridge
SKC     Shiu-Kai Chin, Syracuse
TFM     Tom Melham, Glasgow
TS      Tom Schubert, Portland State