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

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

Label
Theorem proving in higher order logics : 18th international conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings
Title
Theorem proving in higher order logics
Title remainder
18th international conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings
Statement of responsibility
Joe Hurd, Tom Melham (eds.)
Title variation
TPHOLs 2005
Creator
Contributor
Subject
Genre
Language
eng
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."
Member of
Cataloging source
GW5XE
Dewey number
511.3
Illustrations
illustrations
Index
index present
LC call number
QA76.9.A96
LC item number
T655 2005eb
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2005
http://bibfra.me/vocab/lite/meetingName
TPHOLs
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorName
  • Hurd, Joe
  • Melham, T. F.
Series statement
Lecture notes in computer science,
Series volume
3603
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • COMPUTERS
  • COMPUTERS
  • COMPUTERS
  • COMPUTERS
  • COMPUTERS
  • COMPUTERS
  • COMPUTERS
  • Informatique
  • Automatic theorem proving
  • Automatisches Beweisverfahren
  • Démonstration automatique de théorèmes
  • Logique d'ordre supérieur
  • HOL
Label
Theorem proving in higher order logics : 18th international conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings, Joe Hurd, Tom Melham (eds.)
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
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
Control code
262681818
Dimensions
unknown
Extent
1 online resource (ix, 408 pages)
Form of item
online
Isbn
9783540283720
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
  • 9783540283722
  • 10.1007/11541868.
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-28372-0
Specific material designation
remote
System control number
(OCoLC)262681818
Label
Theorem proving in higher order logics : 18th international conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005 : proceedings, Joe Hurd, Tom Melham (eds.)
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
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
Control code
262681818
Dimensions
unknown
Extent
1 online resource (ix, 408 pages)
Form of item
online
Isbn
9783540283720
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
  • 9783540283722
  • 10.1007/11541868.
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-28372-0
Specific material designation
remote
System control number
(OCoLC)262681818

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125
Processing Feedback ...