Theorem Proving in Higher-Order Logics

From Wikipedia, the free encyclopedia

Theorem Proving in Higher-Order Logics (TPHOLs) is an annual international academic conference on the topic of automated reasoning in higher-order logics. The first TPHOLs was held in Cambridge, UK in 1987, but in the early years was an informal gathering of researchers interested in the HOL system and had no formal proceedings. Since 1990 TPHOLs has published formal peer-reviewed proceedings, published by Springer's LNCS series.

TPHOLs brings together the communities using many systems based on higher-order logic such as Coq, Isabelle, NuPRL, PVS, and Twelf. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.

Together with CADE and TABLEAUX, TPHOLs is usually one of the three main conferences of the International Joint Conference on Automated Reasoning (IJCAR) whenever it convenes,

In 2006, TPHOLs was part of the Federated Logic Conference held in Seattle, USA.