Berghofer S., Nipkow T., Urban C., Wenzel M. Theorem Proving in Higher Order Logics

Berlin, Heidelberg.: Springer, 2009. — (xi) 516 p. — ISBN10: 3-642-03358-X. — ISBN13: 978-3-642-03358-2.22nd International Conference, TPHOLs 2009.
Munich, Germany, August 17-20, 2009. Proceedings.This volume constitutes the proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), which was held during August 17-20, 2009 in Munich, Germany. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification.
There were 55 papers submitted to TPHOLs 2009 in the full research category, each of which was refereed by at least three reviewers selected by the Program Committee. Of these submissions, 26 research papers and 1 proof pearl were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2009 also offered a venue for the presentation of emerging trends, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2009 technical report of the Technische Universit¨ at M¨ unchen.
The organizers are grateful to David Basin, John Harrison and Wolfram Schulte for agreeing to give invited talks. We also invited four tool developers to give tutorials about their systems. The following speakers kindly accepted our invitation and we are grateful to them: John Harrison (HOL Light), Adam Naumowicz (Mizar), Ulf Norell (Agda) and Carsten Sch¨ urmann (Twelf).
The TPHOLs conference traditionally changes continents each year to maximize the chances that researchers around the world can attend. TPHOLs started in 1998 in the University of Cambridge as an informal users’ meeting for the HOL system. Since 1993, the proceedings of TPHOLs have been published in the Springer Lecture Notes in Computer Science series.