This book constitutes the refereed proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008, held in Montreal, Canada, in August 2008.
The 17 revised full papers presented together with 1 proof pearl (concise and elegant presentations of interesting examples), 5 tool presentations, and 2 invited papers were carefully reviewed and selected from 40 submissions. The papers cover all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification such as formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalisation of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.
Author(s): Mike Gordon (auth.), Otmane Ait Mohamed, César Muñoz, Sofiène Tahar (eds.)
Series: Lecture Notes in Computer Science 5170
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2008
Language: English
Pages: 321
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering; Artificial Intelligence (incl. Robotics); Logic Design
Front Matter....Pages -
Twenty Years of Theorem Proving for HOLs Past, Present and Future....Pages 1-5
Will This Be Formal?....Pages 6-11
A Short Presentation of Coq....Pages 12-16
An ACL2 Tutorial....Pages 17-21
A Brief Overview of PVS....Pages 22-27
A Brief Overview of HOL4....Pages 28-32
The Isabelle Framework....Pages 33-38
A Compiled Implementation of Normalization by Evaluation....Pages 39-54
LCF-Style Propositional Simplification with BDDs and SAT Solvers....Pages 55-70
Nominal Inversion Principles....Pages 71-85
Canonical Big Operators....Pages 86-101
A Type of Partial Recursive Functions....Pages 102-117
Formal Reasoning About Causality Analysis....Pages 118-133
Imperative Functional Programming with Isabelle/HOL....Pages 134-149
HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier....Pages 150-166
Secure Microkernels, State Monads and Scalable Refinement....Pages 167-182
Certifying a Termination Criterion Based on Graphs, without Graphs....Pages 183-198
Lightweight Separation....Pages 199-214
Real Number Calculations and Theorem Proving....Pages 215-229
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS....Pages 230-245
Certified Exact Transcendental Real Number Computation in Coq....Pages 246-261
Formalizing Soundness of Contextual Effects....Pages 262-277
First-Class Type Classes....Pages 278-293
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL....Pages 294-309
Proof Pearl: Revisiting the Mini-rubik in Coq....Pages 310-319
Back Matter....Pages -
