HOME > Detail View

Detail View

Theorem proving in higher order logics : 20th international conference, TPHOLs 2007 Kaiserslautern, Germany, September 10-13, 2007 : proceedings

Theorem proving in higher order logics : 20th international conference, TPHOLs 2007 Kaiserslautern, Germany, September 10-13, 2007 : proceedings

Material type
단행본
Personal Author
Schneider, Klaus , 1967- Brandt, Jens , 1978-
Title Statement
Theorem proving in higher order logics : 20th international conference, TPHOLs 2007 Kaiserslautern, Germany, September 10-13, 2007 : proceedings / Klaus Schneider, Jens Brandt (eds.).
Publication, Distribution, etc
Berlin :   Springer ,   2007.  
Physical Medium
viii, 399 p. : ill. ; 24 cm.
Series Statement
Lecture notes in computer science , 0302-9743 ; 4732
ISBN
9783540745907 (pbk.) 3540745904 (pbk.)
Bibliography, Etc. Note
Includes bibliographical references and index.
Subject Added Entry-Topical Term
Automatic theorem proving -- Congresses. Logic, Symbolic and mathematical -- Congresses.
000 01133namuu2200289 a 4500
001 000045395821
005 20071101153039
008 071101s2007 gw a b 101 0 eng d
020 ▼a 9783540745907 (pbk.)
020 ▼a 3540745904 (pbk.)
040 ▼a Uk ▼b eng ▼c Uk ▼d 211009
042 ▼a ukblsr
082 0 4 ▼a 004.015113 ▼2 22
090 ▼a 004.015113 ▼b T757t
111 2 ▼a TPHOLs 2007 ▼d (2007 : ▼c Kaiserslautern, Germany)
245 1 0 ▼a Theorem proving in higher order logics : ▼b 20th international conference, TPHOLs 2007 Kaiserslautern, Germany, September 10-13, 2007 : proceedings / ▼c Klaus Schneider, Jens Brandt (eds.).
246 3 ▼a TPHOLs 2007
260 ▼a Berlin : ▼b Springer , ▼c 2007.
300 ▼a viii, 399 p. : ▼b ill. ; ▼c 24 cm.
440 0 ▼a Lecture notes in computer science , ▼x 0302-9743 ; ▼v 4732
504 ▼a Includes bibliographical references and index.
650 0 ▼a Automatic theorem proving ▼v Congresses.
650 0 ▼a Logic, Symbolic and mathematical ▼v Congresses.
700 1 ▼a Schneider, Klaus , ▼d 1967-
700 1 ▼a Brandt, Jens , ▼d 1978-
945 ▼a KINS

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 004.015113 T757t Accession No. 121158509 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

On the Utility of Formal Methods in the Development and Certification of Software.- Formal Techniques in Software Engineering: Correct Software and Safe Systems.- Separation Logic for Small-Step cminor.- Formalising Java's Data Race Free Guarantee.- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.- Formalising Generalised Substitutions.- Extracting Purely Functional Contents from Logical Inductive Types.- A Modular Formalisation of Finite Group Theory.- Verifying Nonlinear Real Formulas Via Sums of Squares.- Verification of Expectation Properties for Discrete Random Variables in HOL.- A Formally Verified Prover for the Description Logic.- Proof Pearl: The Termination Analysis of Terminator.- Improving the Usability of HOL Through Controlled Automation Tactics.- Verified Decision Procedures on Context-Free Grammars.- Using XCAP to Certify Realistic Systems Code: Machine Context Management.- Proof Pearl: De Bruijn Terms Really Do Work.- Proof Pearl: Looping Around the Orbit.- Source-Level Proof Reconstruction for Interactive Theorem Proving.- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF.- Automatically Translating Type and Function Definitions from HOL to ACL2.- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models.- Proof Pearl: Wellfounded Induction on the Ordinals Up to ? 0.- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols.- Primality Proving with Elliptic Curves.- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism.- Building Formal Method Tools in the Isabelle/Isar Framework.- Simple Types in Type Theory: Deep and Shallow Encodings.- Mizar's Soft Type System.


Information Provided By: : Aladin

New Arrivals Books in Related Fields