Theorem Proving in Higher Order Logics : 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Proceedings / edited by Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel.

Format:

Book

Contributor:

Berghofer, Stefan, editor.

Nipkow, Tobias, 1958- editor.

Urban, Christian, editor.

Wenzel, Makarius, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 5674.

Theoretical Computer Science and General Issues ; 5674

Language:

English

Subjects (All):

Computers.

Logic, Symbolic and mathematical.

Computer logic.

Computer science--Mathematics.

Computer science.

Algorithms.

Theory of Computation.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Mathematics of Computing.

Discrete Mathematics in Computer Science.

Algorithm Analysis and Problem Complexity.

Local Subjects:

Theory of Computation.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Mathematics of Computing.

Discrete Mathematics in Computer Science.

Algorithm Analysis and Problem Complexity.

Physical Description:

1 online resource (XI, 517 pages).

Edition:

First edition 2009.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.

System Details:

text file PDF

Summary:

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.

Contents:

Invited Papers

Let's Get Physical: Models and Methods for Real-World Security Protocols

VCC: A Practical System for Verifying Concurrent C

Without Loss of Generality

Invited Tutorials

HOL Light: An Overview

A Brief Overview of Mizar

A Brief Overview of Agda - A Functional Language with Dependent Types

The Twelf Proof Assistant

Regular Papers

Hints in Unification

Psi-calculi in Isabelle

Some Domain Theory and Denotational Semantics in Coq

Turning Inductive into Equational Specifications

Formalizing the Logic-Automaton Connection

Extended First-Order Logic

Formalising Observer Theory for Environment-Sensitive Bisimulation

Formal Certification of a Resource-Aware Language Implementation

A Certified Data Race Analysis for a Java-like Language

Formal Analysis of Optical Waveguides in HOL

The HOL-Omega Logic

A Purely Definitional Universal Domain

Types, Maps and Separation Logic

Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence

Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL

Packaging Mathematical Structures

Practical Tactics for Separation Logic

Verified LISP Implementations on ARM, x86 and PowerPC

Trace-Based Coinductive Operational Semantics for While

A Better x86 Memory Model: x86-TSO

Formal Verification of Exact Computations Using Newton's Method

Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL

A Hoare Logic for the State Monad

Certification of Termination Proofs Using CeTA

A Formalisation of Smallfoot in HOL

Liveness Reasoning with Isabelle/HOL

Mind the Gap.

Other Format:

Printed edition:

ISBN:

978-3-642-03359-9

9783642033599

Access Restriction:

Restricted for use by site license.