This book constitutes the refereed proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 200, held in Munich, Germany, in August 2009. The 26 revised full papers presented together with 1 proof pearl, 4 tool presentations, and 3 invited papers were carefully reviewed and selected from 55 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, formalization of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.
Author(s): David Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt (auth.), Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (eds.)
Series: Lecture Notes in Computer Science 5674 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 517
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Mathematics of Computing; Discrete Mathematics in Computer Science; Algorithm Analysis and Problem Complexity; Models and Principles
Front Matter....Pages -
Let’s Get Physical: Models and Methods for Real-World Security Protocols....Pages 1-22
VCC: A Practical System for Verifying Concurrent C....Pages 23-42
Without Loss of Generality....Pages 43-59
HOL Light: An Overview....Pages 60-66
A Brief Overview of Mizar ....Pages 67-72
A Brief Overview of Agda – A Functional Language with Dependent Types....Pages 73-78
The Twelf Proof Assistant....Pages 79-83
Hints in Unification....Pages 84-98
Psi-calculi in Isabelle....Pages 99-114
Some Domain Theory and Denotational Semantics in Coq....Pages 115-130
Turning Inductive into Equational Specifications....Pages 131-146
Formalizing the Logic-Automaton Connection....Pages 147-163
Extended First-Order Logic....Pages 164-179
Formalising Observer Theory for Environment-Sensitive Bisimulation....Pages 180-195
Formal Certification of a Resource-Aware Language Implementation....Pages 196-211
A Certified Data Race Analysis for a Java-like Language....Pages 212-227
Formal Analysis of Optical Waveguides in HOL....Pages 228-243
The HOL-Omega Logic....Pages 244-259
A Purely Definitional Universal Domain....Pages 260-275
Types, Maps and Separation Logic....Pages 276-292
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence....Pages 293-309
Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL....Pages 310-326
Packaging Mathematical Structures....Pages 327-342
Practical Tactics for Separation Logic....Pages 343-358
Verified LISP Implementations on ARM, x86 and PowerPC....Pages 359-374
Trace-Based Coinductive Operational Semantics for While....Pages 375-390
A Better x86 Memory Model: x86-TSO....Pages 391-407
Formal Verification of Exact Computations Using Newton’s Method....Pages 408-423
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL....Pages 424-439
A Hoare Logic for the State Monad....Pages 440-451
Certification of Termination Proofs Using CeTA ....Pages 452-468
A Formalisation of Smallfoot in HOL....Pages 469-484
Liveness Reasoning with Isabelle/HOL....Pages 485-499
Mind the Gap....Pages 500-515
Back Matter....Pages -
