Theorem Proving in Higher Order Logics [electronic resource] :18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings / edited by Joe Hurd, Tom Melham.
by Hurd, Joe [editor.]; Melham, Tom [editor.]; SpringerLink (Online service).
Material type:
BookSeries: Lecture Notes in Computer Science: 3603Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg, 2005.Description: IX, 409 p. Also available online. online resource.ISBN: 9783540318200.Subject(s): Computer science | Logic design | Software engineering | Artificial intelligence | Computer Science | Mathematical Logic and Formal Languages | Logics and Meanings of Programs | Software Engineering | Artificial Intelligence (incl. Robotics) | Logic DesignDDC classification: 005.131 Online resources: Click here to access online | Item type | Current location | Call number | Status | Date due | Barcode |
|---|---|---|---|---|---|
| MAIN LIBRARY | QA8.9-QA10.3 (Browse shelf) | Available |
Browsing MAIN LIBRARY Shelves Close shelf browser
| Q334-342 Advances in Artificial Life | Q334-342 Text, Speech and Dialogue | Q334-342 KI 2005: Advances in Artificial Intelligence | QA8.9-QA10.3 Theorem Proving in Higher Order Logics | Q334-342 Automated Reasoning with Analytic Tableaux and Related Methods | TK5105.5-5105.9 Embedded Software and Systems | Q334-342 Rough Sets, Fuzzy Sets, Data Mining, and Granular Computing |
Invited Papers -- On the Correctness of Operating System Kernels -- Alpha-Structural Recursion and Induction -- Regular Papers -- Shallow Lazy Proofs -- Mechanized Metatheory for the Masses: The PoplMark Challenge -- A Structured Set of Higher-Order Problems -- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS -- Proving Equalities in a Commutative Ring Done Right in Coq -- A HOL Theory of Euclidean Space -- A Design Structure for Higher Order Quotients -- Axiomatic Constructor Classes in Isabelle/HOLCF -- Meta Reasoning in ACL2 -- Reasoning About Java Programs with Aliasing and Frame Conditions -- Real Number Calculations and Theorem Proving -- Verifying a Secure Information Flow Analyzer -- Proving Bounds for Real Linear Programs in Isabelle/HOL -- Essential Incompleteness of Arithmetic Verified by Coq -- Verification of BDD Normalization -- Extensionality in the Calculus of Constructions -- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic -- A Generic Network on Chip Model -- Formal Verification of a SHA-1 Circuit Core Using ACL2 -- From PSL to LTL: A Formal Validation in HOL -- Proof Pearls -- Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2 -- Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2 -- Proof Pearl: Defining Functions over Finite Sets -- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.
This book constitutes the refereed proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, held in Oxford, UK, in August 2005. The 20 revised full papers presented together with 2 invited papers and 4 proof pearls (concise and elegant presentations of interesting examples) were carefully reviewed and selected from 49 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the topics of this volume are theorem proving, verification, recursion and induction, mechanized proofs, mathematical logic, proof theory, type systems, program verification, and proving systems like HOL, Coq, ACL2, Isabelle/HOL and Isabelle/HOLCF.
There are no comments for this item.