History of ITP Conference Series
History of ITP Conference Series
The Itp conference series
the tphols conference series
is the third conference on Interactive Theorem Proving
and related, ranging from theoretical foundations to
implementation aspects and applications in program
verification, security, and formalization of
The inaugural meeting of
ITP was held on 11-14 July 2010 in Edinburgh,
Scotland, as part of the Federated Logic Conference
(FLoC, 9-21 July 2010).
ITP is the evolution of the TPHOLs conference series to the broad field of interactive theorem proving. TPHOLs meetings took place every year from 1988 until 2009.
2009 was the twenty-second in a series of international conferences on
the applications of higher order logic theorem proving.
The first three (two at
Cambridge and one at Århus) were informal users' meetings for the HOL
system and 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 was strongly endorsed at the business sessions at Turku
and Murray Hill (1997).
An extensive collection of links to various aspects of previous conferences in the series may be found below.
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 the following provers:
longstanding convention is that the annual conference should be held in
a continent different to the location of the previous meeting.
Another tradition is that
the organizers for each meeting handle all aspects of the conference for
the whole year in consultation with the previous few organizers. This
includes selection of the programme committee, editing the proceedings,
fund-raising, programme and local arrangements.
Another responsibility of
the organizers 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.
ITP and tphols conferences
The Netherlands, 22-25 August 2011 [Proceedings]
Edinburgh, Scotland, July 11-14, 2010 [Proceedings]
Munich, Germany, August 17-20, 2009. [ Proceedings ]
Montreal, Canada, August 18-21, 2008. [ Proceedings ]
Kaiserslautern, Germany, September 10-13, 2007. [ Proceedings ]
The 19th International Conference on Theorem Proving in Higher Order Logics,
Seattle, August 17-20, 2006. [ Proceedings ]
Oxford, UK , 22-25 August 2005. [ Proceedings ]
Park City, Utah, USA, 14-17 September 2004.
Rome, Italy, 9-12 September 2003. [ Proceedings ]
Hampton, Virginia, USA, 20-23 August 2002. [ Proceedings ]
Edinburgh, Scotland, 3-6 September 2001. [ Proceedings ]
Unversity of Nice-Sophia-Antipolis, Nice, France, 14-17 September 1999. [ BibTeX file ]
The Australian National University, Canberra, Australia, 28 September - 1 October 1998. [ BibTeX file ]
Bell Labs, Murray Hill, New Jersey, USA, 19-22 August 1997. [ BibTeX file ]
Turku Center for Computer Science and Åbo Akademi University, Turku, Finland, 26-30 August 1996. [ BibTeX file ]
8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, 11-14 September 1995. [ BibTeX file ]
7th International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta, 19-22 September 1994. [ BibTeX file | Photograph ]
4th International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, 28-30 August 1991. [ BibTeX file ]
HOL Users meetings
1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29-30 September 1988. [ Photograph ]