## Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, ProceedingsStefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel 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 veri?cation. There were 55 papers submitted to TPHOLs 2009 in the full research c- egory, each of which was refereed by at least three reviewers selected by the ProgramCommittee. Of these submissions, 26 researchpapers and 1 proofpearl were accepted for presentation at the conference and publication in this v- ume. In keeping with longstanding tradition, TPHOLs 2009 also o?ered 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 Munc ¨ hen. The organizers are grateful to David Basin, John Harrison and Wolfram Schulte for agreeing to give invited talks. We also invited four tool devel- ers 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 Schur ¨ mann (Twelf). |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Other editions - View all

### Common terms and phrases

abstract agent algorithm analysis applied approach arguments assertion bool called compiler complete Computer consistency construction contains correctness datatype deﬁned deﬁnition denote dependency described domain elements equal equation eval evaluation event example execution exists expression extended ﬁnite ﬁrst formal formalisation formula framework function given heap Heidelberg holds implementation induction introduced invariant Isabelle/HOL language Lemma LNCS logic match memory method names nodes Note object operator pairs predicate presented problem proof properties protocol prove reason recursive reduced relation represents requires respect rules semantics separation logic sequence speciﬁcation Springer standard step structure tactics takes termination theorem theory tion trace translation University variables veriﬁcation write