MARC details
| 000 -LEADER |
|---|
| fixed length control field |
05788cam a2200793 i 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
ocm57348553 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20250703143131.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS |
|---|
| fixed length control field |
m o d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr ||||||||||| |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
041210s2004 gw a ob 101 u eng d |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
QCL |
| Language of cataloging |
eng |
| Description conventions |
pn |
| Transcribing agency |
QCL |
| Modifying agency |
OCLCQ |
| -- |
N$T |
| -- |
YDXCP |
| -- |
OCLCQ |
| -- |
YNG |
| -- |
OCLCQ |
| -- |
DKDLA |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
GW5XE |
| -- |
OCLCF |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
AZU |
| -- |
OCL |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
EBLCP |
| -- |
UAB |
| -- |
ESU |
| -- |
VT2 |
| -- |
OCLCA |
| -- |
OCLCQ |
| -- |
OCLCA |
| -- |
WYU |
| -- |
OL$ |
| -- |
OCLCQ |
| -- |
AUD |
| -- |
OCLCQ |
| -- |
LUN |
| -- |
EUX |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
INT |
| -- |
OCLCO |
| -- |
WSU |
| -- |
OCLCO |
| -- |
OCLCL |
| -- |
OCLCO |
| -- |
OCLCQ |
| 016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER |
|---|
| Record control number |
97200064X |
| Source |
DE-101 |
| 019 ## - |
|---|
| -- |
62458722 |
| -- |
144566218 |
| -- |
729901537 |
| -- |
768063540 |
| -- |
1005777757 |
| -- |
1066605878 |
| -- |
1081200939 |
| -- |
1105602973 |
| -- |
1132296414 |
| -- |
1171549881 |
| -- |
1172183936 |
| -- |
1239211893 |
| -- |
1374611682 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
3540301429 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9783540301424 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
3540230173 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9783540230175 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9788354030140 |
| Qualifying information |
(4) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
8354030148 |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/b100400 |
| Source of number or code |
doi |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
AU@ |
| System control number |
000051345755 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
14990912 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
NZ1 |
| System control number |
15296648 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
DKDLA |
| System control number |
820120-katalog:999912299205765 |
| 029 1# - (OCLC) |
|---|
| OCLC library identifier |
AU@ |
| System control number |
000078468973 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)57348553 |
| Canceled/invalid control number |
(OCoLC)62458722 |
| -- |
(OCoLC)144566218 |
| -- |
(OCoLC)729901537 |
| -- |
(OCoLC)768063540 |
| -- |
(OCoLC)1005777757 |
| -- |
(OCoLC)1066605878 |
| -- |
(OCoLC)1081200939 |
| -- |
(OCoLC)1105602973 |
| -- |
(OCoLC)1132296414 |
| -- |
(OCoLC)1171549881 |
| -- |
(OCoLC)1172183936 |
| -- |
(OCoLC)1239211893 |
| -- |
(OCoLC)1374611682 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.9.A96 |
| Item number |
T655 2004eb |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
COM |
| Subject category code subdivision |
025000 |
| Source |
bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
QA |
| Source |
lcco |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
006.333 |
| Edition number |
22 |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 111 2# - MAIN ENTRY--MEETING NAME |
|---|
| Meeting name or jurisdiction name as entry element |
TPHOLs |
| Number of part/section/meeting |
(17th : |
| Date of meeting |
2004 : |
| Location of meeting |
Park City, Utah) |
| 9 (RLIN) |
18618 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Theorem proving in higher order logics : |
| Remainder of title |
17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004 : proceedings / |
| Statement of responsibility, etc. |
editors, Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan. |
| 246 30 - VARYING FORM OF TITLE |
|---|
| Title proper/short title |
TPHOLs 2004 |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Berlin : |
| Name of publisher, distributor, etc. |
Springer, |
| Date of publication, distribution, etc. |
2004. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (viii, 336 pages) : |
| Other physical details |
illustrations |
| 336 ## - CONTENT TYPE |
|---|
| Content type term |
text |
| Content type code |
txt |
| Source |
rdacontent |
| 337 ## - MEDIA TYPE |
|---|
| Media type term |
computer |
| Media type code |
c |
| Source |
rdamedia |
| 338 ## - CARRIER TYPE |
|---|
| Carrier type term |
online resource |
| Carrier type code |
cr |
| Source |
rdacarrier |
| 347 ## - DIGITAL FILE CHARACTERISTICS |
|---|
| File type |
text file |
| Source |
rdaft |
| Authority record control number or standard number |
http://rdaregistry.info/termList/fileType/1002 |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture notes in computer science ; |
| Volume/sequential designation |
3223 |
| 500 ## - GENERAL NOTE |
|---|
| General note |
Title from title screen (viewed December 10, 2004). |
| 500 ## - GENERAL NOTE |
|---|
| General note |
Print version originally published in 2004. |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references and index. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
This book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA, in September 2004. The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction. |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
Error Analysis of Digital Filters Using Theorem Proving -- Verifying Uniqueness in a Logical Framework -- A Program Logic for Resource Verification -- Proof Reuse with Extended Inductive Types -- Hierarchical Reflection -- Correct Embedded Computing Futures -- Higher Order Rippling in IsaPlanner -- A Mechanical Proof of the Cook-Levin Theorem -- Formalizing the Proof of the Kepler Conjecture -- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code -- Extensible Hierarchical Tactic Construction in a Logical Framework -- Theorem Reuse by Proof Term Transformation -- Proving Compatibility Using Refinement -- Java Program Verification via a JVM Deep Embedding in ACL2 -- Reasoning About CBV Functional Programs in Isabelle/HOL -- Proof Pearl: From Concrete to Functional Unparsing -- A Decision Procedure for Geometry in Coq -- Recursive Function Definition for Types with Binders -- Abstractions for Fault-Tolerant Distributed System Verification -- Formalizing Integration Theory with an Application to Probabilistic Algorithms -- Formalizing Java Dynamic Loading in HOL -- Certifying Machine Code Safety: Shallow Versus Deep Embedding -- Term Algebras with Length Function and Bounded Quantifier Alternation. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automatic theorem proving |
| Form subdivision |
Congresses. |
| 9 (RLIN) |
14919 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Théorèmes |
| General subdivision |
Démonstration automatique |
| Form subdivision |
Congrès. |
| 9 (RLIN) |
14921 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
COMPUTERS |
| General subdivision |
Expert Systems. |
| Source of heading or term |
bisacsh |
| 9 (RLIN) |
17903 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Automatic theorem proving |
| Source of heading or term |
fast |
| 9 (RLIN) |
14923 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
proceedings (reports) |
| Source of term |
aat |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings |
| Source of term |
fast |
| 9 (RLIN) |
6065 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Conference papers and proceedings. |
| Source of term |
lcgft |
| 9 (RLIN) |
6065 |
| 655 #7 - INDEX TERM--GENRE/FORM |
|---|
| Genre/form data or focus term |
Actes de congrès. |
| Source of term |
rvmgf |
| 9 (RLIN) |
609890 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Slind, Konrad. |
| 9 (RLIN) |
18619 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Bunker, Annette. |
| 9 (RLIN) |
18620 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Gopalakrishnan, Ganesh. |
| 9 (RLIN) |
18621 |
| 710 2# - ADDED ENTRY--CORPORATE NAME |
|---|
| Corporate name or jurisdiction name as entry element |
LINK (Online service) |
| -- |
https://id.oclc.org/worldcat/entity/E39QH7JmqkRqbCq7YPR7CghJc6 |
| 758 ## - |
|---|
| -- |
has work: |
| -- |
Theorem proving in higher order logics (Text) |
| -- |
https://id.oclc.org/worldcat/entity/E39PCFCmDpRkX6TGPqGdbxVxQq |
| -- |
https://id.oclc.org/worldcat/ontology/hasWork |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Main entry heading |
TPHOLs 2004 (2004 : Park City, Utah). |
| Title |
Theorem proving in higher order logics. |
| Place, publisher, and date of publication |
Berlin ; New York : Springer, 2004 |
| International Standard Book Number |
3540230173 |
| Record control number |
(DLC) 2004111288 |
| -- |
(OCoLC)56492378 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| Uniform title |
Lecture notes in computer science ; |
| Volume number/sequential designation |
3223. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
<a href="https://link.springer.com/10.1007/b100400">https://link.springer.com/10.1007/b100400</a> |
| 938 ## - |
|---|
| -- |
ProQuest Ebook Central |
| -- |
EBLB |
| -- |
EBL3087845 |
| 938 ## - |
|---|
| -- |
EBSCOhost |
| -- |
EBSC |
| -- |
144507 |
| 938 ## - |
|---|
| -- |
YBP Library Services |
| -- |
YANK |
| -- |
2367960 |
| 936 ## - OCLC/CONSER MISCELLANEOUS DATA (OCLC); PIECE USED FOR CATALOGING (pre-AACR2) (RLIN) |
|---|
| OCLC control number(s) of parallel record(s) (OCLC); Piece used for cataloging, PUC (RLIN) |
BATCHLOAD |
| 994 ## - |
|---|
| -- |
92 |
| -- |
ATIST |