Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Fri, 9 Oct 1992 15:09:04 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08601; Fri, 9 Oct 92 06:48:19 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from enet-gw.pa.dec.com by ted.cs.uidaho.edu (16.6/1.34) id AA08596; Fri, 9 Oct 92 06:48:11 -0700 Received: by enet-gw.pa.dec.com; id AA07130; Fri, 9 Oct 92 06:47:12 -0700 Message-Id: <9210091347.AA07130@enet-gw.pa.dec.com> Received: from ricks.enet; by decwrl.enet; Fri, 9 Oct 92 06:47:16 PDT Date: Fri, 9 Oct 92 06:47:16 PDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 09-Oct-1992 0944" To: info-hol@edu.uidaho.cs.ted Apparently-To: info-hol@ted.cs.uidaho.edu Subject: Notes from the HOL'92 general discussion The HOL'92 conference included a general discussion, covering several issues of interest to the higher-order logic theorem-proving community. This is my summary. A caveat: This has been reconstituted from my highly condensed notes, and the discussion has lost a lot of flavor (and some truth) in the process. The text looks like quotes. It isn't. Each person named made a statement something like what appears here, but there was often additional discussion, and what I recorded was generally a collectively clarified opinion. My intention is to allow the discussion to be continued here on info-hol, not to provide a recording. Tom Melham opened the discussion with a list of topics we might want to talk about, and asked that we defer decision-making to an info-hol discussion, so as to include people who couldn't make it to the conference. Tom's list of topics was: 1) Voting for HOL94 2) Views on * scope (HOL + ... other systems?) * formality (refereed, informal, ... ?) * format (conference, workshop?) * organization (by host, by committee?) * location (convention on location, unconstrained) * fees and financial support Tom Melham: Is it generally understood that the conference chairman for year N will coordinate the voting on conference location for year N+1? General agreement: Yes. Phil Windley: The scope of HOL'92 is a good choice, including higher-order logic theorem provers, and not just HOL88 and other LCF decendants. Having published proceedings is good, as is the general level of formality. Elsa Gunter: The fees this year are much higher (at least in US dollars) than they have been in previous years. Let's try to keep student fees very low, because it's important to continue to have students active in the conference. Jeff Joyce: The preliminary budget for HOL'93 seems to show that low student fees are quite possible, and we're trying to keep them as low as possible. Luc Claesen: The fees for HOL'92 are in the same range as the fees of HOL'91 if both the tutorials and the workshop are included. The extras of bus transportations and dinners are also included in the '92 fee. Various companies and government bodies have been contacted for providing student grants. There is a good chance that student grants for HOL'92 are going to be obtained from the EEC along the lines of the CHEOPS ESPRIT Basic Research Action. Carl Seger: Please keep the lists of potential and actual funding sources, for the organizers of the next conferences to use. Jeff Joyce: Despite the desire to include everyone in the decision-making process, we need answers to a few questions at once, in order to continue setting up HOL'93. In particular, what should be the intended scope of HOL'93 (should it include all higher-order logic theorem provers, for example), the formality (should papers be refereed and should there be a published proceedings), and the format (how many days, and should it include things like a two-day tutorial)? Ching-Tsun Chou: I like to have more controversy, I like to hear what people using other theorem proving tools have to say. John Herbert: It's important, though, to have limits on who the conference is intended for. Mike Gordon: Contributors should be able to assume that the audience is familiar with HOL, but let's also encourage users of other provers to present their work. Mark Aagaard: As a member of the Nuprl community, the scope of HOL'92 seems appropriate to me. Jeff Joyce: Okay. How about formality? John Herbert: It's important to continue to include some forum for presentations of work-in-progress, and student work. Jeff Joyce: What about the practice of alternating conferences between North America and Europe? In the voting for HOL'94, should I accept proposals for North America? Will we always alternate? What of Australia, and Asia? Tim Leonard: Let's just avoid repeating a continent on consecutive years. General agreement: Yes. Tim Leonard: When making decisions on info-hol, don't use a strict vote, and don't use strict vetos. Trust your moderator (who is the organizer of the next year's conference, so for the coming year is Jeff Joyce). The moderator should decide whether or not a consensus has been reached. Where a consensus cannot be reached, the moderator decides. Jeff Joyce: How widely should HOL'93 be advertized? General agreement: Very widely. Jeff Joyce: How formal should it be? General agreement: Keep formally refereeing papers, including rejecting papers and publishing proceedings, but also provide a less-formal means for easily presenting student work and work-in-progress.