LEADER 05397nam 22007815 450 001 996465644003316 005 20230406062905.0 010 $a3-642-03359-8 024 7 $a10.1007/978-3-642-03359-9 035 $a(CKB)1000000000772900 035 $a(SSID)ssj0000320358 035 $a(PQKBManifestationID)11253489 035 $a(PQKBTitleCode)TC0000320358 035 $a(PQKBWorkID)10248288 035 $a(PQKB)10317773 035 $a(DE-He213)978-3-642-03359-9 035 $a(MiAaPQ)EBC3064450 035 $a(PPN)139950826 035 $a(EXLCZ)991000000000772900 100 $a20100301d2009 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTheorem Proving in Higher Order Logics$b[electronic resource] $e22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Proceedings /$fedited by Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel 205 $a1st ed. 2009. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009. 215 $a1 online resource (XI, 517 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5674 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-03358-X 320 $aIncludes bibliographical references and index. 327 $aInvited Papers -- Let?s Get Physical: Models and Methods for Real-World Security Protocols -- VCC: A Practical System for Verifying Concurrent C -- Without Loss of Generality -- Invited Tutorials -- HOL Light: An Overview -- A Brief Overview of Mizar -- A Brief Overview of Agda ? A Functional Language with Dependent Types -- The Twelf Proof Assistant -- Regular Papers -- Hints in Unification -- Psi-calculi in Isabelle -- Some Domain Theory and Denotational Semantics in Coq -- Turning Inductive into Equational Specifications -- Formalizing the Logic-Automaton Connection -- Extended First-Order Logic -- Formalising Observer Theory for Environment-Sensitive Bisimulation -- Formal Certification of a Resource-Aware Language Implementation -- A Certified Data Race Analysis for a Java-like Language -- Formal Analysis of Optical Waveguides in HOL -- The HOL-Omega Logic -- A Purely Definitional Universal Domain -- Types, Maps and Separation Logic -- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence -- Formalising FinFuns ? Generating Code for Functions as Data from Isabelle/HOL -- Packaging Mathematical Structures -- Practical Tactics for Separation Logic -- Verified LISP Implementations on ARM, x86 and PowerPC -- Trace-Based Coinductive Operational Semantics for While -- A Better x86 Memory Model: x86-TSO -- Formal Verification of Exact Computations Using Newton?s Method -- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL -- A Hoare Logic for the State Monad -- Certification of Termination Proofs Using CeTA -- A Formalisation of Smallfoot in HOL -- Liveness Reasoning with Isabelle/HOL -- Mind the Gap. 330 $aThis book constitutes the refereed proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 200, held in Munich, Germany, in August 2009. The 26 revised full papers presented together with 1 proof pearl, 4 tool presentations, and 3 invited papers were carefully reviewed and selected from 55 submissions. The papers cover all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification such as formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalization of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5674 606 $aComputer science 606 $aMachine theory 606 $aComputer science?Mathematics 606 $aDiscrete mathematics 606 $aAlgorithms 606 $aTheory of Computation 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aMathematics of Computing 606 $aDiscrete Mathematics in Computer Science 606 $aAlgorithms 615 0$aComputer science. 615 0$aMachine theory. 615 0$aComputer science?Mathematics. 615 0$aDiscrete mathematics. 615 0$aAlgorithms. 615 14$aTheory of Computation. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aMathematics of Computing. 615 24$aDiscrete Mathematics in Computer Science. 615 24$aAlgorithms. 676 $a004.0151 702 $aBerghofer$b Stefan$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aNipkow$b Tobias$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aUrban$b Christian$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aWenzel$b Makarius$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTPHOLs 2009 906 $aBOOK 912 $a996465644003316 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNISA LEADER 01333nam a2200313 i 4500 001 991003489559707536 005 20021217151559.0 008 971030s1990 us a b 001 0 eng d 020 $a0867200529 035 $ab1181861x-39ule_inst 035 $aLE00301633$9ExL 040 $aDip.to Biologia$beng 082 0 $a571.6$222 245 00$aHandbook of protoctista :$bthe structure, cultivation, habitats, and life histories of the eukaryotic microorganisms and their descendants exclusive of animals, plants, and fungi :$ba guide to the algae, ciliates, foraminifera, sporozoa, water molds, slime molds, and the other protoctists /$ceditors, Lynn Margulis ... [et al.] 260 3 $aBoston :$bJones and Bartlett Publ.,$cc1990 300 $axli, 914 p. :$bill. ;$c29 cm 440 4$aThe Jones and Bartlett series in life sciences 500 $aIncludes bibliographies 650 0$aAlgae 650 0$aEukaryotic cells 650 0$aMyxomycetes 650 0$aProtista 700 1 $aMargulis, Lynn 907 $a.b1181861x$b11-03-11$c18-12-02 912 $a991003489559707536 945 $aLE003 571.6 MAR01.01 (1990)$g1$i2003000090277$lle003$o-$pE0.00$q-$rl$s- $t0$u1$v24$w1$x0$y.i12069139$z18-12-02 996 $aHandbook of protoctista$9898842 997 $aUNISALENTO 998 $ale003$b01-01-97$cm$da $e-$feng$gus $h0$i1