|
TPHOLs 2005
Oxford, UK
22-25 August 2005
|
|
|
|
|
|
|
|
|
Business Meeting
Minutes of the business meeting of TPHOLs 2005.
25 August 2005, Martin-Wood Lecture Theatre, Oxford, England.
Taken by Ed Smith.
Key:
MA Mark Adams
RA Rob Arthan
PC Paul Curzon
LD Louise Dennis
JH Joe Hurd
JHar John Harrison
JHi Jason Hickey
PH Peter Homeier
PJ Paul Jackson
MK Matt Kaufman
CM Cesar Munoz
JM John Matthews
TM Tom Melham
MN Michael Norrish
SO Steven Obua
WP Wolfgang Paul
KS Konrad Slind
ST Sofiene Tahar
BW Burkhart Wolff
CW Carl Witty
GW Graham White
-- Welcome --
TM: Welcomes everybody to the meeting.
Explains that there is no official committee for TPHOLs.
Everyone present at the meeting is together responsible for the
points raised and the decisions taken.
-- Programme --
JH: Pleased with the excellent quality of the programme contents.
There were 50 submitted papers for Mature Work, 18 for
Emerging Trends and 4 Proof Pearls.
There were 20 mature works accepted and 4 Proof Pearls.
1 Proof Pearl was rejected and 1 was a convert.
Rejected mature work was not automatically accepted for Emerging
Trends.
Believes this is better than Emerging Trends being a 'reject' category.
Believes that the Proof Pearls worked well.
Thanks the Programme Committee for their work.
Believes that the timing of submission/notification was OK.
Acceptance rate was 40-50%.
-- Sponsors --
TM: Thanks Intel Corporation for the faithful TPHOLs sponsorship.
Is very grateful to NETCA for sponsorship.
A significant amount of money was carried over from the previous
year (Konrad Slind).
-- Finances --
TM: Aimed to break even. T
Total budget of 16500-17000 pounds (excluding accommodation and
t-shirts).
Regretfully, not able to offer any travel bursaries to guarantee
no loss as we were being careful not to make a sizable profit.
Any profit made will be sent forward to next TPHOLs.
Notes that organisers use their institutions to take on the
financial responsibility of the conference - hair-raising!
-- Feedback for TPHOLs 2005 --
RA: Thought the Emerging Trends category was successfully enjoyed
<general consensus>.
MN: Thought the excursion was great.
Thought sessions seemed a bit more rushed than usual.
JH: There are normally 20 papers, but there was pressure to accept
more due to high standards. Having 4 Proof Pearls and two emerging
trends sessions probably made things feel more rushed.
PH: Thought the conference was of very high quality, but didn't feel
as relaxed as in previous years.
TM: Considers if this is an indication that the number of papers
accepted is getting close to an upper bound.
KS: Considers this likely.
MK: Things that everything about the conference seemed about right
<agreeing consensus>.
TM: Explains that most of the cost was spent on obtaining a good
lecture theatre and facilities as this is where the most time was
spent. This was personally appreciated by Tom and he suggests the
same for the future.
MN: It was good to have good AV.
TM: The AV is normally 'OK' but this time we went for the best.
PH: (e-)Mailing talk slides in advance so that they were ready-to-go made
everything go smoother and reduced the cross-over time.
JM: Always interested in hearing about ACL2 and asks if anything else
can be done to make it clear that ACL2 talks are welcome.
JH: Explains that ACL2 submissions were explicitly encouraged on the
call for papers.
MK: Thanks for this gesture.
TM: Relations with Springer seem very smooth.
They very easily accepted our request.
JH: Springer did email everyone a proof of their paper with the wrong
conference title on it which caused some confusion.
-- IJCAR Presentation and Discussion --
TM: TPHOLs 2006 is subsumed into IJCAR.
JHar: Shows IJCAR information.
JH: Summarises how we ended up in IJCAR.
The programme committee had to decide on the validity of the IJCAR
bid because it was after the previous business meeting. They voted
that the bid was valid. The bid was then won by IJCAR.
JHar: Shows IJCAR web page: http://ijcar06.uni-koblenz.de/index.html
Explains that TPHOLs is subsumed within IJCAR (6 days long) which is itself
contained within FLoC (10th - 22nd August).
There is a joint programme committee with representatives from
each component IJCAR conference.
It is an attempt to bring together automated reasoners.
Maria Paola Bonacina is organising workshops at IJCAR.
Several workshops have been proposed. They look interesting but
are unconfirmed. These are administered by FLoC.
There will be one proceedings with multiple volumes.
Page numbers are unclear at the moment.
Parallelism of schedule and schedule conflicts are unknown at
the moment.
Parallel sessions are being avoided.
This may impact competition.
It is unknown if there will be grouping by subject matter.
PH: Is concerned that there might be fewer than ten TPHOLs papers.
JHar: There is not a risk of that.
KS: But under these tight constraints, is it possible?
JHar: Many of the components of IJCAR are quite small.
LD: Is concerned that people might not know where to submit to.
JHar: We will make sure that it is clear that TPHOLs is within IJCAR.
PJ: Will there be strong pressure for 20 minute talks with 5 minutes
for questions? What about accessibility?
JHar: There will not be this much compression.
Thinks that accessibility will not be a problem due to recent
convergence of work.
CW: Will there be separate calls for papers?
JHar: This will be discussed by IJCAR.
KS: What about emerging trends?
JHar: Emerging trends will be preserved.
MN: What about the sizes of constituent conferences in the past - are
we replacing someone? What about culture clashes?
JHar: There is a (unchanging) core of IJCAR conferences and the ones
around the edge change. Culture clashes are possible, but that
is part of the point. It may be disturbing, but it may also be
inspirational.
BW: We should maintain a TPHOLs website and scheme separate from
IJCAR to avoid the danger of disappearance.
MA: Worries about the scope. The call for papers talks about
automated reasoning but does not cater for mechanised reasoning.
PC: What about numbers for the combination of these individual
conferences?
JHar: They are of the same order of magnitude. There is a question of
competition, but there is also an incentive for attendance.
KS: These are both related. People who are not accepted may not
participate.
CM: What is the submission process? Do people send to IJCAR or to
the component conferences?
JHar: This is unknown at the moment.
WP: Observes that Shankar is employing a mechanism for cutting
salaries and suggest he reconsiders.
PH: Is concerned about not carrying much weight at IJCAR. Asks that
there is care taken to keep the character of the
conference. e.g. improvements to current theorem provers that might
not be of interest to those from the other constituent conferences.
BW: What about modelling? Something like compiler verification is
not really is not catered for by the call for papers. Suspects
that these topics might be rejected.
JHar: Suspects that this is not a problem.
CW: Likes the idea of having only a single track of talks.
SO: Asks about the call for papers not catering for formalised
mathematics <further debate about breadth of coverage>.
JHi: Asks how we ended up in the situation of being subsumed by
IJCAR. Asks who received a request for a vote on the issue, and who
responded.
JH: The turnout was low.
Vote reveals 2/3 of those present received a request for a vote on
this issue.
JHar: Summarises the points.
Will try to change the call for papers in light of discussions.
KS: Expresses concern about limited TPHOLs <-> IJCAR communication.
TM: Notes that the remaining PC will still be in communication with
IJCAR.
-- Planning for 2007 --
TM: Proposes that Oxford handles the bids for TPHOLs 2007 in Oct/Nov
this year. Proposes
JH: Is happy to take on this task.
TM: Is everyone happy with this?
<General consensus>
TM: OK - Oxford will follow the usual schedule and harvest this year's
of participant's emails in order to do this.
JM: Can we not vote after IJCAR to give the possibility of voting to
stay in IJCAR?
JH: This will not leave enough preparation time.
CW: Notes that there is no IJCAR 2007.
TM: Would like to see a vigorous 2007 to put us back where we are at
present. We have to decide whether to accept bids for sites in North
America or not. Traditionally the conference alternates between North
America and Europe.
KS: Why not accept from anywhere?
TM: Both alternatives have been voiced during the week.
MN: Is anyone inclined to but in a bid now?
JM: Are we intending to merge with IJCAR again? What is their system?
<discussion and consensus that we are trying IJCAR for one year
only at present>
TM: Vote - North American sites should be allowed to submit bids in
2007:
For: 12
Against: 16
Some abstainers.
KS: Thanks Joe Hurd and Tom Melham for a great meeting.
TM: Thanks participants.
Joe Hurd,
31 August 2005