| 000 | 05604cam a22007454a 4500 | ||
|---|---|---|---|
| 001 | ocn164440057 | ||
| 003 | OCoLC | ||
| 005 | 20250703143555.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 000720s2000 gw a ob 101 0 eng c | ||
| 040 |
_aCOO _beng _epn _cCOO _dHNK _dUAB _dYDXCP _dE7B _dOCLCQ _dIDEBK _dOCLCQ _dOUN _dDKDLA _dOCLCQ _dGW5XE _dOCLCF _dOCLCQ _dOCLCO _dOCL _dOCLCO _dEBLCP _dOCLCQ _dSHS _dOCLCQ _dESU _dOCLCQ _dVT2 _dOCLCA _dOCLCQ _dMERER _dOCLCQ _dLEAUB _dOL$ _dOCLCQ _dAUD _dOCLCQ _dOCLCO _dOCLCQ _dOCLCO _dOCLCQ _dWSU _dOCLCO |
||
| 019 |
_a177507851 _a228375787 _a612013289 _a648319708 _a769771165 _a1005804337 _a1044450207 |
||
| 020 |
_a3540446591 _q(electronic bk.) |
||
| 020 |
_a9783540446590 _q(electronic bk.) |
||
| 020 | _z3540678638 | ||
| 020 | _z9783540678632 | ||
| 024 | 7 |
_a10.1007/3-540-44659-1 _2doi |
|
| 029 | 1 |
_aAU@ _b000051345751 |
|
| 029 | 1 |
_aNZ1 _b14993734 |
|
| 029 | 1 |
_aNZ1 _b15297082 |
|
| 035 |
_a(OCoLC)164440057 _z(OCoLC)177507851 _z(OCoLC)228375787 _z(OCoLC)612013289 _z(OCoLC)648319708 _z(OCoLC)769771165 _z(OCoLC)1005804337 _z(OCoLC)1044450207 |
||
| 042 | _apcc | ||
| 050 | 4 |
_aQA76.9.A96 _bT655 2000 |
|
| 072 | 7 |
_aUYA _2bicssc |
|
| 072 | 7 |
_aMAT018000 _2bisacsh |
|
| 072 | 7 |
_aCOM051010 _2bisacsh |
|
| 082 | 0 | 4 |
_a004/.01/5113 _221 |
| 084 |
_a54.10 _2bcl |
||
| 084 |
_aSS 4800 _2rvk |
||
| 084 |
_aDAT 706f _2stub |
||
| 084 |
_aDAT 005f _2stub |
||
| 049 | _aMAIN | ||
| 111 | 2 |
_aTPHOLs _n(13th : _d2000 : _cPortland, Or.) _921197 |
|
| 245 | 1 | 0 |
_aTheorem proving in higher order logics : _b13th International Conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000 : proceedings / _cMark Aagaard, John Harrison (eds.). |
| 260 |
_aBerlin ; _aHeidelberg ; _aNew York : _bSpringer, _c©2000. |
||
| 300 |
_a1 online resource (ix, 533 pages) : _billustrations |
||
| 336 |
_atext _btxt _2rdacontent |
||
| 337 |
_acomputer _bc _2rdamedia |
||
| 338 |
_aonline resource _bcr _2rdacarrier |
||
| 347 | _atext file | ||
| 347 | _bPDF | ||
| 490 | 1 |
_aLecture notes in computer science, _x0302-9743 ; _v1869 |
|
| 504 | _aIncludes bibliographical references and index. | ||
| 520 | _aThis book constitutes the refereed proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000, held in Portland, Oregon, USA in August 2000. The 29 revised full papers presented together with three invited contributions were carefully reviewed and selected from 55 submissions. All current aspects of HOL theorem proving, formal verification of hardware and software systems, and formal verification are covered. Among the HOL theorem provers evaluated are COQ, HOL, Isabelle, HOL/SPIN, PVS, and Isabelle/HOL. | ||
| 505 | 0 | _aFix-Point Equations for Well-Founded Recursion in Type Theory -- Programming and Computing in HOL -- Proof Terms for Simply Typed Higher Order Logic -- Routing Information Protocol in HOL/SPIN -- Recursive Families of Inductive Types -- Aircraft Trajectory Modeling and Alerting Algorithm Verification -- Intel's Formal Verification Experience on the Willamette Development -- A Prototype Proof Translator from HOL to Coq -- Proving ML Type Soundness Within Coq -- On the Mechanization of Real Analysis in Isabelle/HOL -- Equational Reasoning via Partial Reflection -- Reachability Programming in HOL98 Using BDDs -- Transcendental Functions and Continuity Checking in PVS -- Verified Optimizations for the Intel IA-64 Architecture -- Formal Verification of IA-64 Division Algorithms -- Fast Tactic-Based Theorem Proving -- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover -- A Strong and Mechanizable Grand Logic -- Inheritance in Higher Order Logic: Modeling and Reasoning -- Total-Correctness Refinement for Sequential Reactive Systems -- Divider Circuit Verification with Model Checking and Theorem Proving -- Specification and Verification of a Steam-Boiler with Signal-Coq -- Functional Procedures in Higher-Order Logic -- Formalizing Stålmarck's Algorithm in Coq -- TAS -- A Generic Window Inference System -- Weak Alternating Automata in Isabelle/HOL -- Graphical Theories of Interactive Systems: Can a Proof Assistant Help? -- Formal Verification of the Alpha 21364 Network Protocol -- Dependently Typed Records for Representing Mathematical Structure -- Towards a Machine-Checked Java Specification Book -- Another Look at Nested Recursion -- Automating the Search for Answers to Open Questions -- Appendix: Conjectures Concerning Proof, Design, and Verification. | |
| 650 | 0 |
_aAutomatic theorem proving _vCongresses. _914919 |
|
| 650 | 6 |
_aThéorèmes _xDémonstration automatique _vCongrès. _914921 |
|
| 650 | 7 |
_aAutomatic theorem proving _2fast _914923 |
|
| 655 | 7 |
_aproceedings (reports) _2aat |
|
| 655 | 7 |
_aConference papers and proceedings _2fast _96065 |
|
| 655 | 7 |
_aConference papers and proceedings. _2lcgft _96065 |
|
| 655 | 7 |
_aActes de congrès. _2rvmgf _9609890 |
|
| 700 | 1 |
_aAagaard, Mark, _d1966- _921198 |
|
| 700 | 1 |
_aHarrison, J. _q(John), _d1966- _921199 |
|
| 776 | 0 | 8 |
_iPrint version: _aTPHOLs 2000 (2000 : Portland, Or.). _tTheorem proving in higher order logics. _dBerlin ; Heidelberg ; New York : Springer, ©2000 _w(DLC) 00059577 |
| 830 | 0 |
_aLecture notes in computer science ; _v1869. _x0302-9743 |
|
| 856 | 4 | 0 | _uhttps://link.springer.com/10.1007/3-540-44659-1 |
| 938 |
_aProQuest Ebook Central _bEBLB _nEBL6408004 |
||
| 938 |
_aProQuest Ebook Central _bEBLB _nEBL3061657 |
||
| 938 |
_aebrary _bEBRY _nebr10189177 |
||
| 938 |
_aProQuest MyiLibrary Digital eBook Collection _bIDEB _n95654 |
||
| 938 |
_aYBP Library Services _bYANK _n2719977 |
||
| 994 |
_a92 _bATIST |
||
| 999 |
_c636175 _d636175 |
||