The 14th International Conference on Theorem Proving in Higher Order Logics
3-6 September 2001, Edinburgh, Scotland
The 14th International Conference on Theorem Proving in Higher Order Logics
3-6 September 2001, Edinburgh, Scotland
[Home Page][Conference History][Call for Papers][Guide for Authors][Programme]
[Related Events][How to Get There][Weather and Tourism][Registration][Accommodation]
[Sponsors][Student Bursaries][Proceedings][Photos][Business Meeting][TPHOLs 2002]
Chaired by Richard Boulton (RB)
[Texts in square brackets are editor's remarks.]
RB asked for any comments about this year's conference.
J Moore (JM) said that he appreciated the opportunity to go to the Edinburgh Festival prior to the conference. No-one else at the meeting indicated that they had come early for the Festival.
Cesar Muñoz (CM) complained that it had been difficult to get between TPHOLs and the CHARME 2001 location.
RB explained some of the motivation for the locations of the two conferences and said that it had not originally been the intention to overlap the conferences so much.
Peter Homeier (PH) suggested that the Saturday could have been used to reduce the overlap of the two conferences.
Malcolm Newey (MN) asked whether any co-locations were being planned for 2002. The organisers of TPHOLs 2002 replied that there were other conferences that might be of interest in the USA around the same time as TPHOLs 2002 but no official co-locations were planned at present. [But see later discussion about possible attached workshops.]
JM pointed out that the timing of this year's conference was very difficult for North American academics. RB accepted the point but explained that it could not have been any earlier because accommodation would have been almost impossible to get during the Edinburgh Festival, and if the conference had been any later it would not have been practical for anyone to come early for the Festival, though it appeared that maybe only JM had done that anyway.
Victor Carreño (VC) pointed out that the dates for TPHOLs 2002 [see below] were selected to be before the start of the academic year for most U.S. universities.
RB invited discussion about the way Category B papers were dealt with this year, particularly with regard to how many of the submissions were accepted (almost all of them).
Sara Kalvala (SK) thought it was good to have the poster sessions, including the talks.
VC said that the current plan was to have only one session of posters next year but he will look into the possibility of having two sessions as in 2001.
Mike Gordon (MG) said that he is in favour of accepting most Category B submissions. One reason is that it helps in getting funding for students if they are presenting their work.
JM said that he liked the five minute talks sandwiched between other sessions. It was a nice change of pace and the talks were good.
SK expressed a concern that the Category B presentations are seen as second class, i.e., as rejects from Category A.
RB said that the Category B presentations were a mix of work that didn't make it into the Category A proceedings and new submissions.
Paul Jackson (PJ) asked about the size of Category B papers. Even printed in A5 format, with around 30 papers, the Category B proceedings was getting very large.
John Harrison (JH) asked if it was a cost issue. PJ replied that the cost was not really a problem, but more the bulk, and the issue of whether long papers are appropriate for Category B work.
Konrad Slind (KS) described the format of short papers at the CADE conference.
RB said that the CADE short papers are rather different from the traditional TPHOLs Category B work. The former are heavily refereed, and are often system descriptions.
MN thought the Category B sessions were good this year.
PH raised the subject of the length of Category A papers, there having been a reduction in the limit this year from 18 pages to 16 pages (though some thought that the limit had been 14 pages in the past).
RB said that he had suggested this change because of the tendency for papers to get too long, especially after they have grown a bit for the final version. Long papers can affect the cost of the proceedings (though PJ thought that the price boundaries for Springer LNCS are now quite fine-grained) and make too much work for the reviewers. One year RB was given a 27-page paper to referee. RB said that the size limit for papers in LNCS proceedings is typically 15 pages.
JH suggested that the Programme Chair should only worry about the number of pages if it's necessary to do so.
JM thought that the limit for this year's Computer-Aided Verification conference had been only 12 pages.
Yves Bertot (YB) thought that it is good for papers to be concise.
Shankar (NS) suggested that excess material could be made available by the author(s) on a Web site.
Getting back to the discussion about the size of Category B papers, PJ pointed out that as long as the cost of the proceedings is not a problem, there is no need to ask for the chopping down of Category A submissions that are accepted in Category B.
VC asked how to avoid making Category B sound inferior.
PJ suggested that the wording used this year was OK in that respect.
PH asked whether, in future, a time and place could be scheduled for participants to give demonstrations of their work.
RB observed that the timing of the Category B submission deadline [relative to the Category A deadline] may significantly influence the number of Category B submissions.
CM presented the proposed format for TPHOLs 2002. It will be held from 20th to 23rd August in Hampton, Virginia, USA. The proposed deadlines for papers are:
| Category A | Category B | |
| Submission: | 22 February 2002 | 17 May 2002 |
| Notification: | 22 April 2002 | 17 June 2002 |
| Camera-ready copy: | 24 May 2002 | 5 July 2002 |
There will be three and a half days of talks, a reception at the Virginia Air and Space Museum, and a boat excursion to Chesapeake Bay. There will be two invited speakers: Ricky Butler and Gerard Huet.
VC then described a proposal that had been made to hold a one-day workshop on real numbers in conjunction with TPHOLs 2002. TPHOLs will take place from Tuesday to Friday, so a workshop could take place on the Monday. People would miss talks if the workshop was run in parallel with TPHOLs. If the workshop were to go ahead, should the workshop submissions go through the TPHOLs Programme Committee? Should the accepted papers appear in the TPHOLs LNCS proceedings? VC asked for comments.
KS thought it would be great to have the workshop.
Rob Arthan (RA) agreed provided the content of the workshop is close to theorem proving.
JH mentioned a similar workshop in Lyon last year, and said that the proposal could be seen as a continuation of this.
Laurent Théry (LT) said that the Lyon workshop was half computer arithmetic and half theorem proving, with the goal being to bring the two communities together. LT was not sure that the computer arithmetic people would want to go to the USA for a one-day workshop.
VC asked LT if he would come a whole week before TPHOLs 2002, to which LT said "yes".
VC said that if the people interested in the workshop are mainly from Europe and are not very interested in TPHOLs, it is questionable whether they would come for one day. On the other hand, if the workshop is completely decoupled from TPHOLs, then the TPHOLs 2002 organisers may not want to organise the workshop. Another possibility would be to have a dedicated session about real numbers in TPHOLs, or just a discussion one evening.
YB said that the Programme Committee would then have to be arranged in a different way.
NS mentioned some kind of quota system.
JH asked what would happen if there were not enough submissions for a dedicated session.
NS thought that the workshop was a good idea.
VC asked whether the workshop should be before TPHOLs or in conjunction with it.
NS thought that it should be separate and mentioned that there had been nice workshops at CAV 2001.
PH asked whether other workshops would be considered.
VC said that he had received the proposal for the real numbers workshop from Andrew Adams. Should there be a general call for attached workshops?
Someone then asked if there could also be tutorials.
VC asked whether anyone wanted to give a tutorial.
NS said that people should be asked about this privately.
Nancy Day (ND) said that the tutorials had worked well at TPHOLs 2000.
YB asked who the tutorials would be for. There was then some slightly humorous discussion about possible tutorial topics.
ND thought that a mix of new topics to the TPHOLs community and tutorials for newcomers to the field works well.
JH suggested temporal logic model checking as a possible topic.
JM said that his tutorial at TPHOLs 2000 seemed to have been attended by a mix of HOL people and people from Intel. Next year the conference is at NASA where people may know about PVS but probably not about HOL, for example.
CM said that tutorials could be advertised around NASA to draw the attention of people who don't know about theorem proving or formal methods.
VC added that it would be difficult to guess how many people would attend.
ND suggested having tutorials every two to three years.
RB thought that every three years might be preferable because the conference tends to switch between North America and Europe every two years, though that could change, and it may be that there is more interest in tutorials in North America.
JH mentioned people who may be interested in getting back into theorem proving after doing something else.
Mark Woodcock (MW) suggested having tutorials and workshops in parallel.
MG suggested a tutorial on semi-formal methods such as David Dill's 0-In.
VC summarised that there seemed to be support for parallel workshops and tutorials.
PH thought that, for reaching out, a tutorial on lightweight (hidden) formal methods (e.g. the Extended Static Checking from Compaq Systems Research Center) would be good.
VC thought that the community should be careful not to turn the conference into a recruiting/educational activity. He then called a vote on whether there should be tutorials. The majority of the people present were in favour.
VC said that he would make a call for interest in tutorials. As for workshops, should papers be presented at them?
CM suggested having two NASA technical reports: one for the Category B papers and one for the workshop.
NS thought there should be multiple workshops, and VC agreed to make a call for them.
LT asked if there would be enough physical space at the conference location for multiple workshops.
YB pointed out that other conferences typically make a call for workshops a long time in advance.
There was then a short discussion about how to handle submissions. VC was also concerned that there might not be many participants. The TPHOLs 2002 organisers have to consider the costs.
MW suggested that workshop proposals be refereed.
CM closed the discussion by expressing his hope that the people present would be able to attend next year's conference.
RB said a final word of thanks. In particular, he thanked the sponsors of TPHOLs 2001, Intel and Microsoft Research, who he had neglected to thank at the conference dinner. RB then closed the meeting and the conference.
| CM | Cesar Muñoz, ICASE, Virginia, USA |
| JH | John Harrison, Intel Corporation, Portland, USA |
| JM | J Strother Moore, University of Texas at Austin, USA |
| KS | Konrad Slind, University of Utah, USA |
| LT | Laurent Théry, INRIA Sophia Antipolis, France |
| MG | Mike Gordon, University of Cambridge, UK |
| MN | Malcolm Newey, Australian National University |
| MW | Mark Woodcock, UK |
| ND | Nancy Day, University of Waterloo, Canada |
| NS | Natarajan Shankar, SRI International Computer Science Laboratory, USA |
| PB | Paul Black, NIST, USA |
| PH | Peter Homeier, US Department of Defense |
| PJ | Paul Jackson, University of Edinburgh, UK |
| RA | Rob Arthan, Lemma 1 Limited, UK |
| RB | Richard Boulton, University of Glasgow, UK |
| SK | Sara Kalvala, University of Warwick, UK |
| VC | Victor Carreño, NASA Langley Research Center, USA |
| YB | Yves Bertot, INRIA Sophia Antipolis, France |