History of ITP Conference Series

 

The Itp conference series

the tphols conference series

ITP 2012 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 mathematics.


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.  

TPHOLs 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.

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 the following provers:

Abella  -  Agda  -  ACL2  -  Coq  -  HOL   -  Epigram   -  IMPS  - Isabelle  -  LEGO   -  Matita   -  Nuprl   -  ProofPower - PVS - TPS

traditions

A 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

2nd International Conference on Interactive Theorem Proving,

The Netherlands, 22-25 August 2011 [Proceedings]

   

2011

1st International Conference on Interactive Theorem Proving,

Edinburgh, Scotland, July 11-14, 2010 [Proceedings]

   

2010

The 22nd International Conference on Theorem Proving in Higher Order Logics,

Munich, Germany, August 17-20, 2009. [ Proceedings ]

2009

2008

The 21th International Conference on Theorem Proving in Higher Order Logics,

Montreal, Canada, August 18-21, 2008. [ Proceedings ]

2007

The 20th International Conference on Theorem Proving in Higher Order Logics,

Kaiserslautern, Germany, September 10-13, 2007. [ Proceedings ]

2006

The 19th International Conference on Theorem Proving in Higher Order Logics,

merged with 3rd International Joint Conference on Automated Reasoning,

Seattle, August 17-20, 2006. [ Proceedings ]

HOL workshop

The 18th International Conference on Theorem Proving in Higher Order Logics,

Oxford, UK , 22-25 August 2005. [ Proceedings ]

2005