I propose to organise TPHOLs 2006 as a part of
FLoC 2006 (Federated Logic Conference). An information about
previous FLoCs can be found on the following Web pages:
| FLoC 1996 (Rutgers University, New Jersey, USA); |
| FLoC 1999 (Trento, Italy); |
| FLoC 2002 (Copenhagen, Denmark) |
The following conferences have agreed to be part of FLoC 2006 (for convenience, I provide links to some of the previous conferences).
Having TPHOLs as part of FLoC has many advantages. The participants of TPHOLs will be able to attend other highly relevant events, such as CAV, IJCAR, RTA, SAT, a large number of FLoC workshops (see the FLoC 2002 Workshop Programme for an example), and a number of interesting invited talks at other conferences.
The organisers of the conference will include:
Andrei Voronkov (The University of Manchester).
In August 2006 I will be a visiting researcher at Microsoft Research Redmond. MSR Redmond is heavily involved in organising FLoC 2006. I expect to work in cooperation with some of the past organisers of TPHOLs:
| Tom Melham | (Oxford University); |
| John Harrison | (Intel Corporation). |
The Programme Committee will have a broad representation from the user communities and implementors of the various higher order logic theorem provers, from the major application areas, and with some representation of other theorem proving communities.
Local arrangements will be handled by FLoC.
FLoC will be held Thursday, August 10 - Wednesday, August 23, 2006. The time for individual conferences is to be fixed later. It is likely that the first and the last days will be reserved for workshops and tutorials only.
We expect the conference to consist of four days of fully refereed research paper presentations, talks by invited speakers, and poster sessions for work-in-progress. TPHOLs 2005 aimed at "providing plenty of time between the formal sessions for attendees to mingle and converse". Having plenty of time between the formal sessions at a multi-conference such a FLoC may result in people escaping to other events, so I propose to schedule one or two informal events as part of the formal programme.
As in previous years we will seek to publish the main proceedings as a volume of Springer's Lecture Notes in Computer Science, and offer a venue for the presentation of work-in-progress published as a separate volume. Both volumes will be prepared in time to be available for the conference.
All financial arrangements at FLoC will be centralised. For example, there will be a uniform policy on registration fees. However, the constituent conferences will be independent in using the money they raise. I am confident that I will be able to attract additional financial support from Microsoft Research for TPHOLs. This money can be spent either for having extra invited speakers or for student bursaries.
The TPHOLs call for bids explicitly mentioned the possibilities of having TPHOLs as an independent conference in FLoC or as part of IJCAR. A quick look at the proceedings of IJCAR 2001 and IJCAR 2004 suggests that IJCAR has a very strong resemblance with CADE. For deduction conferences with strong identities (such as TPHOLs, Calculemus, and SAT) it is probably preferable not to join IJCAR as long as this situation remains unchanged. I expressed my concern to the IJCAR Steering Committee, proposing to change the format of IJCAR to have separate streams with their own programme subcommittees (similar to the way IJCAI is organised). However, the Committee felt that the time is too short to change the format of IJCAR 2006 and welcomed to have a discussion on this topic in future.
Given this opinion expressed by the IJCAR Steering Committee, and having in mind no disregard for it, I therefore feel that it is more appropriate for TPHOLs 2006 to be an independent conference in FLoC. Firstly, this will enable more works in the area to be published in the conference proceedings. Secondly, this will give the TPHOLs community to have a full four-day slot in the main programme of FLoC, allowing the conference to make a greater impact.