Amazon cover image
Image from Amazon.com

Theorem proving in higher order logics : 18th international conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings / Joe Hurd, Tom Melham (eds.).

By: Contributor(s): Material type: TextTextSeries: Lecture notes in computer science ; 3603.Publication details: Berlin ; New York : Springer, 2005.Description: 1 online resource (ix, 408 pages) : illustrationsContent type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9783540318200
  • 3540318208
  • 3540283722
  • 9783540283720
Other title:
  • TPHOLs 2005
Subject(s): Genre/Form: Additional physical formats: Print version:: Theorem proving in higher order logics.DDC classification:
  • 511.3 22
LOC classification:
  • QA76.9.A96 T655 2005eb
Online resources:
Contents:
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.
Summary: "This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during 22-25 August 2005 in Oxford, UK."
Holdings
Item type Current library Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library eBook LNCS Available
Total holds: 0

Includes bibliographical references and index.

"This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during 22-25 August 2005 in Oxford, UK."

Print version record.

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.

Powered by Koha