04465nam 22007935 450 99646528710331620230222032210.03-540-74591-210.1007/978-3-540-74591-4(CKB)1000000000491030(SSID)ssj0000320357(PQKBManifestationID)11235216(PQKBTitleCode)TC0000320357(PQKBWorkID)10257688(PQKB)10231438(DE-He213)978-3-540-74591-4(MiAaPQ)EBC3063201(MiAaPQ)EBC6707296(Au-PeEL)EBL6707296(PPN)123164680(EXLCZ)99100000000049103020100301d2007 u| 0engurnn|008mamaatxtccrTheorem Proving in Higher Order Logics[electronic resource] 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings /edited by Klaus Schneider, Jens Brandt1st ed. 2007.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2007.1 online resource (VIII, 404 p.) Theoretical Computer Science and General Issues,2512-2029 ;4732Bibliographic Level Mode of Issuance: Monograph3-540-74590-4 Includes bibliographical references and index.On the Utility of Formal Methods in the Development and Certification of Software -- Formal Techniques in Software Engineering: Correct Software and Safe Systems -- Separation Logic for Small-Step cminor -- Formalising Java’s Data Race Free Guarantee -- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL -- Formalising Generalised Substitutions -- Extracting Purely Functional Contents from Logical Inductive Types -- A Modular Formalisation of Finite Group Theory -- Verifying Nonlinear Real Formulas Via Sums of Squares -- Verification of Expectation Properties for Discrete Random Variables in HOL -- A Formally Verified Prover for the Description Logic -- Proof Pearl: The Termination Analysis of Terminator -- Improving the Usability of HOL Through Controlled Automation Tactics -- Verified Decision Procedures on Context-Free Grammars -- Using XCAP to Certify Realistic Systems Code: Machine Context Management -- Proof Pearl: De Bruijn Terms Really Do Work -- Proof Pearl: Looping Around the Orbit -- Source-Level Proof Reconstruction for Interactive Theorem Proving -- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF -- Automatically Translating Type and Function Definitions from HOL to ACL2 -- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models -- Proof Pearl: Wellfounded Induction on the Ordinals Up to ? 0 -- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols -- Primality Proving with Elliptic Curves -- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism -- Building Formal Method Tools in the Isabelle/Isar Framework -- Simple Types in Type Theory: Deep and Shallow Encodings -- Mizar’s Soft Type System.Theoretical Computer Science and General Issues,2512-2029 ;4732Computer scienceMachine theorySoftware engineeringArtificial intelligenceLogic designTheory of ComputationFormal Languages and Automata TheoryComputer Science Logic and Foundations of ProgrammingSoftware EngineeringArtificial IntelligenceLogic DesignComputer science.Machine theory.Software engineering.Artificial intelligence.Logic design.Theory of Computation.Formal Languages and Automata Theory.Computer Science Logic and Foundations of Programming.Software Engineering.Artificial Intelligence.Logic Design.005.115Schneider Klaus1967-Brandt Jens1978-MiAaPQMiAaPQMiAaPQBOOK996465287103316Theorem Proving in Higher Order Logics772309UNISA03003cam0-2200517---450 99000499455040332120230926152333.0NIRA uede roi' feba (3) 1823 (R)feiIT-NA0105: SG 850 B/78(1)oo,o m.on tere (bsi (3) 1823 (R)feiIT-NA0105: SG 850 B/78(2)O.I- die. 9.3. (1ch (3) 1827 (R)feiIT-NA0105: SG 850 B/78(3;1)E.AD b-i- 3.n- orPu (3) 1828 (R)feiIT-NA0105: SG 850 B/78(3;2)000499455FED01000499455(Aleph)000499455FED0100049945519990604g18231828km-y0itay50------baitaITa-----------------bb0-------<<La >>Divina Commedia di Dante Alighieri giusta la lezione del codice bartoliniano. Volume primo [-III parte II]Udinepei fratelli MattiuzziNella tipografia Pecile1823-18283 v.8°Segn.: [I]⁸ II⁸ III⁴ χ¹ [a]⁸ b-d⁸ e⁴ ²χ¹ [1]⁸ 2-20⁸ 21⁶. - Bianca la carta 19/8 (v. 1)Segn.: π² [1]⁸2-17⁸ χ¹ 18-33⁸ 34⁶ ²χ². - Bianche le carte 34/5,34/6 e l'ultima (v. 2)Segn.: *-2*⁸ 3*¹⁰ [1]⁸ 2-49⁸ 50⁴. - Ultima carta bianca (v. 3.1)Segn.: π⁴ ²π¹ 1-29⁴ 30² [31]⁸ 32-42⁸. - Bianche le carte 32/8 e 42/8 (v. 3.2)1.: [42], LXXII, [2], 299, [5], 303-330 p., [2] c. di tav. : ill. calcogr. ; 2.: [4], 272, [2], 265, [7] p. ; 3.1.: LI, [1], 790, [2] p. ; 3.2.: VII, [3], 165 [i.e. 265], [3], 167-323 [i.e. 423], [3] p.Italia.Udine851.122itaAlighieri,Dante<1265-1321>38904Mattiuzzi650Pecile610ITUNINARICAUNIMARC20050512Visualizza la versione elettronica in SBNWebhttps://books.google.it/books?id=o7Y84TdUiwcC&printsec=frontcover&hl=it&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false20230926Visualizza la versione elettronica in SBNWebhttps://books.google.it/books?id=42kQ3vSQbsgC&printsec=frontcover&hl=it&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false20230926Visualizza la versione elettronica in SBNWebhttps://books.google.it/books?id=nUXXzlUNLd4C&printsec=frontcover&hl=it&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false20230926Visualizza la versione elettronica in SBNWebhttps://books.google.it/books?id=jvtyfuoCIvwC&printsec=frontcover&hl=it&source=gbs_ge_summary_r&cad=0#v=onepage&q&f=false20230926AQ990004994550403321SG 850 B/78(1)Ist.f.m.25572FLFBCSG 850 B/78(2)Ist.f.m.25572FLFBCSG 850 B/78(3;1)Ist.f.m.25572FLFBCSG 850 B/78(3;2)Ist.f.m.25572FLFBCFLFBCDivina Commedia di Dante Alighieri giusta la lezione del codice bartoliniano. Volume primo3560042UNINA