The TPHOLs Conference Series

TPHOLs99 is the twelfth in a series of international conferences on the applications of higher order logic theorem proving.

The first three (two at Cambridge and one at Aarhus) were informal users' meetings for the HOL system and there were the only ones without published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver, Malta, Utah) the conference entertained an increasingly wide field of interest.

The evolution resulted in the program committee for the meeting in Turku (1996) deeming that the scope of the conference included all reasoning tools for higher order logics and adopted the name TPHOLs, being an acronym for Theorem Proving in Higher Order Logics. (The final letter being considered necessary to break the direct connection between the conference and the HOL system.) This decision has been strongly endorsed at the business sessions at Turku and Murray Hill (1997). For the first time the conference is organized outside the community of the HOL system. It witnesses the evolution of the conference and the strong interest in further interactions between different approaches of proof developments.

An extensive collection of links to various aspects of previous conferences in the series may be found below.

Associated Communities

An inspection of the proceedings of recent conferences show that the conference accommodates the user communities of a number of theorem proving systems that support higher order logics. The interested reader is referred to the web sites for these provers.

Traditions

A longstanding convention is that the annual conference should be held in a continent different to the location of the previous meeting. (It can be confidently predicted that there will be bids from America for the 2000 meeting.)

Another tradition is that the organisers for each meeting handle all aspects the conference for the whole year in consultation with the previous few organisers. This includes selection of the program committee, editing the proceedings, fund-raising, program and local arrangements.

Another responsibility of the organisers in year n is to call for bids and conduct a poll for the selection of the venue for the conference in year n+1. (In early 2000 there will be call for bids for the 2000 conference, followed by an e-mail election.)

TPHOLs Conferences

2000

The 2000 International Conference on Theorem Proving in Higher Order Logics, at Portland, USA, August 14 - 18 2000.

1999

The 1999 International Conference on Theorem Proving in Higher Order Logics, Unversity of Nice-Sophia-Antipolis, Nice, France, 14 September - 17 September 1999.

1998

The 1998 International Conference on Theorem Proving in Higher Order Logics, The Australian National University, Canberra, Australia, 28 September - 1 October 1998.

1997

The 1997 International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, New Jersey, USA, 19-22 August 1997.
BibTeX file.

1996

The 1996 International Conference on Theorem Proving in Higher Order Logics, Turku Center for Computer Science (TUCS) and Åbo Akademi University, Turku, Finland (map), 26-30 August 1996.
BibTeX file.

HOL Workshops

1995

8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, 11-14 September 1995.
BibTeX file, Papparazzi contributions.

1994

7th International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta, 19-22 September 1994.
BibTeX file / Photograph (1MB).

1993

6th International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, B.C., Canada, 10-13 August 1993.
BibTeX file / Photograph (2.6MB).

1992

5th International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium, 21-24 September 1992.
BibTeX file / Photograph (1.3MB).

1991

4th International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, 28-30 August 1991.
BibTeX file.

HOL Users Meetings

1990

3rd International HOL Users Meeting, Aarhus University, Denmark,
1-2 October 1990.
Copies of the overhead transparencies from the talks were published as a technical report (BibTeX file).
Abstracts (DVI) / Abstracts (PostScript) / Photograph (1.3MB).

1989

2nd International HOL Users Meeting, Trinity Hall, Cambridge,
14-15 December 1989.
Abstracts (DVI) / Abstracts (PostScript) / Photograph (4.3MB).

1988

1st International HOL Users Meeting, Sidney Sussex College, Cambridge,
29-30 September 1988.
Photograph (2.5MB).